# Re: [isabelle] locales and proofs

```Chris, your code (below) runs fine, but I don't understood your
proof.  Please explain so I can understand the Isabelle proofs.

Isn't Pierce's law the rule
(?P =⇒ ?Q) =⇒ ?P −→ ?Q     (impI)
What do you mean by proof (rule impI)?

I would have proved Pierce's law like this.  Either P or ~P, as you
say.  Two cases:
if P, we're done, because the result is **** --> T, which is T.
If ~P, the result is
((F --> Q) --> F) --> F
= (T --> F) --> F
= F ---> F = T
((F --> Q) --> F) --> F
= (T --> F) --> F
= F ---> F = T

I don't really see how to justify it easily using the Isar rules like
( ¬ ?Q =⇒ ?P) =⇒ ?P ∨ ?Q (disjCI)
which seem primitive.  I'm impressed you wrote such a short proof!

The dox give explain the terms you use, with, show, by etc, but I

--
Best,
Bill

lemma Pierce1: "((P --> Q) --> P) --> P"
proof (rule impI)
assume 1: "(P --> Q) --> P"
have "(~ P) | P" by (rule excluded_middle)
thus P
proof (rule disjE)
assume "P" thus "P" by assumption
next
assume 2: "~ P"
have "P --> Q"
proof (rule impI)
assume "P"
with 2 show "Q" by (rule notE)
qed
with 1 show "P" by (rule mp)
qed
qed

```

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