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.
∀u.∀v.(m(u) ⇒ p(c(u,v)))
∀u.∀v.(p(v) ⇒ p(c(u,v)))
∀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).