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つの仮定から証明を開始し、矛盾に向けて取り組むことができます。

  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から)、QED