1

Give a hilbert style proof

$$ \vdash (\lnot B \rightarrow \lnot A) \rightarrow (( \lnot B \rightarrow A) \rightarrow B)$$

How could I prove it ? When I apply deduction theorem, do I take $ ((\lnot B \rightarrow \lnot A) \rightarrow ( \lnot B \rightarrow A)) $ as a whole and move it to the left side because the parentheses or I can split it and do it like the following :

$$ (\lnot B \rightarrow \lnot A ) , (\lnot B \rightarrow A ) \vdash B$$

Lists of axioms and theorems.

enter image description here enter image description here enter image description here

Mauro ALLEGRANZA
  • 94,169
Out Of Bounds
  • 1,531
  • Question I feel silly asking: What is the $\vdash$ symbol? – Carser Apr 13 '14 at 18:29
  • @Jedediyah It means that the statement on the right of $\vdash$ is a syntactic consequence (that is, you can find a formal a proof) of the set of premisses on the left of $\vdash$, in this case, the empty set. – Git Gud Apr 13 '14 at 18:33
  • @Tennisman You're not supposed to use the deduction theorem. You're being asked to give a formal proof. – Git Gud Apr 13 '14 at 18:35
  • No I can use whatever I want. The question didn't give any conditions. Also that is a part of the question. Another part asks to give proof by resolution which needs using deduction theorem. – Out Of Bounds Apr 13 '14 at 18:36
  • 2
    @Tennisman It specifically says give a Hilbert style proof, to me this means it is asking for a formal proof. – Git Gud Apr 13 '14 at 18:37
  • @Tennisman Do you mind listing the axioms? – Git Gud Apr 13 '14 at 18:39
  • @GitGud See the edit please :) – Out Of Bounds Apr 13 '14 at 18:40
  • @Tennisman I removed the predicate calculus shots since they have nothing to do with this. Can you also add the deduction rules? – Git Gud Apr 13 '14 at 18:44
  • As in "Mathematical Logic" by Tourlakis, 2.6.1 Metatheorem. (Deduction theorem) If $ \Gamma \cup {A} \vdash B$ , then also $ \Gamma \vdash A \rightarrow B $. $ \Gamma $ (Gamma) is a set of formulae. – Out Of Bounds Apr 13 '14 at 18:47
  • @Tennisman Your citation demonstrated Git Gud's point. It classifies it as a metatheorem. If you're using a metatheorem, then you're not giving a Hilbert style proof, or equivalently formal proof which happens in the object logic. The deduction metatheorem tells you that a formal proof exists (and its meta-proof tells you how to find a formal proof), but it doesn't actually exhibit a formal proof. – Doug Spoonwood Apr 14 '14 at 01:06
  • One last comment : the original formula of the exercise was : $(\lnot B \rightarrow \lnot A) \rightarrow (\lnot B \rightarrow A) \rightarrow B$; you have inserted the missing parentheses in the wrong way ; it must be : $(\lnot B \rightarrow \lnot A) \rightarrow ((\lnot B \rightarrow A) \rightarrow B)$. See page 16 : "We say that all connectives are right associative." – Mauro ALLEGRANZA Apr 14 '14 at 06:56
  • Yeah I know when we have connectives with the same priority we start from the right. But the question was in a final exam and it was exactly like what I wrote. Let's say there is no mistake and it's like this $((\lnot B \rightarrow A) \rightarrow (\lnot B \rightarrow \lnot A)) $, shouldn't we move it as a whole to the left side when applying deduction theorem? – Out Of Bounds Apr 14 '14 at 11:51

1 Answers1

4

Basically, we can use 2.4.11 Theorem : $\vdash B \rightarrow A \equiv \lnot B \lor A$ [page 70] and using 2.4.4 Theorem (Double Negation) : $\vdash \lnot \lnot A \equiv A$ [page 67] (and Leibniz) to have :

$\vdash (\lnot B \rightarrow A) \equiv (B \lor A)$.

In the same way :

$\vdash (\lnot B \rightarrow \lnot A) \equiv (B \lor \lnot A)$.

Now we apply 2.5.5 Corollary : $A \lor B, \lnot A \lor B \vdash B$ [page 80], to get :

$(\lnot B \rightarrow \lnot A), (\lnot B \rightarrow A) \vdash B$.

Ex 20, page 109, ask to prove it using "the deduction theorem and resolution"; this means to apply, after the two initial transformations, 2.5.4 Theorem (Cut Rule) [page 79] : $A \lor B, \lnot A \lor C \vdash B \lor C$.

In this way, we get :

$(\lnot B \rightarrow \lnot A), (\lnot B \rightarrow A) \vdash B \lor B$.

The result follows by Idempotency of $\lor$ [page 43] and with the application of the Deduction Theorem twice :

$\vdash (\lnot B \rightarrow \lnot A) \rightarrow ((\lnot B \rightarrow A) \rightarrow B) $.

Mauro ALLEGRANZA
  • 94,169