Logika dla informatyków/Ograniczenia logiki pierwszego rzędu

Link z wykladu 8 do tw. 4.13. Nazwa linku "Cantoro"

Ograniczenia logiki pierwszego rzędu

Ten rozdział poświęcony jest ograniczeniom, którym podlega język logiki pierwszego rzędu. Okazuje się, że nie każde pojęcie da się w nim wyrazić, a także, że są pojęcia, które dają się wyrazić, ale odpowiednie zdanie lub formuła z konieczności musi być skomplikowane. Rozważania w tym rozdziale będziemy prowadzić przy założeniu, że w sygnaturze występują wyłącznie symbole relacyjne. Wyniki dają się zastosować do sygnatur z symbolami funkcyjnymi, ale wymaga to zakodowania wszystkich funkcji jako relacji.

Zaczniemy od miary skomplikowania formuł, która będzie przydatna w dalszym ciągu.

Definicja 4.1

Rangę kwantyfikatorową Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle QR\var(\varphi)} formuły Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \var\varphi} definiujemy jak następuje:

• $QR\bot =QRt_{1}=t_{2}=QRr(t_{1},\dots ,t_{k}))=0$ dla dowolnych termów $t_{1},\dots ,t_{k}$ oraz $r\in \Sigma _{k}^{R}$.
• Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle QR(\var\varphi\to \psi )=\max(QR(\var\varphi ),QR(\psi ) )} .
• Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle QR(\forall x\var\varphi )=1+QR(\var\varphi )} .

Intuicyjnie $QR$ to głębokość zagnieżdżenia kwantyfikatorów w formule. Jest to jedna z wielu możliwych miar stopnia komplikacji formuły Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \var\varphi} . Parametr ten ma następujące znaczenie: jeśli struktura ${\mathfrak {A}}$ ma $n$elementów, to pesymistyczny czas sprawdzenia, czy dla zdania Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \var\varphi} zachodzi Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \mathfrak A\models \var\varphi} jest asymptotycznie proporcjonalny do Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle n^{QR(\var\varphi )}} , gdy użyjemy naturalnego algorytmu do wykonania tego zadania, który dla każdego kwantyfikatora w formule przegląda wszystkie elementy struktury.

Teraz możemy wyjaśnić, dlaczego nie dopuszczamy symboli funkcyjnych w sygnaturze. Otóż ich obecność zakłóca potrzebne nam własności funkcji $QR$. Tytułem przykładu, formuła $R(x,f(f(x)))$ jest atomowa i jej ranga kwantyfikatorowa powinna wynosić $0$. Tymczasem gdy $f$ będziemy reprezentować w strukturze jako dwuargumentową relację $F$, ta sama formuła przybierze postać $\exists y\exists zF(x,y)\land F(y,z)\land R(x,z))$, której ranga kwantyfikatorowa wynosi 2. Twierdzenia, których dalej dowodzimy, odwołują się do wartości $QR$ zdefiniowanych powyżej dla logiki bez symboli funkcyjnych. To właśnie jest przyczyna, dla której funkcje wykluczamy z rozważań.

Charakteryzacja Fraïssé

Definicja 4.2

Jeśli ${\mathfrak {A}}$ jest strukturą relacyjną oraz $\emptyset \neq B\subseteq A$, to struktura ${\mathfrak {A}}_{|B}$ tej samej sygnatury $\Sigma$ co ${\mathfrak {A}}$, nazywana podstrukturą indukowaną przez $B$, w ${\mathfrak {A}}$, ma nośnik $B$, zaś dla każdego $r\in \Sigma _{n}^{R}$

$r^{{\mathfrak {A}}_{|B}}=r^{\mathfrak {A}}\cap B^{n}$.

Definicja 4.3

Niech ${\mathfrak {A}},B$ będą strukturami relacyjnymi tej samej sygnatury $\Sigma$, ponadto niech $A'\subseteq A$ i $B'\subseteq B$. Jeśli funkcja $h:A'\to B'$ jest izomorfizmem podstruktur indukowanych $h:{\mathfrak {A}}_{|A'}\cong {\mathfrak {B}}_{|B'}$, to mówimy, że $h$ jest częściowym izomorfizmem z ${\mathfrak {A}}$ w ${\mathfrak {B}}$. Jego dziedzina to $dom(h)=A'$, a obraz to $rg(h)=B'$.

