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$
  • $\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 at 18:39
  • $\begingroup$ I am using Tourlakis' Mathematical Logic (2008) and the axioms contained within it. $\endgroup$ – Bill Feb 19 at 19:57
  • $\begingroup$ Which doesn't help anyone who doesn't have that book on hand. $\endgroup$ – Graham Kemp Feb 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 at 23:20
  • $\begingroup$ Yeah, it's what the class is using @Bram28 $\endgroup$ – Bill Feb 20 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$
  • $\begingroup$ Unfortunately, Tourlakis' axioms look nothing like this .... $\endgroup$ – Bram28 Feb 21 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.