A simple device here consists of juxtaposing the axiom and its substitution instance. For example juxtaposing axiom 1 and step 1 like this:
axiom 1 (φ→(ψ→φ))
step 1 (p→((q→p)→p))
Now line up the parentheses arrows or equivalently connective symbols, and letters as much as possible.
axiom 1 ( φ → ( ψ→φ))
| | | |
| | | |
step 1 ( p → ( (q→p)→p))
But wait, make all the arrows line only with arrows, and allow variables to line up with any well-formed formula. Thus, here we have
axiom 1 ( φ → ( ψ → φ ) )
| | | | | | | | |
| | | | ----- | | | |
step 1 ( p → ( (q→p) → p ) )
Thus, to get step 1 from axiom 1 we substitute φ with p (abbreviate φ/p hereafter), and ψ/(q→p). I'll omit drawing lines from parentheses to parentheses.
axiom 2 (( φ → ( ψ → χ )) → (( φ → ψ ) → ( φ → χ)))
| | | | | | | | |
| | ---- | | ----- | | |
step 2 (( p → ( (q→p) → p )) → (( p → (q→p) ) → ( p → p)))
So, φ/p, ψ/(q→p), χ/p gives us step 2 from axiom 2.
Now let's juxtapose step 2 and step 1, but do things a little bit differently. Instead of matching the entirety of step 2 to step 1, let's just match the left hand side of step 2 to step 1. Why do this?
step 2 (( p → ( (q → p) → p )) → (( p → (q→p)) → ( p → p)))
| | | | | | |
| | | | | | |
step 1 ( p → ( (q → p) → p ))
Thus, since the rule of detachment says
$\alpha$
($\alpha$→$\beta$)
$\beta$
we can infer step 3 (( p → (q→p)) → ( p → p)). So, we matched just the left hand side of step 2 here to the entire formula of step 1, because once we did that, we knew we could detach something. Here's axiom 1 and step 4 juxtaposed
axiom 1 ( φ → ( ψ → φ ))
| | | | |
| | | | |
step 4 ( p → ( q → p ))
So in axiom 1 we φ/p, ψ/q.
Now let's put step 4 and step 3 next to each other similar to how we put steps 1 and 2 next to each other.
step 3 ( ( p → ( q → p )) → ( p → p))
| | | | |
| | | | |
step 4 ( p → ( q → p ))
And thus by detachment we may infer (p→p).
You might find the following interesting also. Let's treat the axioms above as steps. Thus, we'll want to match the left hand side of one axiom with the entirety of another axiom.
axiom 2 (( φ → ( ψ → χ )) → (( φ → ψ ) → ( φ → χ)))
| | | | |
| | | | |
axiom 1 ( φ → ( ψ → φ ))
Thus in axiom 2 χ/φ makes the left hand side of axiom 2 into axiom 1 (or the left hand side of axiom 2 becomes equiform with axiom 1). Substitutions have to come as uniform, so in axiom 2 we have to substitute all instance of χ with φ. Thus, by detachment we may infer what the right side becomes after substitution
3 ((φ→ψ)→(φ→φ))).
Now let's juxtapose 3 and axiom 1
3 ( ( φ → ψ ) →(φ→φ)))
| | |
| | -----
axiom 1 ( φ → (ψ→φ) )
So, with the substitution ψ/(ψ→φ) the left hand side of 3 matches the entirety of axiom 1. Thus, we may infer
4 (φ→φ).
I didn't make these diagrams up. Perhaps they are due to A. N. Prior.
If I'm correct I can also replace the entire formula from step 3 by axiom(1)? Then the formula variables would be the three atomic propositions.
Is this correct?
– Byebye May 27 '14 at 13:49"I can also replace the entire formula from step 3 by axiom(1)?"– Git Gud May 27 '14 at 13:51Could you explain how they got from the formula in step 3 to the formula in step 4?
And if they applied axiom(1) to get from the formula in step 3 how did they do that?
– Byebye May 27 '14 at 13:54(Did I phrase that correctly?)
Which got me confused as there seemed to be no relation to step 3 at all (other than having the same atomic propositions).
– Byebye May 27 '14 at 14:03