En utilisant la règle « classique » Isabelle

Question

je suis tombé sur un problem set pour la déduction naturelle Isabelle qui utilise la règle classical:

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

Je suis plus habitué à utiliser la « loi du milieu exclu » (excluded_middle) et 'reductio ad absurdum' (ccontr).

Je suppose que classical est équivalent aux deux ci-dessus, mais je ne peux pas en prouver l'un ou l'autre, ou le lemma "A −→ ¬ ¬ A" qui est dans l'ensemble des problèmes. Je ne pense pas que je suis juste en train de mal comprendre la règle, parce que j'ai réussi à l'utiliser avec succès pour prouver lemma "¬ ¬ A −→ A" de l'ensemble des problèmes. Quelqu'un pourrait-il me donner quelques conseils/stratégies/démonstrations pour l'utilisation de cette règle?

Answer 1

Que diriez-vous ceci:

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 

Notez que A ⟶ ¬ ¬ A ne nécessite pas un raisonnement classique:

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

réponse de Joachim Breitner m'a donné toutes les informations dont je avais besoin, mais je voulais le mettre en format que j'ai mieux compris et également équipé de l'ensemble de problème que j'ai initialement référencé (cela dit d'utiliser uniquement la méthode apply).

Voici les preuves de Breitner écrites dans ce format:

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

« Lemme 1 » Je pense que je suis un peu raccourcie puisque je n'ai pas utilisé une seconde notE (il était inutile que le A ∨ ¬ A avait déjà été montré) .

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

Comme le souligne Breitner sur « Lemme 2 » ne pas utiliser classical, et serait en fait valable dans la logique intuitionniste. Quant à ce que j'ai appris pour l'utilisation de la règle classical, on peut la visualiser comme une sorte de «preuve par contradiction»: nous sommes autorisés à assumer la négation et devons prouver notre affirmation originale.