Im tryng to prove that this is a theorem using Hilbert calculus $(∀x_1 (∀x_2 (p(x_1) ⇒ ((¬ p(x_2)) ⇒ (¬(p(x_1) ⇒ p(x_2)))))))$

The problem is getting this part $(p(x_1) ⇒ ((¬ p(x_2)) ⇒ (¬(p(x_1) ⇒ p(x_2)))))))$ because then we just have to do some generalizations but i cant seem to prove this i get stuck, I tried using this theorems

$(α ⇒ (β ⇒ (α ∧ β)))$

$ ((α ∧ β) ⇒ α)$

but i cant seem to find a way to get that expression. Thanks.

  • 1
    $\begingroup$ Obviously, for an "Hilbert's proof", you have to state the axioms and rules of the system you are using... $\endgroup$ – Mauro ALLEGRANZA Mar 24 '19 at 12:24

1) $p(x_1)$ --- premise

2) $\lnot p(x_2)$ --- premise

3) $(p(x_1) \to p(x_2))$ --- premise

4) $p(x_2)$ --- from 1) and 3) by MP

Up to now we have : $\{ p(x_1), \lnot p(x_2), (p(x_1) \to p(x_2)) \} \vdash p(x_2)$, and thus, by DT :

6) $\{ p(x_1), \lnot p(x_2) \} \vdash (p(x_1) \to p(x_2)) \to p(x_2)$.

Obviously : $\{ p(x_1), \lnot p(x_2), (p(x_1) \to p(x_2)) \} \vdash \lnot p(x_2)$, and thus, by DT :

7) $\{ p(x_1), \lnot p(x_2) \} \vdash (p(x_1) \to p(x_2)) \to \lnot p(x_2)$.

We use the propositional tautology :

8) $\vdash (A \to B) \to ((A \to \lnot B) \to \lnot A)$

to get :

9) $\{ p(x_1), \lnot p(x_2) \} \vdash \lnot (p(x_1) \to p(x_2))$.

Now we conclude with two application of DT

10) $\vdash p(x_1) \to (\lnot p(x_2) \to \lnot (p(x_1) \to p(x_2)))$

followed by two Generalization :

11) $\forall x_1 \forall x_3 (p(x_1) \to (\lnot p(x_2) \to \lnot (p(x_1) \to p(x_2)))).$

  • $\begingroup$ Ah , i dont think i was aware of the existence of that axiom , guess it simplies it a bit $\endgroup$ – Something Mar 24 '19 at 12:42
  • $\begingroup$ @PedroSantos - as said above, there are many axiom system; the one that I suggest allows every propositional tautology as axiom, plus quantifier axioms and modus ponens. $\endgroup$ – Mauro ALLEGRANZA Mar 24 '19 at 12:45
  • $\begingroup$ Yeah in my logic class we just gave the 5 axioms and the use of MP and Generalizations. Then we constructed theorems that we could use whenever we wanted. $\endgroup$ – Something Mar 24 '19 at 12:46
  • $\begingroup$ Just a questin since we have $p(x_2)$ and its negative cant we aplly the contradiction theorem to get ${p(x1),¬p(x2)⊢ ¬(p(x1)→p(x2))$ and then get the others from the deduction theorem and then do the generalizations ? @MauroALLEGRANZA $\endgroup$ – Something Mar 24 '19 at 17:51
  • 1
    $\begingroup$ @PedroSantos - perfect. You can use it in place of step 8) above. $\endgroup$ – Mauro ALLEGRANZA Mar 24 '19 at 18:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.