Decidability of logical theories

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.