Introduction to Logic
Consider a language with a single object constant a, a single unary function constant s, and two unary relation constants p and q. We start with the premises shown below. We know that p is true of s(a) and only s(a). We know that q is also true of s(a), but we do not know whether it is true of anything else.
¬p(a) 
p(s(a)) 
∀x:¬p(s(s(x))) 
q(s(a)) 
Prove ∀x.(p(x) ⇒ q(x)). Hint: Break the problem into two parts  first prove the result for s(x), and then use that intermediate conclusion to prove the overall result.
Show Instructions
To apply a rule of inference, check the lines you wish to use as premises and click the button for the rule of inference. Reiteration allows you to repeat an earlier item. To delete one or more lines from a proof, check the desired lines and click Delete. When entering expressions, use Ascii characters only. Use ~ for ¬; use & for ∧; use  for ∨; use => for ⇒; use <=> for ⇔; use A for ∀; use E for ∃; and use : for . in quantified sentences. Also, for variables use strings of alphanumeric characters that begin with a capital letter. For example, to write the sentence ∀x.∃y.(p(x) ∧ q(y) ⇒ r(y)∨¬s(y)), write AX:EY:(p(X)&q(Y)=>r(Y)~s(Y)).
1
~p(a)
Premise
2
p(s(a))
Premise
3
AX:~p(s(s(X)))
Premise
4
q(s(a))
Premise
5
p(s(a))
Assumption
6
q(s(a))
Reiteration
4
7
p(s(a)) => q(s(a))
Implication Introduction
5
6
8
p(s(X)) => q(s(X))
Assumption
9
p(s(s(X)))
Assumption
10
~q(s(s(X)))
Assumption
11
p(s(s(X)))
Reiteration
9
12
~q(s(s(X))) => p(s(s(X)))
Implication Introduction
10
11
13
~q(s(s(X)))
Assumption
14
~p(s(s(X)))
Universal Elimination
3
15
~q(s(s(X))) => ~p(s(s(X)))
Implication Introduction
13
14
16
~~q(s(s(X)))
Negation Introduction
12
15
17
q(s(s(X)))
Negation Elimination
16
18
p(s(s(X))) => q(s(s(X)))
Implication Introduction
9
17
19
(p(s(X)) => q(s(X))) => (p(s(s(X))) => q(s(s(X))))
Implication Introduction
8
18
20
AX:((p(s(X)) => q(s(X))) => (p(s(s(X))) => q(s(s(X)))))
Universal Introduction
19
21
AX:(p(s(X)) => q(s(X)))
Induction
7
20
22
p(a)
Assumption
23
~q(a)
Assumption
24
p(a)
Reiteration
22
25
~q(a) => p(a)
Implication Introduction
23
24
26
~q(a)
Assumption
27
~p(a)
Reiteration
1
28
~q(a) => ~p(a)
Implication Introduction
26
27
29
~~q(a)
Negation Introduction
25
28
30
q(a)
Negation Elimination
29
31
p(a) => q(a)
Implication Introduction
22
30
32
p(X) => q(X)
Assumption
33
p(s(X)) => q(s(X))
Universal Elimination
21
34
(p(X) => q(X)) => (p(s(X)) => q(s(X)))
Implication Introduction
32
33
35
AX:((p(X) => q(X)) => (p(s(X)) => q(s(X))))
Universal Introduction
34
36
AX:(p(X) => q(X))
Induction
31
35