Na zasadzie konwencji umawiamy się, że $\emptyset$ jest częściowym izomorfizmem z ${\mathfrak {A}}$ w ${\mathfrak {B}}$ o pustej dziedzinie i pustym obrazie.

Dla dwóch częściowych izomorfizmów $g,h$ z ${\mathfrak {A}}$ w ${\mathfrak {B}}$ piszemy $g\subseteq h$ gdy $dom(g)\subseteq dom(h)$ oraz $g(a)=h(a)$ dla wszystkich $a\in dom(g)$, to jest wtedy, gdy $g$ jest zawarte jako zbiór w $h$.

Definicja 4.4

Niech $m$ będzie dodatnią liczbą naturalną. Dwie struktury relacyjne tej samej sygnatury są $m$-izomorficzne, co oznaczamy ${\mathfrak {A}}\cong _{m}{\mathfrak {B}}$, gdy istnieje rodzina $\{I_{n}|n\leq m\}$, w której każdy $I_{n}$ jest niepustym zbiorem częściowych izomorfizmów z ${\mathfrak {A}}$ w ${\mathfrak {B}}$, oraz spełniająca następujące dwa warunki:

• Tam Dla każdego $h\in I_{n+1}$ oraz każdego $a\in$ istnieje takie $g\in I_{n}$, że $h\subseteq g$ oraz $a\in dom(g)$.
• Z powrotem Dla każdego $h\in I_{n+1}$ oraz każdego $b\in B$ istnieje takie $g\in I_{n}$, że $h\subseteq g$ oraz $b\in rg(g)$.

Samą rodzinę $\{I_{n}|n\leq m\}$ nazywamy wówczas $m$-izomorfizmem struktur ${\mathfrak {A}}$ i ${\mathfrak {B}}$, co oznaczamy $\{I_{n}|n\leq m\}:{\mathfrak {A}}\cong _{m}{\mathfrak {B}}$.

Nieformalne wyjaśnienie jest takie: $I_{n}$ to zbiór częściowych izomorfizmów, które mogą być rozszerzone $n$-krotnie o dowolne elementy w dziedzinie i obrazie, a kolejne rozszerzenia leżą w $I_{n-1},\dots ,I_{0}$.

Definicja 4.5

Dwie struktury relacyjne tej samej sygnatury są skończenie izomorficzne, symbolicznie ${\mathfrak {A}}\cong _{fin}{\mathfrak {B}}$, gdy istnieje rodzina $\{I_{n}|n\in \omega \}$, taka że każda podrodzina $\{I_{n}|n\leq m\}$ jest $m$-izomorfizmem.

Jeśli $\{I_{n}|n\leq m\}$ ma powyższe własności, to piszemy $\{I_{n}|n\leq m\}:{\mathfrak {A}}\cong _{fin}{\mathfrak {B}}$, a samą rodzinę nazywamy skończonym izomorfizmem.

Fakt 4.6

• Jeśli ${\mathfrak {A}}\cong {\mathfrak {B}}$, to ${\mathfrak {A}}\cong _{fin}{\mathfrak {B}}$.
• Jeśli ${\mathfrak {A}}\cong _{fin}{\mathfrak {B}}$ oraz nośnik math>\mathfrak A</math> jest zbiorem skończonym, to ${\mathfrak {A}}\cong {\mathfrak {B}}$.

Dowód

Definicja 4.7

Dwie struktury ${\mathfrak {A}}$ i ${\mathfrak {B}}$ tej samej sygnatury są elementarnie równoważne, co zapisujemy symbolicznie ${\mathfrak {A}}\equiv {\mathfrak {B}}$, gdy dla każdego zdania $\varphi$ logiki pierwszego rzędu nad tą samą sygnaturą, Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \mathfrak A\models\var\varphi} wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \mathfrak B\models\var\varphi} .

Dwie struktry ${\mathfrak {A}}$ i ${\mathfrak {B}}$ tej samej sygnatury są $m$-elementarnie równoważne, symbolicznie ${\mathfrak {A}}\equiv _{m}{\mathfrak {B}}$, gdy dla każdego zdania Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \var\varphi} logiki pierwszego rzędu nad tą samą sygnaturą, o randze kwantyfikatorowej nie przekraczającej $m$, zachodzi Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \mathfrak A\models\var\varphi} wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \mathfrak B\models\var\varphi} .

