Aiuto necessario con l'esercizio * 148 in SC Kleene Introduzione alla metamatematica.
Permettere $x$ essere una variabile, $A(x)$ una formula e $y$ una variabile distinta da $x$ che è gratuito per $x$ in $A(x)$ e non si verifica gratuitamente in $A(x)$.
Permettere $Q(x)$ essere: $\forall y [y<x \Rightarrow \lnot A(y)]$.
Ho bisogno di aiuto per dimostrarlo $Q(x), \lnot A(x) \vdash Q(x')$ usando il sistema di Kleene (qui 'è il successore).
Questa è l'ultima parte dell'esercizio * 148 (principio del numero minimo per un segmento iniziale dei numeri naturali) pagina 190 nell'Introduzione alla metamatematica di Kleene. Secondo Kleene questo dovrebbe essere usato:$\vdash a\le b \sim a \lt b'$
Grazie
Risposte
Useremo il seguente lemma: $y < x' \rightarrow y = x \vee y < x$. Questo lo puoi derivare in diversi modi: ad esempio tramite un argomento di induzione, o semplicemente facendo appello a 139 e 141 stabiliti in precedenza.
Darò una prova di deduzione naturale $Q(x), \neg A(x) \vdash Q(x')$. Il sistema che uso potrebbe non corrispondere esattamente a quello di Kleene, ma dovrebbe assomigliare abbastanza da permetterti di tradurre tra di loro. Fammi sapere se questo ti dà problemi.
Poiché la tua conclusione desiderata è $\forall y. y < x' \rightarrow \neg A(y)$, puoi iniziare la prova con quattro presupposti e lavorare verso una contraddizione.
- Assumere $\forall y. y < x \rightarrow \neg A(y)$ - es $Q(x)$
- Assumere $\neg A(x)$.
- Assumere $y < x'$.
- Assumere $A(y)$.
- Avere $y < x' \rightarrow y = x \vee y < x$ (dal lemma discusso sopra).
- Avere $y = x \vee y < x$ (da 5 e 1 utilizzando l'eliminazione dell'implicazione).
- Assumere $y=x$.
- Avere $A(x)$ (da 7 a 4 con sostituzione).
- Hanno una contraddizione (da 8 e 2).
- Avere $y = x \rightarrow \neg A(y)$ (da 7-9 per assurdo, annullando l'ipotesi 7).
- Avere $y<x \rightarrow \neg A(y)$ (da 1 per eliminazione universale).
- Avere $\neg A(y)$ (da 6, 10, 11 utilizzando l'eliminazione della disgiunzione).
- Hanno una contraddizione (da 12 e 4).
- Avere $\neg A(y)$ (da 4-13 per introduzione di negazione, scaricando l'assunzione 4).
- Avere $y < x' \rightarrow \neg A(y)$ (da 3-14 implicitamente introduzione, scaricando ipotesi 3).
- Avere $\forall y. y<x' \rightarrow \neg A(y)$(da 15 per introduzione universale), QED .