Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question
    
How does your second step follow from axiom 2? –  mjqxxxx Oct 4 '12 at 19:00
    
I think I'm substituting again instead of deducing ... –  Stephen Oct 4 '12 at 19:06
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 you $(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. Can you see what $B$ should be? –  mjqxxxx Oct 4 '12 at 20:43
    
If I substituted $A\lor A$ for B I could use mp to eliminate the first implication leaving $(A\Rightarrow A\lor A)\Rightarrow (A\Rightarrow A)$ and then if I use a specialization of a2 I can use mp again to leave me with $A\Rightarrow A$? (I will explore this on my chalk board but I think that's the direction you're pointing me) –  Stephen Oct 4 '12 at 21:33
    
@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. –  Stephen Oct 4 '12 at 21:34

1 Answer 1

up vote 1 down vote accepted

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} $$

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.