SC Kleene Metamatatiğe girişte egzersiz * 148 için gerekli yardım.

Question

İzin Vermek $x$ değişken ol, $A(x)$ bir formül ve $y$ farklı bir değişken $x$ hangisi için ücretsiz $x$ içinde $A(x)$ ve özgür olmuyor $A(x)$.

İzin Vermek $Q(x)$ olmak: $\forall y [y<x \Rightarrow \lnot A(y)]$.

Bunu kanıtlamak için biraz yardıma ihtiyacım var $Q(x), \lnot A(x) \vdash Q(x')$ Kleene sistemini kullanarak (burada 'halefi var).

Bu alıştırmanın son kısmıdır * 148 (doğal sayıların ilk bölümü için en az sayı ilkesi), sayfa 190, Kleene'nin Metamatematiğe Giriş. Kleene'ye göre bu kullanılmalıdır:$\vdash a\le b \sim a \lt b'$

Teşekkürler

Answer 1

Aşağıdaki lemmayı kullanacağız: $y < x' \rightarrow y = x \vee y < x$. Bunu birkaç yolla türetebilirsiniz: örneğin, bir tümevarım argümanı yoluyla veya daha önce belirlenmiş 139 ve 141'e başvurarak.

Doğal bir kesinti kanıtı vereceğim $Q(x), \neg A(x) \vdash Q(x')$. Kullandığım sistem Kleene'ninkine tam olarak uymayabilir, ancak aralarında çeviri yapmanıza yetecek kadar benzemeli. Eğer sorun çıkarırsa bana haber ver.

İstediğiniz sonuç $\forall y. y < x' \rightarrow \neg A(y)$İspatınıza dört varsayımla başlayabilir ve bir çelişki için çalışabilirsiniz.

1. Varsaymak $\forall y. y < x \rightarrow \neg A(y)$ - yani $Q(x)$
2. Varsaymak $\neg A(x)$.
3. Varsaymak $y < x'$.
4. Varsaymak $A(y)$.
5. Sahip olmak $y < x' \rightarrow y = x \vee y < x$ (yukarıda tartışılan lemma tarafından).
6. Sahip olmak $y = x \vee y < x$ (5 ve 1'den çıkarım eliminasyonu kullanılarak).
7. Varsaymak $y=x$.
8. Sahip olmak $A(x)$ (ikame kullanılarak 7 ve 4'ten).
9. Bir çelişki var (8 ve 2'den).
10. Sahip olmak $y = x \rightarrow \neg A(y)$ (çelişki ile 7-9 arası, varsayımı boşa çıkararak 7).
11. Sahip olmak $y<x \rightarrow \neg A(y)$ (1'den evrensel eleme ile).
12. Sahip olmak $\neg A(y)$ (6, 10, 11'den ayrılma eliminasyonu kullanılarak).
13. Bir çelişki var (12 ve 4'ten).
14. Sahip olmak $\neg A(y)$ (4-13'ten olumsuzluğa giriş, varsayımın kaldırılmasıyla 4).
15. Sahip olmak $y < x' \rightarrow \neg A(y)$ (3 ila 14 arasında, dolaylı olarak giriş, varsayımın çıkarılmasıyla).
16. Sahip olmak $\forall y. y<x' \rightarrow \neg A(y)$(evrensel girişle 15'ten), QED .