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