1
$\begingroup$

I was given a task to construct a Hilbert-style proof for the following:

$A → B ⊢ C ∨ A → C ∨ B$

I figured I could use the axiom $A→B≡A∨B≡B$, but this leads me nowhere since I don't think I can use the consequent anywhere.

The theorem is intuitively true to me (since we know $A→B$, adding a true $C$ in there will give $⊤→⊤$, obviously true, and a false $C$ gives the original $A→B$), but I do not know how to prove this.

I'm using Tourlakis' Mathematical Logic and all axioms contained within it.

$\endgroup$
6
  • $\begingroup$ What you're doing there $A→B≡A∨B≡B$ is neither hilbert-caluclus nor sequent-calculus ... . If you want help on this one, you'll first have to tell us exactly what rules you have to work with, because there are many logical proof systems. $\endgroup$ – Bram28 Feb 19 '19 at 18:39
  • $\begingroup$ I am using Tourlakis' Mathematical Logic (2008) and the axioms contained within it. $\endgroup$ – Bill Feb 19 '19 at 19:57
  • $\begingroup$ Which doesn't help anyone who doesn't have that book on hand. $\endgroup$ – Graham Kemp Feb 19 '19 at 22:32
  • $\begingroup$ Looked at that book ... ugh, that's not a very user-friendly system for beginners. Do you have to use that book? $\endgroup$ – Bram28 Feb 19 '19 at 23:20
  • $\begingroup$ Yeah, it's what the class is using @Bram28 $\endgroup$ – Bill Feb 20 '19 at 0:12
1
$\begingroup$

Here are the relevant Hilbert Axiom Schemas...(your book may label them differently, or treat disjunction as a substitution.)

$$\begin{array}{rl}\mathrm A2.&\phi\to(\psi\to\phi) \\ \mathrm A3.&(\phi\to(\psi\to\xi))\to((\phi\to\psi)\to(\phi\to\xi)) \\ \lor\mathrm {IL}.&\phi\to(\phi\lor\psi) \\ \lor\mathrm {IR}.&\phi\to(\psi\lor\phi) \\ \lor\mathrm E.&(\phi\to\xi)\to((\phi\to\xi)\to((\phi\lor\psi)\to\xi)) \\\hdashline \mathrm P1.&A\to B \\\hline 2.&\lower{2ex}\ddots\end{array}$$

$\endgroup$
1
  • $\begingroup$ Unfortunately, Tourlakis' axioms look nothing like this .... $\endgroup$ – Bram28 Feb 21 '19 at 3:38
0
$\begingroup$

1) $A \to B \ \ \ \ \ \langle \text { assumption } \rangle$

2) $ C \lor A \ \ \ \ \ \ \langle \text { assumption } \rangle$

3) $C \lor A \equiv \lnot C \to A \ \ \ \ \langle 2.4.11 \rangle$

4) $\lnot C \to A \ \ \ \ \langle (2,3) + \text {Eqn} \rangle$

5) $\lnot C \to B \ \ \ \ \langle (2.5.9 \text { Coroll. - Transitivity of} \to) \rangle$

6) $C \lor B \equiv \lnot C \to B \ \ \ \ \langle 2.4.11 \rangle$

7) $C \lor B \ \ \ \ \langle (5,6) + \text {Eqn} \rangle$

8) $C \lor A \to C \lor B \ \ \ \langle (2.6.1 \text { Deduction Theorem}) \rangle$

$\endgroup$

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.