[isabelle] checking if a formula is intuitionistically valid



-----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-----


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.