# Logika - ćwiczenia 11

## Logika pierwszego rzędu ogólnie nierozstrzygalna, ale czasem rozstrzygalna...
- ograniczenia sygnatury
- ograniczenia rzędu formuły
- niestandardowe pytania (np. dot 1 teorii)

### Niezbyt duży model
Niech sygnatura będzie relacyjna i składa się z symboli unarnych $\Sigma = \{P_1, \ldots P_m\}$. Niech $\phi$ będzie zdaniem o randze kwantyfikatorowej $q$. Udowodnij, że jeśli $\phi$ spełnialne to ma model mocy co najwyżej $q\cdot2^m$.

Jeśli weźmiemy (duży) model $B$ formuły $\phi$, to istnieje model A wielkości $≤q\cdot2^m$, taki, że A jest nieodróżnialny od B za pomocą gry E-F o q rundach.

Wystarczy wziąć elementy tych samych "rodzajów" (w sensie należenia bądź nie do interpretacji odp. symboli $P_i$). Jeśli w B jest elementów danego rodzaju ≤ q to w A bieżemy tyle samo, a jeśli > q, to w A bieżemy $q$.
W grze o $q$ rundach strategia Duplikatora jest oczywista.

A zatem, żeby rozstrzygnąć spełnialność formuły $\phi$ wystarczy przejrzeć wszystkie modele $≤ q\cdot 2^m$, których jest skończenie wiele.
A zatem ten fragment FOL jest rozstrzygalny.

## Wstęp / przypomnienie

*Teoria* to zbiór zdań zamknięty na konsekwencje logiczne.
*Teoria struktury* A, ozn. Th(A) to zbiór wszystkich zdań prawdziwych w strukturze A. Siłą rzeczy jest on zamknięty na konsekwencje logiczne :)
Przez $Th(\Gamma)$, gdzie $\Gamma$ jest zbiorem zdań oznaczamy teorię będącą domknięciem zbioru $\Gamma$ ze względu na konsekwencje logiczne.

## Eliminacja kwantyfikatorów

Teoria $T$ dopuszcza eliminację kwantyfikatorów jeśli dla każdej formuły $\phi$ istnieje $\psi$ bez kwantyfikatorów i takie, że
- $fv(\psi) \subseteq fv(\phi$)
- $T \vDash \phi ↔ \psi$

Przykłady:
$\forall x. (P(x) ∧ ¬ P(x))$ możemy zastąpić przez $\bot$.
$\forall x. (P(x) ∨ ¬ P(x))$ możemy zastąpić przez $\top$.
Jeśli rozważamy porządki gęste $(\exists x. a < x ∧ x < b) \equiv a < b$

**Fakt1**. Eliminację kwantyfikatorów wystarczy badać na formułach postaci
$\exists x (\phi_1 ∧ \ldots ∧ \phi_n)$, gdzie $\phi_i$ to formuły "prawie" atomowe (czyli atomowe lub ich negacje), których zmienne wolne zawierają $x$.

Możemy zastąpić $\forall$, $→$, $↔$ przez $\exists$, ∨, ∧, ¬, używając praw de Morgana, def. implikacji i równoważności. A potem idąc od dołu eliminujemy kwantyfikatory \exists, "przepychając" każdy z nich uprzednio w dół (stosując rozdzielność alternatywy względem koniunkcji, kwantyfikatora exists względem alternatywy, wyłączania koniunktów nie zależnych od $x$, praw de Morgana itp.) - aż doprowadzimy do wymaganej postaci. Potem eliminujemy ten kwantyfikator i zabieramy się za kolejny... I tak dalej, aż się skończą...

### Sygnatura pusta

Dla dowolnego A, Th(A) ma efektywną eliminację kwant w Th(A).

$\psi = \exists x. x=a_1 ∧ ... ∧ x=a_m ∧ x \neq b_1 ∧ ... ∧ x \neq b_n$.

* jesli któreś b_i to x (czyli mamy $x \neq x$), to całe $\psi \equiv \bot$
* jeśli któreś a_i to x (czyli mamy $x = x$), to usuwamy tę równość
* jeśli pozostaje jakieś $x = a_i$ (gdzie a_i to nie x), to
zastępujemy x przez a_i w pozostałej części formuły, a kwantyfikator usuwamy
(np. $\exists x. x=a_1 ∧ x\neq b_1 ∧ x \neq b_2 \quad \equiv \quad a_1 \neq b_1 ∧ a_1 \neq b_2$)

* może tak być, że nic nie zostało, wtedy $\top$:

$\exists x. x=x \quad \equiv \text{usuwamy x=x}\equiv\quad \exists x. (\text{pusta koniunkcja}) \quad \equiv \quad \top$

* jeśli nie ma żadnych równości, tylko same nie-równości

$\exists x. x \neq b_1 ∧ ... ∧ x \neq b_m$
Zał na początek, że |A| > m (być może |A| nieskończone).
Wtedy ta formuła jest zawsze prawdziwa, czyli zastępujemy całość przez $\top$.

Wpp na przykład
gdy model ma |A|=2:
$\exists x. x \neq b_1 ∧ x \neq b_2 \quad \equiv \quad b_1=b_2$

gdy model ma |A|=3:
$\exists x. x \neq b_1 ∧ x \neq b_2 ∧ x \neq b_3 ∧ x \neq b_4 \quad \equiv \quad$ alternatywa koniunkcji równości mówiąca $|\{b_1,b_2,b_3,b_4\}| < 3$, czyli $(b_1=b_2 ∧ b_3=b_4) ∨ (b_1=b_2 ∧ b_2=b_3) ∨ ...$

