SCKleeneのメタ数学入門の演習* 148で必要なヘルプ。
Aug 18 2020
しましょう $x$ 変数であること、 $A(x)$ 式と $y$ とは異なる変数 $x$ これは無料です $x$ に $A(x)$ で無料で発生しません $A(x)$。
しましょう $Q(x)$ be: $\forall y [y<x \Rightarrow \lnot A(y)]$。
私はそれを証明するのにいくつかの助けが必要です $Q(x), \lnot A(x) \vdash Q(x')$ Kleeneのシステムを使用します(ここでは 'が後継です)。
これは、Kleeneのメタ数学入門の190ページの演習* 148(自然数の最初のセグメントの最小数の原則)の最後のビットです。Kleeneによると、これを使用する必要があります。$\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')$。私が使用しているシステムは、Kleeneのシステムに正確に対応していない可能性がありますが、それらの間で変換するのに十分なほど似ているはずです。それで問題が発生した場合はお知らせください。
あなたの望む結論は $\forall y. y < x' \rightarrow \neg A(y)$、4つの仮定から証明を開始し、矛盾に向けて取り組むことができます。
- 仮定する $\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から)、QED。