Email Gateway (Aug 22 2022 at 10:07): Email Gateway (Aug 22 2022 at 10:07):From: "W. Douglas Maurer" <maurer@gwu.edu>
I have been taught to write proof (rule ccontr) at the start of a
proof by contradiction. Looking through the library, I see over four
dozen uses of (rule ccontr) in proofs. Yet there are some proofs by
contradiction in which (rule ccontr) is not used, and in which, in
fact, it wouldn't work if it were used. In particular, step 5 of the
proof of Cantor's theorem in "A Tutorial Introduction to Structured
Isar Proofs" is of this form; it is just the word "proof" by itself.
So my question is: When do you use (rule ccontr), and when don't you
use that rule? What are the criteria? -Douglas
Email Gateway (Aug 22 2022 at 10:07):From: Lars Noschinski <noschinl@in.tum.de>
This proof starts with the rule notI (implicitly). Strictly speaking,
this is not a proof by contradiction, as you don't need the law of the
exlucded middle here.
The proof would also work with "rule ccontr" as initial step. Instead of
"?S : range f", your assumption would then be "~~ ?S : range f", which
simplifies (using the law of the excluded middle) to "?S : range f".
Last updated: Apr 25 2024 at 12:23 UTC