Aiuto necessario con l'esercizio * 148 in SC Kleene Introduzione alla metamatematica.

Aug 18 2020

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

2 Z.A.K. Aug 19 2020 at 04:44

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.

  1. Assumere $\forall y. y < x \rightarrow \neg A(y)$ - es $Q(x)$
  2. Assumere $\neg A(x)$.
  3. Assumere $y < x'$.
  4. Assumere $A(y)$.
  5. Avere $y < x' \rightarrow y = x \vee y < x$ (dal lemma discusso sopra).
  6. Avere $y = x \vee y < x$ (da 5 e 1 utilizzando l'eliminazione dell'implicazione).
  7. Assumere $y=x$.
  8. Avere $A(x)$ (da 7 a 4 con sostituzione).
  9. Hanno una contraddizione (da 8 e 2).
  10. Avere $y = x \rightarrow \neg A(y)$ (da 7-9 per assurdo, annullando l'ipotesi 7).
  11. Avere $y<x \rightarrow \neg A(y)$ (da 1 per eliminazione universale).
  12. Avere $\neg A(y)$ (da 6, 10, 11 utilizzando l'eliminazione della disgiunzione).
  13. Hanno una contraddizione (da 12 e 4).
  14. Avere $\neg A(y)$ (da 4-13 per introduzione di negazione, scaricando l'assunzione 4).
  15. Avere $y < x' \rightarrow \neg A(y)$ (da 3-14 implicitamente introduzione, scaricando ipotesi 3).
  16. Avere $\forall y. y<x' \rightarrow \neg A(y)$(da 15 per introduzione universale), QED .