# Language proof and logic Chapter 15 question 16 help

I'm trying to go about solving this problem but I'm having problems even knowing how to approach it. Can someone help me to set it up?

Here is the premise: ∀x∀y(x ⊆ y ↔️ ∀z(z ∈ x ⟶ z ∈ y)

Here is the goal: ∀x∀y∀z((x ⊆ y ∧ y ⊆ z) ⟶ x ⊆ z)

• Don't try to instantiate to `s` until you have raised a context containing the term as a local variable. Nov 30 '18 at 7:06

Here is the premise: ∀x∀y(x ⊆ y ↔️ ∀z(z ∈ x ⟶ z ∈ y)

Here is the goal: ∀x∀y∀z((x ⊆ y ∧ y ⊆ z) ⟶ x ⊆ z)

Your premise is a definition for the subset relation. Your goal is the property of transitivity. You should recognise them, although knowing this not needed for this problem.

Anyway. Your obvious first step is to set up Universal Introductions ... and let's do a Conditional Introduction while we're at it. (Note: Some proof checkers allow you to combine these steps)

``````|_ ∀x ∀y (x ⊆ y ↔️ ∀z(z ∈ x ⟶ z ∈ y)
|  |_ [a]
|  |  |_ [b]
|  |  |  |_ [c]
|  |  |  |  :                                    :
|  |  |  |  |_ a ⊆ b ∧ b ⊆ c
|  |  |  |  |   :                                :
|  |  |  |  |  a ⊆ c                             ...
|  |  |  |  (a ⊆ b ∧ b ⊆ c) ⟶ a ⊆ c             ⟶I
|  |  |  ∀z ((a ⊆ b ∧ b ⊆ z) ⟶ a ⊆ z)           ∀I
|  |  ∀y ∀z ((a ⊆ y ∧ y ⊆ z) ⟶ a ⊆ z)           ∀I
|  ∀x ∀y ∀z ((x ⊆ y ∧ y ⊆ z) ⟶ x ⊆ z)           ∀I
``````

To obtain equivalences for those three subset statements, use Universal Elimination on the premise a few times.

Now, those will be three universal quantified statements, so assume another arbitrary term in order to eliminate and introduce the universal quantifiers as needed.

Everything then meets at the middle with a sub-proof for the constructive dilemma.

`````` |_ ∀x ∀y (x ⊆ y ↔️ ∀z(z ∈ x ⟶ z ∈ y))
|  |_ [a]
|  |  |_ [b]
|  |  |  |_ [c]
|  |  |  |  ∀y (a ⊆ y ↔️ ∀z(z ∈ a ⟶ z ∈ y))      ∀E
|  |  |  |  ∀y (b ⊆ y ↔️ ∀z(z ∈ b ⟶ z ∈ y))      ∀E
|  |  |  |  a ⊆ b ↔️ ∀z(z ∈ a ⟶ z ∈ b)           ∀E
|  |  |  |  a ⊆ c ↔️ ∀z(z ∈ a ⟶ z ∈ c)           ∀E
|  |  |  |  b ⊆ c ↔️ ∀z(z ∈ b ⟶ z ∈ c)           ∀E
|  |  |  |  |_ a ⊆ b ∧ b ⊆ c
|  |  |  |  |  a ⊆ b                              ∧E
|  |  |  |  |  b ⊆ c                              ∧E
|  |  |  |  |  ∀z(z ∈ a ⟶ z ∈ b)                 ↔️E
|  |  |  |  |  ∀z(z ∈ b ⟶ z ∈ c)                 ↔️E
|  |  |  |  |  |_ [d]
|  |  |  |  |  |  d ∈ a ⟶ d ∈ b                  ∀E
|  |  |  |  |  |  d ∈ b ⟶ d ∈ c                  ∀E
|  |  |  |  |  |  |_ d ∈ a
|  |  |  |  |  |  |  d ∈ b                        ⟶E
|  |  |  |  |  |  |  d ∈ c                        ⟶E
|  |  |  |  |  |  d ∈ a ⟶ d ∈ c                  ⟶I
|  |  |  |  |  ∀z(z ∈ a ⟶ z ∈ c)                 ∀I
|  |  |  |  |  a ⊆ c                              ↔️E
|  |  |  |  (a ⊆ b ∧ b ⊆ c) ⟶ a ⊆ c             ⟶I
|  |  |  ∀z ((a ⊆ b ∧ b ⊆ z) ⟶ a ⊆ z)           ∀I
|  |  ∀y ∀z ((a ⊆ y ∧ y ⊆ z) ⟶ a ⊆ z)           ∀I
|  ∀x ∀y ∀z ((x ⊆ y ∧ y ⊆ z) ⟶ x ⊆ z)           ∀I
``````
• I'm sorta getting it but I'm having trouble trying to make a ⊆ c, it's not letting me use elimination to get there. And i was trying to implement a similar system to what someone else commented above but it doesn't seem to be working out. Nov 30 '18 at 5:10

Here is the premise: ∀x∀y(x ⊆ y ↔️ ∀z(z ∈ x ⟶ z ∈ y)

Here is the goal: ∀x∀y∀z((x ⊆ y ∧ y ⊆ z) ⟶ x ⊆ z)

In natural language, the premise says that if a set x is a subset of a set y then for all elements z of the set x those elements z are also elements of the set y. The goal is to show that this entails that if a set x is a subset of a set y and that set y is a subset of a set z then the set x is a subset of the set z.

I will outline how you might proceed.

The premise defines what it means for one set to be a subset of another in terms of elements of those sets. Since the goal has three subset relationships use universal elimination three times to derive the following three lines from the premise:

• a ⊆ b ↔️ s ∈ a ⟶ s ∈ b
• b ⊆ c ↔️ s ∈ b ⟶ s ∈ c
• a ⊆ c ↔️ s ∈ a ⟶ s ∈ c

In the above a, b and c are names for sets and s is the name for an element of a set.

Make an assumption: a ⊆ b ∧ b ⊆ c

This is the antecedent of the goal. We need to derive the consequent: a ⊆ c

Use conjunction elimination to break up the assumption into two lines:

• a ⊆ b
• b ⊆ c

Use conditional elimination or modus ponens to derive these two lines:

• s ∈ a ⟶ s ∈ b
• s ∈ b ⟶ s ∈ c

Make an assumption: s ∈ a

From that derive s ∈ b and from that derive s ∈ c.

Discharge that last assumption by introducing the following conditional:

• s ∈ a ⟶ s ∈ c

Use that to derive a ⊆ c. Now you can discharge the first assumption made by introducing the following conditional:

• (a ⊆ b ∧ b ⊆ c) ⟶ a ⊆ c

Use universal introduction on the three names. The name a becomes the variable x, b becomes the variable y and c becomes the variable z.

That should complete the proof.