Verwenden die Regel ‚klassische‘ in Isabelle

Question

stieß ich auf ein problem set für natürliche Abzug in Isabelle, die die Regel classical verwendet:

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

ich mit dem ‚Gesetz der ausgeschlossenen Mitte‘ bin mehr gebraucht (excluded_middle) und "reductio ad absurdum" (ccontr).

Ich gehe davon aus, dass classical ist äquivalent zu beiden der oben genannten, aber ich kann nicht beweisen, von ihnen, oder die lemma "A −→ ¬ ¬ A", die in dem Problem ist. Ich glaube nicht, dass ich die Regel nur falsch verstehe, weil ich es geschafft habe, es erfolgreich zu verwenden, um lemma "¬ ¬ A −→ A" aus dem Problemsatz zu beweisen. Könnte mir jemand Tipps/Strategien/Demonstrationen für die Verwendung dieser Regel geben?

Answer 1

Wie wäre es damit:

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 

Beachten Sie, dass A ⟶ ¬ ¬ A nicht klassische Argumentation erfordert:

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 

Answer 2

Joachim Breitner Antwort gab mir alle Informationen, die ich brauchte, aber ich wollte es in ein setzen Format, das ich besser verstanden habe und auch mit der Problemmenge, auf die ich ursprünglich Bezug nahm (die besagt, dass nur die apply Methode verwendet wird).

Hier Are Breitner's proofs written in dieser 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 nicht Einsatz ein zweites notE (es WAS unnecessary als die A ∨ ¬ A had bereits been shown) .

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

Wie Breitner weist darauf hin, 'Lemma 2' nicht verwendet classical, und in der Tat würde in intuitionismus gültig.

Was ich für die Verwendung der Regel classical gelernt habe, kann man es sich als eine Art "Beweis durch Widerspruch" vorstellen: Wir dürfen die Negation annehmen und müssen unsere ursprüngliche Aussage beweisen.