Rozstrzygalność teorii logicznych

Zad. 1

Sygnatura składa się z jednego jednoragumentowego symbolu funkcyjnego $f$ . Niech $\psi$ będzie zdaniem $\forall x(f(f(x))=x\land \lnot f(x)=x)$ .

Udowodnić, że teoria $\{\varphi\in FO~|~\psi\models\varphi\}$ jest rozstrzygalna.
Udowodnić, że teoria $\{\varphi\in FO~|~\psi\models\varphi\}$ należy do PSPACE.

Zad. 2

Sygnatura jest pusta. Niech $\Gamma$ będzie zbiorem zdań $\{\forall x_1\dots x_n\exists x_{n+1}(\bigwedge_{i=1}^n\lnot x_{n+1}=x_i)~|~n\in\mathbb{N}\}$ .

Udowodnić, że teoria $\{\varphi\in FO~|~\Gamma\models\varphi\}$ jest rozstrzygalna.
Udowodnić, że teoria $\{\varphi\in FO~|~\Gamma\models\varphi\}$ należy do PSPACE.

Zad. 3

Udowodnić, że następujący problem decyzyjny jest nierozstrzygalny:
Dane:Formuła $\varphi$ logiki pierwszego rzędu
Pytanie:Czy $\varphi$ ma wyłącznie skończone modele?

Zad. 4

Wyjaśnić, jak można pogodzić ze sobą Zadania 2 i 3.

Zad. 5

Czy teoria pierwszego rzędu ciała liczb zespolonych $\mathfrak{C}=\langle\mathbb{C},+,\cdot,0,1\rangle$ jest rozstrzygalna?

Odpowiedź

TAK

Żeby rozstrzygnąć zdanie o liczbach zespolonych, traktuje się je jako pary liczb rzeczywistych.

Czyli kwantyfikator $\exists z_i$ zastępujemy $\exists x_iy_i$ , stałą $0$ przez parę $0,0$ , stałą $1$ przez parę $0,0$ , sumę $z_i+z_j$ przez parę $x_i+x_j$ i $y_i+y_j$ , iloczyn $z_i\cdot z_j$ przez parę $x_i\cdot x_j-y_i\cdot y_j$ i $x_i\cdot y_j+x_j\cdot y_i.$ Równości zastępujmy przez koniunkcje dwóch równości: odpowiednio pierwszych i drugich elementów każdej z par.

Po takiej przeróbce otrzymane zdanie jest prawdziwe w $\mathfrak{R}=\langle\mathbb{R},+,\cdot,0,1\rangle$ wtedy i tylko wtedy, gdy zadnie wyjściowe było prawdziwe w $\mathfrak{C}=\langle\mathbb{C},+,\cdot,0,1\rangle$ .
Teoria liczb rzeczywistych jest rozstrzygalna na mocy twierdzenia Tarskiego, które jest w notatkach i było na wykładzie.

Informatyka MIMUW