Fakt 4.8

${\mathfrak {A}}\cong _{f}in{\mathfrak {B}}$ wtedy i tylko wtedy, gdy dla każdego naturalnego $m$ zachodzi ${\mathfrak {A}}\cong _{m}{\mathfrak {B}}$.

Dowód

Wynikanie z lewej do prawej jest oczywiste. Załóżmy teraz, że dla każdego $m$ istnieje rodzina $\{I_{n}^{m}|n\leq m\}$ spełniająca warunki z definicji relacji $\cong _{m}$. Rozważmy rodzinę $\{J_{n}|n\in \omega \}$ gdzie $J_{n}=\bigcup _{m\in \omega }I_{n}^{m}$. Bezpośrednie sprawdzenie pokazuje natychmiast, że spełnia ona warunki definicji relacji $\cong _{fin}$.

Twierdzenie 4.9

Niech $\Sigma$ będzie dowolną sygnaturą relacyjną zawierającą skończenie wiele symboli, oraz niech ${\mathfrak {A}},{\mathfrak {B}}$ będą dowolnymi strukturami nad $\Sigma$.

• Dla każdego $m\in \mathbb {N}$ zachodzi równoważność: ${\mathfrak {A}}\cong _{m}{\mathfrak {B}}$ wtedy i tylko wtedy, gdy ${\mathfrak {A}}\equiv _{m}{\mathfrak {B}}$.
• ${\mathfrak {A}}\cong _{fin}{\mathfrak {B}}$ wtedy i tylko wtedy, gdy ${\mathfrak {A}}\equiv {\mathfrak {B}}$.

Dowód

Jest oczywiste, że druga równoważnośc wynika z pierwszej. Pierwszą z kolei udowodnimy tylko z lewej do prawej strony. Dowód w stronę przeciwną jest bardziej zawiły technicznie, a w dodatku ta implikacja jest rzadko używana w praktyce. Wyraża za to istotną z metodologicznego punktu widzenia informację: jeśli dwie struktury są ($m$- )elementarnie równoważne, to fakt ten można na pewno udowodnić posługując się metodą Fraïssé, choć oczywiście nie ma gwarancji, że będzie to metoda najprostsza.

Ustalmy $m\in \mathbb {N}$. Dowód tego, że z ${\mathfrak {A}}\cong _{m}{\mathfrak {B}}$ wynika ${\mathfrak {A}}\equiv _{m}{\mathfrak {B}}$ sprowadza się do wykazania następującego faktu za pomocą indukcji ze względu na budowę Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \var\varphi} :

\begin{quote}Niech Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \{I_n | n\leq m\''} będzie rodziną o której mowa w definicji ${\mathfrak {A}}\cong _{m}{\mathfrak {B}}$, niech Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \var\varphi} będzie formułą o co najwyżej $r$ zmiennych wolnych (bez utraty ogólności niech będą to $x_{1},\dots ,x_{r}$ ) i spełniającą Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle QR(\var\varphi )\leq n\leq m} oraz niech $g\in I_{n}$. Wówczas dla dowolnych $a_{1},\dots ,a_{r}\in dom(g)$ następujące dwa warunki są równoważne:

Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \mathfrak A,x_1:a_1,\dots,x_r:a_r\models\var\varphi}
Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \mathfrak B,x_1:g(a_1 ),\dots,x_r:g(a_r )\models\var\varphi} .\end{quote}

Dla formuł atomowych powyższa teza wynika wprost z faktu, że $g$ jest częściowym izomorfizmem (przypomnijmy że w sygnaturze nie ma symboli funkcyjnych i co za tym idzie jedynymi termami są zmienne).

Gdy Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \var\varphi} ma postać $\psi \to \xi$, to mamy następujący ciąg równoważnych warunków:

• ${\mathfrak {A}},x_{1}:a_{1},\dots ,x_{r}:a_{r}\models \psi \to \xi$

• ${\mathfrak {A}},x_{1}:a_{1},\dots ,x_{r}:a_{r}\not \models \psi$ lub ${\mathfrak {A}},x_{1}:a_{1},\dots ,x_{r}:a_{r}\models \xi$

• ${\mathfrak {A}},x_{1}:g(a_{1}),\dots ,x_{r}:g(a_{r})\not \models \psi$ lub ${\mathfrak {A}},x_{1}:g(a_{1}),\dots ,x_{r}:g(a_{r})\models \xi$