W ogólności dla $m ≥ |A|$:
$\exists x. x \neq b_1 ∧ ... ∧ x \neq b_m \quad \equiv \quad$ alternatywa koniunkcji równości mówiąca $|\{b_1,...,b_m\}| < |A|$

### Liczby całkowite z porządkiem
Rozważmy teorię struktury $\langle Z, ≤ \rangle$

$\Sigma = \{ ≤ \}$ - jeden symbol relacyjny dwuargumentowy.

Tu nie da się wyeliminować kwantyfikatorów, bo formuła mówiąca "y jest następnikiem x" da się napisać z kwantyfikatorem:
$\phi_s(x,y) \equiv x ≤ y ∧ \forall z. x < z → y ≤ z$
albo trzymając się ściśle sygnatury moglibysmy napisać:
$\phi_s(x,y) \equiv x ≤ y ∧ \forall z. x ≤ z → x = z ∨ y ≤ z$

Teraz pokażemy, że nie da się tego zrobić bez kwantyfikatora:
Rozważmy dowolna formułę bez kwantyfikatorów o 2 zmiennych x i y:
$\psi(x,y)$
Popatrzmy na nią w taki sposób: $\psi_x(y)$ - co możemy powiedzieć o y względem x?
Okazuje się, że są tylko kombinacje tych trzech możliwości:
$y>x, \quad y=x, \quad y<x$
Wszystkie formuły bez kwantyfikatorów są spełnione przez "kombinacje" w/w zbiorów (dowód przez indukcję: formuły atomowe są, koniunkcja, alternatywa, negacja tego nie psują - bo to przecięcie, suma, dopełnienie). Ale następnik $\{x+1\}$ nie jest taką kombinacją, więc nie da się go otrzymać bez kwantyfikatorów.

A zatem spróbujmy dołożyć następnik (i poprzednik) i rozważyć teorię struktury:
$\langle Z, ≤, s, p \rangle$
(Teraz $\Sigma_R = \{≤\}, \Sigma_F=\{s,p\}$ - symbol relacyjny j.w. oraz dwa symbole funkcyjne unarne)

Rozważmy formuły postaci $\exists x. \text{koniunkcja formuł atomowych i ich negacji}$
Ponieważ x < y ≈ s(x) ≤ y to zauważmy, że:

¬ (x ≤ y) ≈ x > y ≈ x ≥ s(y)

¬ (x = y) ≈ x < y ∨ x > y ≈ s(x) ≤ y ∨ x ≥ s(y)

Czyli każdą formułę atomową możemy doprowadzić do nierówności nieostrych oraz równości (w sumie równości też moglibyśmy zastąpić nierównościami nieostrymi, ale one się łatwo dają załatwić :)

Przy pojawieniu się alternatywy musimy "podzielić" kwantyfikator na dwa, ale koniec końców dostajemy:
$\exists x. \text{koniunkcja nierówności i równości zawierających x}$.

Porządkujemy wszystkie równości i nierówności (p(s(coś))=coś)
p(coś) ≤ p(inne) wtw coś ≤ inne itd,
s(coś) ≤ inne wtw coś ≤ p(inne)
Idziemy w kierunku uzyskania postaci x = coś, x ≤ coś, albo coś ≤ x i zawsze do takiej postaci dojdzieemy.

Jeśli jest jakaś równość x = "coś bez x" to postępujemy jak w poprzednim zadaniu (usuwamy kwantyfikator i zastępujemy x poprzez "coś bez x").
Wpp:
Jeśli mamy równość x=x to ją eliminujemy.
Podobnie nierówności p(p(x)) ≤ x oraz x ≤ s(s(s(x))) (dowolna nieujemna liczba s / p)

Jak się trafi nierówność j.w. ale odwrotnie (np. p(x) ≥ x lub x ≥ s(s(x)) - dowolna niezerowa liczba s i p), to całość jest fałszywa $\bot$.
Podobnie, jak będzie równość w stylu x = p(p(x)) albo x = s(s(s(x))).

Pozostała nam taka możliwość:
$\exists x. t_1 ≤ x ∧ ... ∧ t_n ≤ x ∧ x ≤ s_1 ∧ ... ∧ x ≤ s_m$, gdzie w $t_i$ oraz $s_j$ nie ma x.

Jeśli n=0 lub m=0, to całość jest równoważna $\top$, bo Z jest nieograniczone ani z dołu ani z góry.

Wpp, jeśli n>0 i m>0, formuła jest równoważna:
$\bigwedge_{i,j} t_i ≤ s_j$
(wszystkie ograniczenia dolne x mają być mniejsze-równe niż wszystkie ograniczenia górne x).

A zatem umiemy efektywnie wyeliminować kwantyfikatory z każdej formuły nad < Z, ≤, s, p >!

Zauważmy, że w otrzymanej po eliminacji formule możemy zastąpić wszystkie p przez s (po drugiej stronie nie/równości).
A więc pokazaliśmy, że z formuły zapisanej za pomocą ≤ i s też umiemy wyeliminować kwantyfikatory (w trakcie eliminowania używamy p, ale tylko "na chwilę" - ważne, że końcowa formuła nie ma p i jest równoważna tej początkowej).

A zatem mając dane dowolne zdanie $\phi$ możemy w nim wyeliminować wszystkie kwantyfikatory - zostanie nam zdanie bez kwantyfikatorów i bez zmiennych wolnych (bo zdanie ich nie miało), a zatem będzie to formuła równoważna $\top$ lub $\bot$.

<div style="height: 3000px"></div>