SC Kleene Introduction to metamathematics의 운동 * 148에 필요한 도움.

Question

허락하다 $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')$ Kleene의 시스템을 사용합니다 (여기서 '는 후속 작업입니다).

이것은 Kleene 's Introduction to metamathematics의 190 페이지에있는 * 148 (자연수의 초기 세그먼트에 대한 최소 수 원칙)의 마지막 연습입니다. Kleene에 따르면 다음을 사용해야합니다.$\vdash a\le b \sim a \lt b'$

감사

Answer 1

다음과 같은 기본형을 사용할 것입니다. $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)$, 네 가지 가정으로 증명을 시작하고 모순을 향해 작업 할 수 있습니다.

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에 의해 3-14에서).
16. 있다 $\forall y. y<x' \rightarrow \neg A(y)$(유니버설 소개로 15에서), QED .