EX 1

L’ensemble de formules suivant est-il satisfaisable ?

On note $(1),(2),(3)$ respectivement les formules précédentes.

Par factorisation de $(3)$, on dérive $P(f(c,b),f(c,b))\vee \neg Q(c^{\prime },a)$ pour toutes constantes $c,c^{\prime }\in \{a,b\}$

Puis, par factorisation avec $(1)$, on dérive $P(f(c,b),f(c,b))$ pour toute constante $c^{\prime }\in \{a,b\}$

Par ailleurs, par résolution de $(2)$, on dérive $\neg P(f(a,c^{\prime }),f(a,c^{\prime }))$ pour toute constante $c^{\prime }\in \{a,b\}$.

Donc avec $c^{\prime }=b,c=a$ dans les formules qui précèdent, on dérive par résolution $\mathrm{\perp }$.

Donc par correction de $Res+Fact$, on en déduit que l’ensemble est insatisfaisable.

NB : Notons que comme l’ensemble est insatisfaisable, il est nécéssaire de pouvoir en dériver $\mathrm{\perp }$, par complétude réfutationnelle de $Res+Fact$.

EX 2

1.

Faux, prendre la théorie des ordres denses (complète, cohérente, et même récursive), ou la théorie $Th(\mathbb{N})$ (théorie d’un modèle : cohérente et complète).

2.

Faux : prendre $Th(\mathbb{N})$ (théorie d’un modèle : complète, mais indécidable car contient $Q$).

3.

Vrai si la théorie est saturée (supposé dans le cours), puisqu’alors elle contient $\mathrm{\perp }$, et, partant, toutes les autres formules.

4.

Vrai :

M1 :

si on avait un modèle $M$ fini de $Q$, le graphe de la fonction “successeur” serait de la forme

avec

• $k\ne 0$ puisque $0$ n’est pas un successeur

mais alors on n’a plus l’injectivité du successeur, puisque $k=succ(n)=succ(k-1)$

M2 :

S’il existait un modèle fini $M$ de $Q$, par le principe des tiroirs : il existerait $p>n\in \mathbb{N}$ tel que :

mais alors, par injectivité du successeur :

absurde, puisque $0$ n’est pas un successeur.

5.

Faux : on pose

$T_1$ est

• incohérente
• complète
• décidable

mais $Q\subseteq T_1$ (et $Q$ est engendrée par un ensemble fini d’axiomes), mais $Q$ n’est pas décidable.

6.

Vrai : on exécute les deux machines de Turing en parallèle.

7.

On aurait envie de dire : “Vrai : deuxième théorème d’incomplétude de Gödel.”

Mais c’est plutôt “on ne sait pas” : voir l’explication dans cette partie du cours de $𝜆$-calcul de Jean Goubault-Larrecq.

Problème

1.

a).

on utilise l’axiome $(1)$ pour montrer que $s(0)\ge s(0)$, d’où (par $(5)$) $s(0)\ge 0$.

Et comme d’après $(7)$ : $0\ge s(0)$, il vient par $(2)$ que $0=s(0)$

b).

Par $(9)$ : $s(p(0))=0=s(0)$ (avec ce qui précède), donc $p(0)\ge 0$ (par $(4)$), et d’après $(7)$ et $(2)$ : $p(0)=0$

c).

Montrons que :

En effet :

D’après $(5)$, comme $s(x)\ge s(x)$ (par $(1)$), on conclut.

Montrons que $\forall x.p(s(x))=x$

On sait que $\forall x.p(s(x))\ge x$ avec $(9)$ et $(5)$.

Par $(2)$, il suffit donc de montrer que $\forall x.x\ge p(s(x))$.

Or, c’est équivalent à montrer, par $(5)$, que $\forall x.s(x)\ge s(x)$, ce qui est vrai par $(1)$.

d).

Par $(4)$ et $\forall x.p(s(x))=x$, on en déduit que $\forall x,y.(x\ge s(y)\leftrightarrow p(x)\ge y)$.

On conclut, avec $(5)$, que $\forall x,y.x\ge y\leftrightarrow (x=y\vee p(x)\ge y)$.

e).

Montrons que :

En effet :

On conclut avec $(4)$ et $\forall x.s(x)\ge x$.

Par $\forall x.x\ge p(x)$ et par $\forall x,y.x\ge y\leftrightarrow (x=y\vee p(x)\ge y)$, on en déduit que

f).

Par $\forall x,y.x\ge y\leftrightarrow p(x)\ge p(y)$ et $(1)$, il suffit de montrer que $p(y)\ge p(x)\wedge p(x)\ngeqq p(y)\leftrightarrow y\ge s(x)\wedge x\ne 0$

Or, par $(4)$ et $(5)$, $p(y)\ge p(x)\leftrightarrow y\ge x\leftrightarrow y\ge s(x)\vee x=y$

Donc

Réciproquement, on utilise $(1)$ et a).

2.

$\mathbb{Z}\cup \{+\infty \}$ où $0$ est interprété comme $+\infty$ en est un modèle.

3.

Non, démonstration analogue à EX 2.4)

4.

On simplifie les formules avec 1. c)

5.

En enlevant l’axiome 7, $\mathbb{Z}$ est un modèle.

Pour montrer que

on exhibe un modèle de $T$ qui ne satisfait pas $𝜙$.

Donc pour montrer que $T$ est incomplète, on veut montrer que

• $T⊭𝜙$
• $T⊭\neg 𝜙$, i.e. $T\models 𝜙$

Donc on exhibe deux modèles de $T$ : l’un ne vérifiant pas $𝜙$, l’autre vérifiant $𝜙$.

• Pour l’axiome 8 : on prend un modèle avec un seul élément

• Pour l’axiome 9 : on prend $\mathbb{Z}\cup \{+\infty \}$, où $p=s=succ$