Требуется помощь с упражнением * 148 в SC Kleene Введение в метаматематику.

Aug 18 2020

Позволять $x$ быть переменной, $A(x)$ формула и $y$ переменная, отличная от $x$ что бесплатно для $x$ в $A(x)$ и не происходит бесплатно в $A(x)$.

Позволять $Q(x)$ быть: $\forall y [y<x \Rightarrow \lnot A(y)]$.

Мне нужна помощь в доказательстве этого $Q(x), \lnot A(x) \vdash Q(x')$ используя систему Клини (вот и преемник).

Это последняя часть упражнения * 148 (принцип наименьшего числа для начального сегмента натуральных чисел), страница 190 во введении Клини в метаматематику. По словам Клини, это следует использовать:$\vdash a\le b \sim a \lt b'$

благодаря

Ответы

2 Z.A.K. Aug 19 2020 at 04:44

Мы собираемся использовать следующую лемму: $y < x' \rightarrow y = x \vee y < x$. Это можно вывести несколькими способами: например, с помощью индукционного аргумента или просто апеллируя к ранее установленным 139 и 141.

Я дам доказательство естественной дедукции $Q(x), \neg A(x) \vdash Q(x')$. Система, которую я использую, может не точно соответствовать системе Клини, но должна быть достаточно похожа на нее, чтобы вы могли переводить между ними. Сообщите мне, если это доставит вам какие-либо проблемы.

Поскольку ваш желаемый вывод $\forall y. y < x' \rightarrow \neg A(y)$, вы можете начать доказательство с четырех предположений и продолжить работу в направлении противоречия.

  1. Предполагать $\forall y. y < x \rightarrow \neg A(y)$ - т.е. $Q(x)$
  2. Предполагать $\neg A(x)$.
  3. Предполагать $y < x'$.
  4. Предполагать $A(y)$.
  5. Есть $y < x' \rightarrow y = x \vee y < x$ (по рассмотренной выше лемме).
  6. Есть $y = x \vee y < x$ (от 5 до 1 с использованием исключения импликации).
  7. Предполагать $y=x$.
  8. Есть $A(x)$ (с 7 и 4 с заменой).
  9. Получили противоречие (с 8 и 2).
  10. Есть $y = x \rightarrow \neg A(y)$ (от 7-9 от противного, отклоняя предположение 7).
  11. Есть $y<x \rightarrow \neg A(y)$ (из 1 по универсальному исключению).
  12. Есть $\neg A(y)$ (из 6, 10, 11 с использованием исключения дизъюнкции).
  13. Получили противоречие (с 12 и 4).
  14. Есть $\neg A(y)$ (с 4-13 введением отрицания, снятием допущения 4).
  15. Есть $y < x' \rightarrow \neg A(y)$ (от 3 до 14 подразумевается введение, отклонение предположения 3).
  16. Есть $\forall y. y<x' \rightarrow \neg A(y)$(из 15 по всеобщему введению), КЭД .