Проверка языка и логика Глава 15, вопрос 16, помощь

Вот посылка: ∀x∀y(x ⊆ y ↔️ ∀z(z ∈ x ⟶ z ∈ y)

Вот цель: ∀x∀y∀z((x ⊆ y ∧ y ⊆ z) ⟶ x ⊆ z)

Ваша предпосылка — это определение отношения подмножества. Ваша цель — свойство транзитивности. Вы должны распознать их, хотя знать это не обязательно для этой задачи.

В любом случае. Ваш очевидный первый шаг — настроить универсальное введение... и давайте сделаем условное введение, пока мы на нем. (Примечание. Некоторые средства проверки позволяют комбинировать эти шаги.)

|_ ∀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

Чтобы получить эквивалентность для этих трех утверждений подмножества, используйте универсальное исключение несколько раз.

Теперь это будут три универсальных квантификатора, поэтому примите другой произвольный термин, чтобы устранить и ввести универсальные кванторы по мере необходимости.

Затем все встречается в середине с дополнительным доказательством конструктивной дилеммы.

 |_ ∀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

Вот посылка: ∀x∀y(x ⊆ y ↔️ ∀z(z ∈ x ⟶ z ∈ y)

Вот цель: ∀x∀y∀z((x ⊆ y ∧ y ⊆ z) ⟶ x ⊆ z)

На естественном языке посылка гласит, что если множество x является подмножеством множества y, то для всех элементов z множества x эти элементы z также являются элементами множества y. Цель состоит в том, чтобы показать, что отсюда следует, что если множество x является подмножеством множества y и это множество y является подмножеством множества z, то множество x является подмножеством множества z.

Я объясню, как вы можете действовать.

Предпосылка определяет, что означает, что одно множество является подмножеством другого с точки зрения элементов этих множеств. Поскольку цель имеет три отношения подмножества, используйте универсальное исключение три раза, чтобы получить следующие три строки из предпосылки:

• а ⊆ б ↔️ s ∈ а ⟶ s ∈ б
• б ⊆ с ↔️ s ∈ б ⟶ s ∈ с
• а ⊆ с ↔️ s ∈ а ⟶ s ∈ с

В приведенном выше примере a, b и c — имена наборов, а s — имя элемента набора.

Сделайте предположение: a ⊆ b ∧ b ⊆ c

Это предшественница цели. Нам нужно вывести следствие: a ⊆ c

Используйте исключение союзов, чтобы разбить предположение на две строки:

• а ⊆ б
• б ⊆ в

Используйте условное исключение или modus ponens, чтобы вывести эти две строки:

• s ∈ а ⟶ s ∈ b
• s ∈ b ⟶ s ∈ c

Сделайте предположение: s ∈ a

Отсюда выводим s ∈ b, а из этого выводим s ∈ c.

Отмените это последнее предположение, введя следующее условное выражение:

• s ∈ а ⟶ s ∈ с

Используйте это, чтобы получить a ⊆ c. Теперь вы можете опровергнуть первое сделанное предположение, введя следующее условное выражение:

• (а ⊆ б ∧ б ⊆ в) ⟶ а ⊆ в

Используйте универсальное введение по трем именам. Имя a становится переменной x, b становится переменной y, а c становится переменной z.

Это должно завершить доказательство.