0

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?

enter image description here

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. – Graham Kemp Nov 30 '18 at 7:06
2

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 ⊆ c) ⟶ a ⊆ c)           ∀I
|  |  ∀y ∀z ((a ⊆ b ∧ b ⊆ c) ⟶ a ⊆ c)           ∀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. – jessie Nov 30 '18 at 5:10
1

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.

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.