Aksjomatyka Rachunku Predykatów

Rachunek predykatów podobnie jak klasyczny rachunek zdań może być wprowadzony aksjomatycznie. Pierwsza grupa aksjomatów to aksjomaty klasycznego rachunku zdań. Druga dotyczy kwantyfikatora \( \forall \) oraz jego interakcji z implikacją. Przypomnijmy, że kwantyfikator \( \exists \) traktujemy jako pewien skrót zapisu.

Definicja 3.1. Schematy aksjomatów rachunku predykatów

1. (Aksjomaty logiki zdaniowej) Każda formuła pasująca do któregokolwiek z poniższych schematów jest tautologią

(a) \( (\phi \Rightarrow (\psi \Rightarrow \phi)) \)

(b) \( (\phi \Rightarrow (\nu \Rightarrow \psi) \Rightarrow ((\phi \Rightarrow \nu) \Rightarrow (\phi \Rightarrow \psi) ) \)

2. (Aksjomaty dotyczące kwantyfikatora)

(a) Dla dowolnej formuły \( \phi \) oraz termu \( t \) następująca formuła jest aksjomatem \( \forall_x \phi \Rightarrow (\phi [x arrow t]) \) (uwaga na podstawienie)

(b) Dla dowolnej formuły \( \phi \) oraz zmiennej \(\mathrm {x} \), która nie ma wolnych wystąpień w \( \phi \) następująca formuła jest aksjomatem \( \phi \Rightarrow \forall_x \phi \)

(c) Dla dowolnych formuł \( {\phi} \) i \( {\psi} \) aksjomatem jest formuła \( \forall_x(\phi \Rightarrow \psi) \Rightarrow ((\forall_x \phi)\Rightarrow(\forall_x \psi)) \)

Poza tym do aksjomatów dorzucamy również wszystkie generalizacje formuł pasujących do powyższych schematów. Generalizacja formuły jest to ta sama formuła poprzedzona blokiem kwantyfikatorów ogólnych - dla dowolej formuły \( \phi \) oraz dowolnych zmiennych \( x_1,\dots,x_k \) formuła \( \forall_{x_1} \dots \forall_{x_k} \phi \) jest generalizacją \( \phi \).

Podobnie jak w rachunku zdań dowodem formuły \( {\phi} \) nazwiemy ciąg formuł \( \phi_0, \dots, \phi_n \) taki, że \( \phi_n \) jest tym samym napisem co \( {\phi} \) a każda formuła \( \phi_i \) dla \( i < n \) jest aksjomatem rachunku predykatów lub powstaje z dwóch formuł występujących wcześniej w dowodzie poprzez zastosowanie reguły Modus Ponens z Wykładu 2.

Definicja 3.2.

Twierdzeniem rachunku predykatów nazywamy dowolną formułę którą da się dowieść z aksjomatów rachunku predykatów.

Przykład 3.3.

Formalne dowody twierdzeń rachunku predykatów są zwykle skomplikowane. Dlatego w rozważanym przykładzie poczynimy kilka uproszczeń. Będziemy się zajmować formułą \( \displaystyle p(t) \Rightarrow \exists_x p(x). \)

Zamiast dowodzić dokładnie powyższą formułę, dowiedziemy podobny fakt, a mianowicie, że jeśli dołączymy do zbioru aksjomatów formułę \( \displaystyle p(t) \), to będziemy w stanie udowodnić \( \displaystyle \exists_x p(x) \). Twierdzenie o dedukcji, które można znaleźć w wykładzie Logika dla informatyków, mówi, że te podejścia są równoważne.

W poniższym dowodzie pominiemy również dowód formuły \( \displaystyle \neg \neg \forall_x \neg p(x) \Rightarrow \forall_x \neg p(x) \). Formuła ta pasuje do schematu \( \displaystyle \neg \neg \phi \Rightarrow \phi \). Łatwo więc sprawdzić, że formuła \( \displaystyle \neg \neg \phi \Rightarrow \phi \) jest tautologią klasycznego rachunku zdań, a więc -- w myśl twierdzenia Posta (patrz Wykład 2, Twierdzenie 4.4) -- ma dowód. Po zastąpieniu w tym dowodzie zmiennej \( \displaystyle \phi \) formułą \( \displaystyle \forall_x \neg p(x) \), otrzymamy dowód formuły \( \displaystyle \neg \neg \forall_x \neg p(x) \Rightarrow \forall_x \neg p(x) \).

Przestawiamy uproszczony dowód formuły \( \displaystyle p(t) \Rightarrow \exists_x p(x) \):

\( \displaystyle \neg \neg \forall_x \neg p(x) \Rightarrow \forall_x \neg p(x) \) (patrz komentarz powyżej)
\( \displaystyle (\forall_x \neg p(x)) \Rightarrow \neg p(t) \) (aksjomat 2a)
\( \displaystyle [(\forall_x \neg p(x)) \Rightarrow \neg p(t)] \Rightarrow ([\neg \neg \forall_x \neg p(x)] \Rightarrow [(\forall_x \neg p(x)) \Rightarrow \neg p(t)]) \) (aksjomat 1a)
\( \displaystyle [\neg \neg \forall_x \neg p(x)] \Rightarrow [(\forall_x \neg p(x)) \Rightarrow \neg p(t)] \) (MP z 2 i 3)
\( \displaystyle ([\neg \neg \forall_x \neg p(x)] \Rightarrow [(\forall_x \neg p(x)) \Rightarrow \neg p(t)]) \Rightarrow [(\neg \neg \forall_x \neg p(x) \Rightarrow \forall_x \neg p(x)) \Rightarrow [(\neg \neg \forall_x \neg p(x))\Rightarrow \neg p(t)]] \) (aksjomat 1b)
\( \displaystyle (\neg \neg \forall_x \neg p(x) \Rightarrow \forall_x \neg p(x)) \Rightarrow [(\neg \neg \forall_x \neg p(x))\Rightarrow \neg p(t)] \) (MP z 4 i 5)
\( \displaystyle (\neg \neg \forall_x \neg p(x))\Rightarrow \neg p(t) \) (MP z 6 i 1)
\( \displaystyle p(t) \Rightarrow ([\neg \neg \forall_x \neg p(x)]\Rightarrow p(t)) \) (aksjomat 1a)
\( \displaystyle p(t) \) (dołączyliśmy tę formułę jako aksjomat)
\( \displaystyle [\neg \neg \forall_x \neg p(x)]\Rightarrow p(t) \) (MP z 8 i 9)
\( \displaystyle ([\neg \neg \forall_x \neg p(x)]\Rightarrow p(t)) \Rightarrow [((\neg \neg \forall_x \neg p(x))\Rightarrow \neg p(t)) \Rightarrow \neg \forall_x \neg p(x)] \) (aksjomat 1c)
\( \displaystyle (\neg \neg \forall_x \neg p(x))\Rightarrow \neg p(t)) \Rightarrow \neg \forall_x \neg p(x) \) (MP z 10 i 11)
\( \displaystyle \neg \forall_x \neg p(x) \) (MP z 7 i 12)

