Re: [isabelle] checking if a formula is intuitionistically valid



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.

Please consult the table of ascii equivalents of mathematical symbols in the appendix of the Tutorial on Isabelle/HOL.


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

apply iprover (* for intuitionistic logic *)
apply blast   (* for classical logic *)

Regards
Tobias





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