Introduction to Logic
Assume a language with the object constant a and the function constant s. Given r(a), ∀x.(p(x) ⇒ r(s(x))), ∀x.(q(x) ⇒ r(s(x))), and ∀x.(r(x) ⇒ p(x) ∨ q(x)), use the Fitch system with Linear Induction to prove ∀x.r(x).
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
r(a)
Premise
2
AX:(p(X) => r(s(X)))
Premise
3
AX:(q(X) => r(s(X)))
Premise
4
AX:(r(X) => p(X)  q(X))
Premise
5
r(X)
Assumption
6
r(X) => p(X)  q(X)
Universal Elimination
4
7
p(X)  q(X)
Implication Elimination
5
6
8
p(X) => r(s(X))
Universal Elimination
2
9
q(X) => r(s(X))
Universal Elimination
3
10
r(s(X))
Or Elimination
7
8
9
11
r(X) => r(s(X))
Implication Introduction
5
10
12
AX:(r(X) => r(s(X)))
Universal Introduction
11
13
AX:r(X)
Induction
1
12
