Complex Fitch exercise to prove ∀x.r(x) [closed]

Question

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

Answer 1

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

Answer 2

Here's the solution! I hope this helps anyone else.