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.∀v.¬m(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