CODEWITHSUNDEEP
logicisabelle
IIM
IIM

Reputation: 533

Using the rule 'classical' in Isabelle

I came across a problem set for natural deduction in Isabelle that uses the rule classical:

( \<not> A ==> A) ==>A

I am more used to using the 'law of excluded middle' (excluded_middle) and 'reductio ad absurdum' (ccontr).

I'm assuming that classical is equivalent to both of the above, but I can't prove either of them from it, or the lemma "A −→ ¬ ¬ A" which is in the problem set. I don't think I am just misunderstanding the rule, because I managed to use it successfully to prove lemma "¬ ¬ A −→ A" from the problem set. Could someone give me some tips/strategies/demonstrations for using this rule?

Upvotes: 3

Views: 448

Answers (2)

IIM
IIM

Reputation: 533

Joachim Breitner's answer gave me all the information I needed, but I wanted to put it into a format that I understood better and also fitted with the problem set I originally referenced (this said to use only the apply method).

Here are Breitner's proofs written in this format:

lemma 1: "A ∨ ¬ A"
apply (rule classical)
apply (rule disjI1)
apply (rule classical)
apply (erule notE)
apply (rule disjI2)
apply assumption
done

'Lemma 1' I think I have shortened slightly since I did not use a second notE (it was unnecessary as the A ∨ ¬ A had already been shown).

lemma 2: "A ⟶ ¬ ¬ A"
apply (rule impI)
apply (rule notI)
apply (rule notE)
apply assumption
apply assumption
done

As Breitner points out, 'Lemma 2' does not use classical, and would in fact be valid in intuitionistic logic.

As for what I have learned for using the rule classical, one can visualise it as a kind of 'proof by contradiction': we are allowed to assume the negation and must prove our original statement.

Upvotes: 1

Joachim Breitner
Joachim Breitner

Reputation: 25782

How about this:

lemma "A ∨ ¬ A"
proof(rule classical)
  assume "¬ (A ∨ ¬ A)"
  have "A"
  proof(rule classical)
    assume "¬ A"
    hence "(A ∨ ¬ A)" by (rule disjI2)
    with ‹¬ (A ∨ ¬ A)›
    show ?thesis by (rule notE)
  qed
  hence "(A ∨ ¬ A)" by (rule disjI1)
  with ‹¬ (A ∨ ¬ A)›
  show ?thesis by (rule notE)
qed

Note that A ⟶ ¬ ¬ A does not require classical reasoning:

lemma "A ⟶ ¬ ¬ A"
proof(rule impI)
  assume A
  show "¬ ¬ A"
  proof(rule notI)
    assume "¬ A"
    from this ‹A›
    show False by (rule notE)
  qed
qed

Upvotes: 5

Related Questions