1

I'm trying to prove a formula in the Hilbert system.

First of all, I have a question whether a certain step is allowed. Provided that the theorem ⊢A→A has already been proven in the Hilbert system.

Can I replace an occurence of the form A→A in another proof in the Hilbert system by true (since A→A is provable)?

Secondly, I'm trying to proof ⊢A∧B→A. However, I get stuck. I first try to remove the conjunction. 

      ....
{¬A,A} ⊢ ¬B         (deduction)
{¬A}   ⊢ A→¬B       (deduction)
       ⊢ ¬A→(A→¬B)  (contrapositive)
       ⊢ ¬(A→¬B)→A  (definition ∧) 
       ⊢ A∧B→A

As you can see, I get a contradiction wihtin the axioms. Does anyone have any suggestions of how to proof this theorem in the Hilbert system?

José Carlos Santos
  • 427,504
Alwin
  • 11
  • 1
    (1) It may be very very useful to know about the axioms and rules you are allowed to use... (2) You cannot replace $A \rightarrow A$ in another formula to get a new theorem; what you can do is to replace into the theorem $\vdash A \rightarrow A$ a formula $B$ in place of (every occurrence of) $A$ and you get a new theorem (e.g. let $B := P \lor P$, you may have : $\vdash (P \lor P) \rightarrow (P \lor P)$). – Mauro ALLEGRANZA Mar 10 '14 at 17:15
  • Of course, when you have proved $\vdash A \rightarrow A$, you can use it in a new proof; i.e., you can use it as a "derived" axiom. I mean that in a proof of $A$ form the set of assumprions $\Gamma$ (i.e. $\Gamma \vdash A$) you can tacitly "enlarge" $\Gamma$ to include also $A \rightarrow A$; due to the fact that $\vdash A \rightarrow A$ (you have already proved it) you have also (trivially) : $\Gamma \vdash (A \rightarrow A)$. – Mauro ALLEGRANZA Mar 10 '14 at 17:29
  • Basically your proof is sound, provided that you have already proved (or they are in your "axiom set") : (i) $\vdash \lnot A \rightarrow (A \rightarrow B)$ - you need it in the first step; (ii) $\vdash (\lnot A \rightarrow B) \rightarrow (\lnot B \rightarrow A)$ - you need it in order to "contrapose". – Mauro ALLEGRANZA Mar 10 '14 at 17:35
  • Okay, so if I understand you correctly, I cannot for instance deduce ⊢ ¬true → (B→¬C) from ⊢ ¬(A → A) → (B→¬C) given that A → A has already been proven (and could be added as axiom) – Alwin Mar 10 '14 at 17:38
  • NO; what you can do (for example) is : $\vdash (B \rightarrow \lnot C)$ from $\vdash (A \rightarrow A) \rightarrow (B \rightarrow \lnot C)$ given that $(A \rightarrow A)$ has already been proven. – Mauro ALLEGRANZA Mar 10 '14 at 17:40
  • From $\vdash \lnot A \rightarrow (A \rightarrow \lnot B)$ that must be provable (if it is not an axiom), because it is a tautology, if you may contrapose, you will get (by modus ponens, and you will also double negation) your : $\vdash \lnot (A \rightarrow \lnot B) \rightarrow A$ and then you may apply the definition of $\land$. – Mauro ALLEGRANZA Mar 10 '14 at 17:44

0 Answers0