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).

I know I have to reach r(X) => r(s(X)) so I’m guessing I’ve made a mistake somewhere between steps 8 and 10, but I can’t figure it out exactly. Any help is much appreciated. Thanks. (I’m using Stanford’s proof assistant). enter image description here

2 Answers 2


You are building up to to an implication introduction for an arbitrary x: assuming r(x) aiming to derive r(s(x)). That is the correct approch.

So after assuming r(x), why not look for a premise that will give you something to usable with that assumption? The fourth premise.

  |  r(a)                      Premise
  |  ∀x.(p(x) ⇒ r(s(x)))       Premise
  |  ∀x.(q(x) ⇒ r(s(x)))       Premise
  |_ ∀x.(r(x) ⇒ p(x) ∨ q(x))   Premise
  |  |_ r(x)                    Assumption
  |  |  r(x) ⇒ p(x) ∨ q(x)     ∀Elimination: 4
  |  |  p(x) ∨ q(x)            ⇒Elimination: 6             
  :  :  :
  :  :  :
  |  |  r(s(x))                
  |  r(x) ⇒ r(s(x))            ⇒Introduction
  |  ∀x.(r(x) ⇒ r(s(x))        ∀Introduction
  |  ∀x.r(x)                    Induction

Well, you should see where this is going. ...

  • Thank you Graham. This really helped me a lot. However, do you know how do I continue from p(x) ∨ q(x) ? “Or elimination” option doesn't work in this case. Jun 1, 2020 at 22:10
  • "Or elimination" will work. It is exactly what you should do after some more universal eliminations. @JessieThePinkMan Jun 1, 2020 at 22:59
  • Thanks Graham. You were right. Just figured how to solve it. I'm attaching a copy here in case it helps anyone else. Jun 2, 2020 at 17:07

Here's the solution! I hope this helps anyone else.enter image description here

Not the answer you're looking for? Browse other questions tagged .