Email Gateway (Aug 18 2022 at 20:04): Email Gateway (Aug 18 2022 at 20:04):From: Bill Richter <richter@math.northwestern.edu>
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
couldn't figure out what they meant. Please explain in your example!
Last updated: Apr 27 2024 at 01:05 UTC