0
$\begingroup$

I'm learning propositional calculus in a discrete mathematics course.

I'm trying to kick the habit of using axioms like equations and now I'm a little stuck and could use a nudge.

Using a compact Hilbert system of axioms: $ \begin{array}[ll] \text{a1}:&A\lor A\Rightarrow A\\ \text{a2}:&A\Rightarrow A\lor B\\ \text{a3}:&A\lor B\Rightarrow B\lor A\\ \text{a4}:&(A\Rightarrow B)\Rightarrow((C\Rightarrow A)\Rightarrow (C\Rightarrow B))\\ \end{array} \\\\ \text{Prove: }A\Rightarrow A $

I derived the following:

$ \begin{array}[lll] \\ 1&(A\Rightarrow B)\Rightarrow((A\lor A\Rightarrow A)\Rightarrow (A \lor A\Rightarrow B))&\text{using C=$A\lor A$ in a4}\\ 2&(A\Rightarrow B)\Rightarrow (A\lor A\Rightarrow B)&\text{mp using 1 and a1}\\ 3&(A\Rightarrow A\lor B)\Rightarrow(A\lor A \Rightarrow A\lor B)&\text{sub. A$\lor$ B for B}\\ 4&A\lor A\Rightarrow A\lor B&\text{mp using 3 and a2}\\ \end{array} $ I'm pretty sure I'm not too far off of getting this to come together but I'm a little stumped as to an appropriate substitution.

Or have I taken a wrong turn in one of my substitutions already?

  • 0
    @mjqxxxx Thank you for your help, it's greatly aided my understanding. I think I will try to find a book or site with a list of problems so I can practice this more.2012-10-04

1 Answers 1

1

The only way to derive $A \Rightarrow A$ is using axiom 4 (or axiom 1, if you could first derive $(A \Rightarrow A) \vee (A \Rightarrow A)$, which seems harder rather than easier). Replacing $B$ and $C$ with $A$, and $A$ with $B$, in axiom 4 gives $(B\Rightarrow A) \Rightarrow ((A\Rightarrow B)\Rightarrow(A\Rightarrow A))$. So if you can get $B \Rightarrow A$ and $A \Rightarrow B$ for any formula $B$, you have the result. Using $A\vee A$ in place of $B$ works. Here's a proof: $ \begin{array}{ l l l } \text{a.} & (A \vee A\Rightarrow A) \Rightarrow ((A\Rightarrow A\vee A)\Rightarrow (A\Rightarrow A)) & \text{(specialization of axiom 4)} \\ \text{b.} & (A\Rightarrow A\vee A)\Rightarrow(A\Rightarrow A) & \text{(a. and axiom 1, using modus ponens)} \\ \text{c.} & A\Rightarrow A\vee A & \text{(specialization of axiom 2)} \\ \text{d.} & A\Rightarrow A & \text{(b. and c., using modus ponens)} \\ \end{array} $