Ostatnia formuła to dokładnie \( \displaystyle \exists_x p(x) \) po rozpisaniu skrótu \( \displaystyle \exists \).

Przykład teorii w rachunku predykatów

W oparciu o logikę predykatów możemy budować nowe teorie, dokładając inne, tzw. pozalogiczne aksjomaty. W językach wielu teorii pojawia się symbol predykatywny \( =^2 \), mający symbolizować równość. Ponieważ zwykle wymagamy aby te same własności były spełnione dla \( =^2 \), zostały wyodrębnione specjalne aksjomaty dla równości. Aksjomaty, te to wszystkie formuły oraz ich generalizacje odpowiadające poniższym schematom:

1. \( t=t \), dla każdego termu \( t \)

2. \( ( t_1=t_1' \wedge \ldots \wedge t_k= t_k' ) \Rightarrow f(t_1,\ldots,t_k) = f(t_1', \ldots,t_k') \), dla dowolnego symbolu funkcyjnego \( f \), oraz dowolnych termów \( t_1,\ldots,t_k, t_1', \ldots, t_k' \), gdzie \( k \) jest ilością argumentów symbolu \( f \)

3. \( ( t_1=t_1' \wedge \ldots \wedge t_k= t_k' ) \Rightarrow ( p(t_1,\ldots,t_k) \Rightarrow p(t_1', \ldots,t_k') ) \), dla dowolnego symbolu predykatywnego \( p \), oraz dowolnych termów \( t_1,\ldots,t_k, t_1', \ldots, t_k' \), gdzie \( k \) jest ilością argumentów symbolu \( p \)

Rozważmy język, w którym mamy jeden binarny symbol predykatywny \( =^2 \), jeden symbol stałej \( 0 \) oraz symbole funkcyjne \( s^1, +^2, \times^2 \). Zgodnie z przyjętą konwencją termy i formuły będziemy zapisywać infixowo. Do aksjomatów logicznych, oraz aksjomatów dla równości, dokładamy następujące aksjomaty:

1. \( \forall_x \forall_y (s(x)=s(y) \Rightarrow x=y) \)

2. \( \forall_x \neg s(x)=0 \)

3. \( \forall_x (\neg (x=0) \Rightarrow (\exists_y s(y)=x)) \)

4. \( \forall_x x+0=x \)

5. \( \forall_x \forall_y x+s(y)=s(x+y) \)

6. \( \forall_x x\times 0= 0 \)

7. \( \forall_x \forall_y x\times s(y)=x \times y+y \)

Teorią Q nazwiemy wszystkie formuły w ustalonym języku które da się udowodnić z aksjomatów logiki predykatów z dołączonymi aksjomatami równości oraz 1-7. Nietrudno się przekonać, że wszystkie twierdzenia teorii Q są prawdziwe w liczbach naturalnych, przy naturalnej interpretacji występujących symboli (\( s(x) \) interpretujemy jako \( x+1 \)). W następnym wykładzie (patrz Wykład 4) przedstawiamy aksjomatyczną teorię w rachunku predykatów nazywaną teorią mnogości ZFC.

Informatyka MIMUW