• ${\mathfrak {A}},x_{1}:g(a_{1}),\dots ,x_{r}:g(a_{r})\models \psi \to \xi$,

przy czym druga równoważność wynika z założenia indukcyjnego, a pierwsza i trzecia z definicji semantyki.

Gdy Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \var\varphi} ma postać $\forall x\psi$, to, jako że Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle x_{r+1}\notin FV(\var\varphi )} i co za tym idzie $\models (\forall x\psi )\leftrightarrow \forall x_{r+1}\psi (x_{r+1}/x)$ (patrz Fakt #alfa-konw ), możemy bez utraty ogólności założyć, że Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \var\varphi} ma postać $\forall x_{r+1}\psi$. Z założenia Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle QR(\var\varphi )\leq n} wynika, że $QR(\psi )\leq n-1$. Mamy teraz następujący ciąg równoważnych warunków:

• Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle (\mathfrak A,x_1:a_1,\dots,x_r:a_r )\models\var\varphi}

• Dla każdego $a\in A$ zachodzi$({\mathfrak {A}},x_{1}:a_{1},\dots ,x_{r}:a_{r},x_{r+1}:a)\models \psi$

• Dla każdego $a\in A$ istnieje takie $h\in I_{n-1}$, że $g\subseteq h$, $a\in dom(h)$ oraz $({\mathfrak {A}},x_{1}:a_{1},\dots ,x_{r}:a_{r},x_{r+1}:a)\models \psi$

• Dla każdego $a\in A$ istnieje takie $h\in I_{n-1}$, że $g\subseteq h$, $a\in dom(h)$ oraz $({\mathfrak {B}},x_{1}:g(a_{1}),\dots ,x_{r}:g(a_{r}),x_{r+1}:h(a))\models \psi$

• Dla każdego $b\in B$ istnieje takie $h\in I_{n-1}$, że $g\subseteq h$, $b\in rg(h)$ oraz $({\mathfrak {B}},x_{1}:g(a_{1}),\dots ,x_{r}:g(a_{r}),x_{r+1}:b)\models \psi$

• Dla każdego $b\in B$ zachodzi $({\mathfrak {B}},x_{1}:g(a_{1}),\dots ,x_{r}:g(a_{r}),x_{r+1}:b)\models \psi$

• Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle (\mathfrak B,x_1:g(a_1 ),\dots,x_r:g(a_r ) )\models\var\varphi} .

Równoważności druga i czwarta zachodzą na mocy warunków Tam i Z powrotem, trzecia na mocy założenia indukcyjnego, a pozostałe na mocy definicji spełniania.

Pokażemy teraz pierwszy przykład inherentnego ograniczenia logiki pierwszego rzędu.

Fakt 4.10

Jeśli ${\mathfrak {A}},{\mathfrak {B}}$ są dwoma skończonymi liniowymi porządkami o mocach większych niż $2^{m}$, to ${\mathfrak {A}}\equiv _{m}{\mathfrak {B}}$.

Dowód

Bez utraty ogólności możemy założyć, że $A=\{0,\dots ,N\}$, $B=\{0,\dots ,M\}$, przy czym $2^{m}<N\leq M$, a porządek jest porządkiem naturalnym. Dowód przeprowadzamy wykorzystując Twierdzenie #fraisse, czyli w istocie wykazujemy, że ${\mathfrak {A}}\cong _{m}{\mathfrak {B}}$.

Dla danego $k\leq m$ określmy "odległość" $d_{k}$ pomiędzy elementami naszych struktur jak następuje:

Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle d_k(a,b) = \begin{cases}|b-a| & \text{\ jeśli } |b-a|< 2^k \\\infty & \text{\ jeśli } wpp.\end{cases}}

Niech $I_{k}$ dla $k\leq m$ będzie zbiorem wszystkich częściowych izomorfizmów $g$ z ${\mathfrak {A}}$ w ${\mathfrak {B}}$ takich, że $\{\langle 0,0\rangle ,\langle N,M\rangle \}sbseteqg$ oraz $d_{k}(a,b)=d_{k}(g(a),g(b))$ dla wszystkich $a,b\in dom(g)$. Oczywiście $I_{k}\neq \emptyset$ bo $\{\langle 0,0\rangle ,\langle N,M\rangle \}\in I_{k}$.

