4

⊢(¬A→A)→A

I don't know how to solve this proof with the Axiom, Theorem and Inference rule in Hilbert-style proof system so I ask my classmate and he show me his answer. After viewing his proof, I was confused that his proof have controdiction in the assumption. (¬A→A)and ¬A can't be both true, so I disagreed with his proof. But he insisted that he is right. So I want to ask you for help. Can assumption in Hilbert style proof system be contradictory? If not, how to prove the formula correctly. His proof is attached below: enter image description here

4
  • Yes, it is possible. Ex Falso (aha Explosion) is a valid principle. Commented May 5 at 6:55
  • It is perfectly logical: he shows that if you assume ~A->A and ~A at the same time, you can obtain a contradiction. Therefore they cannot both be true at once. Therefore, if one is true, the other must be false.
    – causative
    Commented May 5 at 7:57
  • 4
    This is not a Hilbert-style proof. Such a proof cannot have ⊢ in it, nor can one use deduction meta-theorem as in 7 and 10. This looks more like a natural deduction proof with 7 and 10 as Implication Introductions. And yes, you can use subproofs with contradictory assumptions in natural deductions, and then discharge the assumptions by Implication Introductions.
    – Conifold
    Commented May 5 at 7:58
  • If you still want an answer in Hilbert style, can you provide the axioms? Commented May 5 at 13:20

1 Answer 1

1

As Conifold points out, you can use contradictory assumptions in natural deduction proofs. You just have to discharge the assumptions in the usual way. But your question asks about a Hilbert style proof, and the proof you show is not one of those.

You haven't specified which Hilbert style proof system you propose to use. Let's use Hilbert's own system, which consists of these five axioms and the rule of modus ponens (MP).

A1. φ → (χ → φ) 
A2. (φ → (χ → ψ)) → (χ → (φ → ψ)) 
A3. (χ → ψ) → ((φ → χ) → (φ → ψ)) 
A4. φ → (¬φ → χ) 
A5. (φ → χ) → ((¬φ → χ) → χ) 

Your theorem may be proved as follows:

1.  A → (B → A)                                     A1 
2.  (A → (B → A)) → (B → (A → A))                   A2
3.  B → (A → A)                                     1,2 MP
4.  A → (¬B → A)                                    A1 
5.  (A → (¬B → A)) → (¬B → (A → A))                 A2
6.  ¬B → (A → A)                                    4,5 MP
7.  (B → (A → A)) → ((¬B → (A → A)) → (A → A))      A5 
8.  (¬B → (A → A)) → (A → A)                        7,3 MP
9.  A → A                                           8,6 MP
10. (A → A) → ((¬A → A) → A)                        A5
11. (¬A → A) → A                                    10,9 MP 

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .