# Logika - ćwiczenia 8

### Problem 2.4.1.
Let φ be a formula and f unary function symbol s.t.
1) f is not used in φ, and
2) every free occurrence of variable y in φ is not under the scope of a quantifier binding variable x.
Show that ∀x.∃y.φ is satisfiable if, and only if, ∀x.φ[y↦f(x)] is satisfiable.
Is the first assumption necessary? And the second one? Find counterexamples in each case.

* $∀x.∃y.φ$ is satisfiable $\quad$ if, and only if,$\quad ∀x.φ[y↦f(x)]$ is satisfiable

$A, \rho \vDash ∀x.∃y.φ$ , bo dla każdego a istnieje b, że $A, \rho[x↦a, y↦b] \vDash φ$.

rozszerzamy model A do A' poprzez dodanie $f^A$,
$f^A(a)=b$

$A', \rho \vDash ∀x.φ[y↦f(x)]$ , bo dla każdego a $[φ[y↦f(x)]]_{\rho'} = [φ]_{\rho'[y↦[f(x)]_{\rho'}]}$, gdzie $\rho'= \rho[x↦a]$, czyli

$A', \rho' \vDash φ[y↦f(x)]$ wtw $A', \rho' \vDash [φ]_{\rho'[y↦[f(x)]_{\rho'}]}$

a zatem nowy model będzie spełniać nową formułę.

* że f musi być świeże w φ

Zróbmy formułę φ (zawierającą f) taką, żeby ∀x.∃y.φ było spełnialne, ale ∀x.φ[y↦f(x)] nie

$\forall x. \exists y. R(f(x)) \land \neg R(y)$
Ta formuła jest spełnialna, bo
A={0,1}
f(x) = 0
R(0)
\neg R(1)
w w/w modelu zachodzi, ale formuła
$\forall x. \exists y. R(f(x)) \land \neg R(f(x))$
jest oczywiście niespełnialna.

* że y nie mogą występować w φ pod dodatkowym kwantyfikatorem ∀x lub ∃x

To jest spełnialne, np. w modelu o 2 elementach {a,b}
∀x.∃y.((∃x. y ≠ x) ∧ y=x)
(jak na zewnętrznemu x przyporządkujemy a, to na y i wewnętrzny x przyporządkujemy b i vice-versa)

∀x.((∃x. f(x) ≠ x) ∧ f(x)=x)
Ta formuła jest równoważna $((∃x. f(x) ≠ x) ∧ ∀x.f(x)=x)$, a ta jest oczywiście niespełnialna.

### Definiowalność

K klasy struktur "definiowalne" za pomocą jednej formuły pierwszego rzędu $\phi$.

$\mathfrak{K} = \{{\cal A} \mid {\cal A} \vDash \phi\}$

* czy ważne jest czy \phi jest zdaniem (czyli formułą bez zmiennych wolnych)?
Nie, bo $\{{\cal A} \mid {\cal A} \vDash \phi\} = \{{\cal A} \mid {\cal A} \vDash \overline{\forall}\phi\}$, gdzie $\overline{\forall}\phi$ to domknięcie wszystkich wolnych zmiennych $\phi$ kwantyfikatorami ogólnymi.

* a może w definicji powinna być \phi jest spełnialna w A

$\mathfrak{K} = \{{\cal A} \mid \phi \textrm{ jest spełnialna w } {\cal A}\}$

No podobnie jak wyżej, wystarczy domknąć \phi kwantyfikatorami szczegółowymi.

### Twierdzenie o zwartości
(Nieskończony) zbiór formuł $\Gamma$ jest spełnialny wtw gdy jest skończenie-spełnialny (czyli każdy jego skończony podzbiór jest spełnialny).

Warianty:

(Nieskończony) zbiór formuł $\Gamma$ jest niespełnialny wtw gdy ma skończony niespełnialny podzbiór.

Formuła \psi jest konsekwencją (nieskończonego) zbioru formuł $\Gamma$ wtw, gdy jest konsekwencją jego skończonego podzbioru.

Powiemy, że klasa $\mathfrak{K}$ jest definiowalna (jedną formuł logiki I rzędu), wtw gdy istnieje $\phi$, t. że $\mathfrak{K} = \{{\cal A} \mid {\cal A} \vDash \phi\}$.

Powiemy, że klasa $\mathfrak{K}$ jest aksjomatyzowalna (zbiorem formuł logiki I rzędu), wtw gdy istnieje $\Gamma$, t. że $\mathfrak{K} = \{{\cal A} \mid {\cal A} \vDash \Gamma\}$.

### Problem 2.9.6
"Skończoność" nie jest aksjomatyzowalna za pomocą zbioru formuł I rzędu.

Załóżmy, że jest aksjomatyzowalna za pomocą zbioru $\Delta$.

Napiszmy nieskończony zbiór formuł $\Gamma$, który mówi, że ew. struktura, która miałaby go spełniać jest nieskończona.

$\gamma_n = \exists x_1\dots \exists x_n. x_1 \neq x_2 ∧ \dots ∧ x_{n-1} \neq x_n$

$\Gamma = \{\gamma_n \mid n > 0\}$.

Bierzemy sobie zbiór $\Gamma \cup \Delta$ i... okazuje się, że cały zbiór jest sprzeczny, ale każdy jego skończony podzbiór jest niesprzeczny.

Istotnie, jesli weźmiemy $\Xi \subseteq \Gamma \cup \Delta$, to $\Xi = \Gamma_0 \cup \Delta_0$, gdzie $\Gamma_0 \subseteq \Gamma$ i \Delta_0 \subseteq \Delta$. Ponieważ $\Gamma_0$ jest skończona, więc istnieje $\gamma_m \in \Gamma_0$, gdzie $m$ to najwyższy numer formuły $\gamma_i 2 \Gamma_0$. Wtedy dowolna struktura o $m$ elementach spełnia zarówno $\Gamma_0$ jak i $\Delta_0$, bo jest to struktura skończona, a każda struktura skończona spełnia $\Delta$. A zatem $\Xi$ niesprzeczny.

Dostaliśmy więc sprzeczność z tw. o zwartości.