Pokazujemy własność Tam dla rodziny $\{I_{k}|k\leq m\$. Niech $g\in I_{k+1}$. Niech $a\in \{0,\dots ,N\}$. Mamy wskazać w $I_{k}$ częściowy izomorfizm $h\supseteq g$ taki, że $a\in dom(h)$.

Rozróżniamy dwa przypadki:

1. Jeśli istnieje takie $b\in dom(g)$, że $d_{k}(a,b)<\infty$, to w $B$ jest dokładnie jeden element $a'$, który jest tak samo położony względem $g(b)$ jak $a$ względem $b$, oraz spełnia $d_{j}(a',g(b))=d_{j}(a,b)$. Kładziemy wówczas $h(a):=a'$ i $h$ jest wtedy częściowym izomorfizmem zachowującym odległości $d_{j}$.
2. Jeśli natomiast takiego $b$ nie ma, to niech $a'<a<a''$, gdzie $a',a''$ są najbliższymi $b$elementami po lewej i po prawej, które należą do $dom(g)$. Wówczas $d_{j}(a',a)=d_{j}(a,a'')=\infty$, co w myśl definicji $d_{j}$ oznacza, że $d_{j+1}(a',a'')=\infty$. Zatem na mocy założenia indukcyjnego także $d_{j+1}(g(a'),g(a''))=\infty$. Istnieje więc $g(a')<b<g(a'')$ takie, że Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle {d_j(g(a' ),b )=d_j(b,g(a'' ) )=\infty} , i wówczas kładąc $h(a):=b$uzyskujemy żądane rozszerzenie.

Przykład powyższy wskazuje na kilka istotnych ograniczeń logiki pierwszego rzędu. Po pierwsze, nie da się żadnym zdaniem zdefiniować nawet tak prostego pojęcia jak "porządek liniowy o parzystej liczbie elementów", i to bez względu na to, jak byśmy je rozumieli dla modeli nieskończonych. Istotnie, zdanie które miałoby definiować taką własność musiałoby mieć jakąś rangę kwantyfikatorową, powiedzmy $q$. Jednak w myśl poprzedniego twierdzenia, porządki o mocach $2^{q}+1$ i $2^{q}+2$ są $q$-elementarnie równoważne i nasze hipotetyczne zdanie jest albo prawdziwe w obu, albo fałszywe w obu, podczas gdy powinno być w jednym fałszywe, a w drugim prawdziwe.

Drugim ograniczeniem jest fakt, że każda specyfikacja porządku liniowego o mocy $n$ w logice pierwszego rzędu musi z konieczności mieć rangę kwantyfikatorową co najmniej $\log _{2}n$, a więc sugeruje algorytm sprawdzenia, czy dany obiekt mocy $m$ istotnie spełnia tę specyfikację, którego czas działania ma rząd wielkości $m^{\log _{2}n}$, co jest wynikiem fatalnym.\footnote{Na szczęście znamy lepsze algorytmy wykonujące to zadanie.} Bierze się to stąd, że prawdziwość zdania o randze kwantyfikatorowej $q$ sprawdza się w danej skończonej strukturze za pomocą $q$ zagnieżdżonych pętli, z których każda przegląda cały nośnik struktury i odpowiada jednemu kwantyfikatorowi.

Gra Ehrenfeuchta

Charakteryzacja Fraïssé jest dość skomplikowana i odpychająca w bezpośrednim użyciu. W praktyce jej popularność ogromnie zwiększyło podanie przez Andrzeja Ehrenfeuchta jej równoważnego opisu w terminach dwuosobowej gry, którą teraz zdefiniujemy. Gra ta doskonale sprawdza się w rozumowaniach intuicyjnych. Praktyczne doświadczenie wskazuje, że próby napisania bardzo formalnego dowodu przy użyciu gry kończą się zwykle wskazaniem rodziny zbiorów częściowych izomorfizmów w duchu Fraïssé.

Niech $\Sigma$ będzie sygnaturą relacyjną i niech ${\mathfrak {A}},{\mathfrak {B}}$ będą strukturami sygnatury $\Sigma$.

Dla uproszczenia zakładamy, że $A\cap B=\emptyset$. h

Definicja 4.11

Definicja powyższa dopuszcza powtarzanie ruchów przez obu graczy, czyli wybieranie elementów, które poprzednio były już wybrane. Jest to dogodne, gdyż upraszcza definicję. Gdybyśmy bowiem zakazali tego, to albo niemożliwe byłoby rozegranie gry $G_{m}({\mathfrak {A}},{\mathfrak {B}})$, gdy choć jedna ze struktur ma moc mniejszą niż $m$, albo trzeba by było wprowadzić w definicji specjalny warunek służący do rozstrzygania zwycięstwa w sytuacjach, gdy brak możliwości dalszych ruchów.

W praktyce jednak w dowodach prawie nigdy nie rozpatruje się takich ruchów, gdyż jest oczywiste, że wykonanie takiego posunięcia przez gracza I nie przybliża go do zwycięstwa, zaś gdy wykona je gracz II mimo że nie zrobił tego gracz I, powoduje to jego natychmiastową przegraną.

Twierdzenie 4.12

• Gracz II ma strategię wygrywającą w grze $G_{m}({\mathfrak {A}},{\mathfrak {B}})$ wtedy i tylko wtedy, gdy ${\mathfrak {A}}\cong _{m}{\mathfrak {B}}$.
• Gracz II ma dla każdego $m$ strategię wygrywającą w grze $G_{m}({\mathfrak {A}},{\mathfrak {B}})$ wtedy i tylko wtedy, gdy ${\mathfrak {A}}\cong _{fin}{\mathfrak {B}}$.

Dowód

Ćwiczenie.

Poniższe twierdzenie ilustruje, w jaki sposób gra może zostać wykorzystana dla wskazania ograniczeń możliwości logiki pierwszego rzędu.

Twierdzenie 4.13

Jeśli ${\mathfrak {A}}=\langle A,\leq ^{\mathfrak {A}}\rangle$ i ${\mathfrak {B}}=\langle B,\leq ^{\mathfrak {B}}\rangle$ są dwoma porządkami liniowymi, gęstymi, bez elementu pierwszego i ostatniego, to ${\mathfrak {A}}\equiv {\mathfrak {B}}$.

Dowód

W myśl Twierdzenia #ehrenfeucht należy pokazać, że dla każdego $m$ gracz II ma strategię wygrywającą w grze $G_{m}({\mathfrak {A}},{\mathfrak {B}})$. Opiszemy teraz tę strategię. Jej postać nie zależy od liczby rund do rozegrania. Pokażemy też, że jeśli po zakończeniu poprzedniej rundy warunek wygrywający dla gracza II był spełniony, to po wykonaniu ruchu zgodnie ze wskazaną strategią pozostanie on nadal spełniony. Wówczas na mocy zasady indukcji po rozegraniu dowolnej ilości rund, w których gracz II będzie się stosował do tej strategii, pozostanie on zwycięzcą.

Zauważmy, że warunek o częściowym izomorfizmie w naszej sytuacji oznacza tyle, że zbiory $\{a_{1},\dots ,a_{k}\}$ i $\{b_{1},\dots ,b_{k}\}$ elementów wybranych w każdej ze struktur, po posortowaniu rosnąco zgodnie z porządkiem odpowiednio $\leq ^{\mathfrak {A}}$ oraz $\leq ^{\mathfrak {B}}$ prowadzą do identycznych ciągów indeksów swoich oznaczeń. Dokładnie, jeśli $a_{i_{1}}<^{\mathfrak {A}}a_{i_{2}}<^{\mathfrak {A}}\dots <^{\mathfrak {A}}a_{i_{k}}$ i $b_{j_{1}}<^{\mathfrak {B}}b_{j_{2}}<^{\mathfrak {B}}\dots <^{\mathfrak {B}}b_{j_{k}}$, to zachodzą równości $i_{\ell }=j_{\ell }$ dla $\ell =1,\dots ,k$.

• Na pierwszy ruch gracza I gracz II odpowiada w dowolny sposób. Przed tą rundą nie było wybranych elementów, czyli przekształcenie opisane w definicji gry było przekształceniem pustym, które na mocy konwencji jest częściowym izomorfizmem. Po wykonaniu ruchu zgodnie ze strategią ciągi indeksów w obu strukturach są oczywiście identyczne.

• We wszystkich kolejnych rundach gracz II określa swój ruch następująco. Niech $a_{i_{1}}<^{\mathfrak {A}}a_{i_{2}}<^{\mathfrak {A}}\dots <^{\mathfrak {A}}a_{i_{k}}$ i $b_{i_{1}}<^{\mathfrak {B}}b_{i_{2}}<^{\mathfrak {B}}\dots <^{\mathfrak {B}}b_{i_{k}}$ będą (identycznymi na mocy założenia indukcyjnego) ciągami indeksów przed wykonaniem tego ruchu. Ze względu na symetrię sytuacji, możemy bez utraty ogólności założyć, że gracz I wybiera strukturę ${\mathfrak {A}}$. Może symbolem $a_{k+1}$ oznaczyć:
  • Element mniejszy od $a_{i_{1}}$. Wówczas gracz II wybiera element mniejszy od $b_{i_{1}}$ w ${\mathfrak {B}}$, który istnieje na mocy założenia, że w ${\mathfrak {B}}$ nie ma elementu najmniejszego. Widać, że nowe ciągi indeksów pozostaną równe.
  • Element większy od $a_{i_{k}}$. Wówczas gracz II wybiera element większy od $b_{i_{k}}$ w ${\mathfrak {B}}$, który istnieje na mocy założenia, że w ${\mathfrak {B}}$ nie ma elementu ostatniego. Widać, że także teraz nowe ciągi indeksów pozostaną równe.
  • Element $a$ spełniający $a_{i_{\ell }}<^{\mathfrak {A}}a<^{\mathfrak {A}}a_{i_{\ell +1}}$ dla pewnego $\ell$. W ${\mathfrak {B}}$ istnieje element $b$ spełniający $b_{i_{\ell }}<^{\mathfrak {B}}b<^{\mathfrak {B}}b_{i_{\ell +1}}$, gdyż ${\mathfrak {B}}$ jest porządkiem gęstym. Gracz II wybiera taki element i również w tym wypadku widać, że nowe ciągi indeksów pozostaną równe.

Na tym dowód istnienia strategii wygrywającej dla gracza II jest zakończony.

Z powyższego wynika między innymi, że $\langle \mathbb {R} ,\leq \rangle \equiv \langle \mathbb {Q} ,\leq \rangle$. Zatem nie ma zdania logiki pierwszego rzędu, które definiuje pojęcie porządku ciągłego (tzn. takiego, w którym wszystkie niepuste ograniczone podzbiory mają kres górny i kres dolny), bo musiałoby ono być prawdziwe w pierwszej ze struktur, a fałszywe w drugiej.

Definicja 4.14

Teorią nazywamy dowolny zbiór zdań, zamknięty ze wszględu na konsekwencje semantyczne, tj. taki zbiór zdań $\Delta$, że Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \Delta\models\var\varphi} zachodzi tylko dla Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \var\varphi\in\Delta} . Przykładem teorii jest każdy zbiór postaci Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \{\var\varphi\ |\ \Gamma\models\var\varphi\}} , zwany teorią aksjomatyczną wyznaczoną przez $\Gamma$, czy też postaci Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle Th( \mathcal K )=\{\var\varphi\ | \mathfrak A\models\var\varphi} , dla każdego ${\mathfrak {A}}\in {\mathcal {K}}\}$ (teoria klasy struktur ${\mathcal {K}}$) albo Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle Th(\mathfrak A )= \{\var\varphi\ | \mathfrak A\models\var\varphi\}} (teoria modelu ${\mathfrak {A}}$ ). Teorię $\Delta$ nazywamy zupełną, gdy dla każdego zdania Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \var\varphi} , dokładnie jedno ze zdań Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \var\varphi} i Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \lnot\var\varphi} należy do $\Delta$. Zbiór zdań prawdziwych w ustalonym modelu jest oczywiście zawsze teorią zupełną.

Wniosek 4.15

Teoria klasy ${\mathcal {A}}$ wszystkich porządków liniowych, gęstych, bez elementu pierwszego i ostatniego jest zupełna.

Dowód

Teoria, o której mówimy, nie ma modeli skończonych. W myśl Twierdzenia #Cantoro wszystkie jej modele nieskończone są elementarnie równoważne. Zatem $Th({\mathcal {A}})=Th(\langle \mathbb {Q} ,\leq \rangle )$, a teoria pojedynczego modelu jest zawsze zupełna.