Introduction to Logic

Consider a language with object constants a and b, binary function constant c, and unary relation constants m and p and q. The definitions for the relations are shown below. Relation m is true of a and only a. Relation p is true of a structured object if and only if it is a linear list (as defined in Chapter 7) with a top-level element that satisfies m. Relation q is true of a structured object if and only if there is an element anywhere in the structure that satisfies m.

m(a)
¬m(b)
u.∀vm(c(u,v))
  u.∀v.(m(u) ⇒ p(c(u,v)))
u.∀v.(p(v) ⇒ p(c(u,v)))
¬p(a)
¬p(b)
u.∀v.(p(c(u,v)) ⇒ m(u) ∨ p(v))
  u.(m(u) ⇒ q(u)))
u.∀v.(q(u) ⇒ q(c(u,v)))
u.∀v.(q(v) ⇒ q(c(u,v)))
¬m(a) ⇒ ¬q(a)
¬m(b) ⇒ ¬q(b)
u.∀v.(q(c(u,v)) ⇒ q(u) ∨ q(v))

Your job is to show that any object that satisfies p also satisfies q. Starting with the preceding axioms, use Fitch with Structural Induction to prove ∀x.(p(x) ⇒ q(x)). Beware: The proof requires more than 50 steps (including the premises).

Show Instructions
Herbrand
Objects a, b, c
Functions f, g
Goal  Incomplete