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

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

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. Commented Jun 1, 2020 at 22:10
• "Or elimination" will work. It is exactly what you should do after some more universal eliminations. @JessieThePinkMan Commented 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. Commented Jun 2, 2020 at 17:07

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