Email Gateway (Aug 18 2022 at 10:11): Email Gateway (Aug 18 2022 at 10:11):From: Joseph Vidal-Rosset <joseph.vidal-rosset@univ-nancy2.fr>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Hello,
I am sincerely interested in using isabelle but I meet real
difficulties in starting alone with it.
First of all, I would be happy if I'd succeed to use isabelle just as
as simple theorems checker for formulas of first order logic. For
example, I do not even succeed in checking the validity of a classical
formula like:
(p \to q) \leftrightarrow (\neg q \to \neg p) (1)
I know that it is not useful to get isabelle in order to use it at this
low level, but I would be happy to get help just with the syntax. I do
not know why when I try to read the manuals I meet always message of
error. Thanks to tell me how to translate (1) in isar. That will help
me.
The second question that I want to ask here is maybe very naive, but I
do not feel shame. Is it possible to use isabelle just to check it a
propositional formula is intuionistically valid, or just classically
valid? For example: can isabelle tell me that (p \lor \neg p) is not
(intuitionistically) valid? And what about first order intuitionist
predicate calculus?
Thanks for your help,
Jo.
Joseph Vidal-Rosset
Université de Nancy 2
Département de philosophie
Bd Albert 1er
F-54000 Nancy
page web: http://jvrosset.free.fr
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
iD8DBQFF0tyyFVqVy0eTtT8RAvmoAKCNzMGPc71KHJBs/28VPdsyhyZyGACdF0aB
9/K/XaX7m/esPs+42XAC/Nw=
=MIfO
-----END PGP SIGNATURE-----
Last updated: Nov 21 2024 at 12:39 UTC