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)\).

  1. Udowodnić, że teoria \(\{\varphi\in FO~|~\psi\models\varphi\}\) jest rozstrzygalna.
  2. 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}\}\).

  1. Udowodnić, że teoria \(\{\varphi\in FO~|~\Gamma\models\varphi\}\) jest rozstrzygalna.
  2. 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?