Teoria K

Note

Ha come sintassi delle FBF con solo $\neg ,\Rightarrow$. Utilizza gli stessi assiomi della teoria L assieme a:

$$\text{Ax}:\{\begin{array}{l}(\forall xA(x))\Rightarrow A[t/x]\text{dove }t\text{ eˋ un termine libero per }x\\ \forall x(A\Rightarrow B)\Rightarrow (A\Rightarrow \forall xB)\end{array}$$

Inoltre ha come regole di inferenza:

1. Modus ponens $A,A\Rightarrow B{⊢}_{K}B$
2. Generalizzazione: $A(x){⊢}_K\forall xA(x)$

Diciamo $\Gamma {⊢}_{K}A$ se esiste $A_1,\cdots ,A_m$ tale che:

$$\Gamma {⊢}_K{A}_1,\Gamma \cup \{A_1\}{⊢}_K{A}_2,\cdots ,\Gamma \cup \{A_1,\cdots ,A_{m-1}\}{⊢}_K{A}_m$$

Dove ciascuna $A_i$ è assioma appartenente a $\Gamma \cup \{A_1,\cdots ,A_{i-1}\}$ oppure è ottenuta mediante una regola di inferenza da $\Gamma \cup \{A_1,\cdots ,A_{i-1}\}$.

Per il teorema di correttezza a completezza forte la teoria K è:

• Corretta: $\Gamma ⊢A\Rightarrow \Gamma \models A$
• Completa: $\Gamma \models A\Rightarrow \Gamma ⊢A$

Tip

La teoria K è indecidibile.

Se $\Gamma \ne \varnothing$, pensiamo a $\Gamma$ come degli assiomi di una teoria.

Teoria K con assiomi propri

Teoria con identità (uguaglianza)

Abbiamo bisogno di una lettera predicativa $E(x,y)$ che catturi la relazione di uguaglianza:

$$\Gamma =\{\begin{array}{l}\forall xE(x,x)\\ \forall x\forall y\left(E(x,y)\Rightarrow (A(x|x)\Rightarrow A(x|y/x)\right)\end{array}$$

In una teoria simile possiamo definire il concetto di esistenza unica:

$$\exists !xA(x)\equiv \exists x(A(x)\wedge \forall y(A(y)\Rightarrow E(x,y)))$$

Teoria con identità dei numeri naturali

Prima formulazione assiomi di Peano:

1. $0$ è un numero naturale
2. Se $x$ è un numero naturale, allora ne esiste un altro $S(x)$ detto successivo di $x$
3. $0\ne S(x)\forall x$
4. Se $S(x)=S(y)⟹x=y$
5. Principio di induzione: se $Q$ è una proprietà su $\mathbb{N}$ che soddisfa:

• $0$ soddisfa $Q$
• se ogni volta che $x$ soddisfa $Q$, anche $S(x)$ soddisfa $Q$ Allora tutti i naturali soddisfano $Q$.

Assiomi teoria dei numeri naturali

Abbiamo come lettere funzionali $f(x)=x+1,S(x,y)=x+y,P(x,y)=x\cdot y$ e come costante $0$:

$$\begin{array}{rlrl}& \forall x(\neg E(0,f(x)))& 0\ne S(x)\forall x& \\ & \forall x\forall y(E(f(x),f(y))\Rightarrow E(x,y))& S(x)=S(y)⟹x=y& \\ & \forall x(E(S(x,0),x))& x+0=x& \\ & \forall x\forall y(E(S(f(x),y),f((S(x,y)))))& (x+1)+y=(x+y)+1& \\ & \forall xE(P(x,0),0)& x\cdot 0=0& \\ & \forall x\forall y(E(P(x,f(y)),S(P(x,y),x)))& x\cdot (y+1)=x\cdot y+x& \\ & (A(0)\wedge \forall x(A(x)\Rightarrow A(f(x))))⟹\forall xA(x)& \text{Principio di induzione per }A& \end{array}$$

Primo teorema di incompletezza di Gödel

Note

Se $S$ è una teoria del primo ordine che contiene l’aritmetica ($S_1,\cdots ,S_n\in S$) e che sia consistente (cioè non produca sia $\phi$ che $\neg \phi$), allora esiste una FBF $\psi$ tale che né $\psi$ né $\neg \psi$ sono dimostrabili: $S/{⊢}_K\psi$ e $S/{⊢}_K\neg \psi$. Inoltre $\psi$ è un affermazione che è vera nella teoria dei numeri naturali.