Przypomnijmy, reguła Modus Ponens mówi, że jeśli akceptujemy formułę \(\displaystyle{ \alpha}\) (jako prawdziwą), i jeśli akceptujemy formułę postaci \(\displaystyle{ \alpha \Rightarrow \beta}\) , gdzie \(\displaystyle{ \beta}\) jest dowolną formułą, to powinniśmy zaakceptować również formułę \(\displaystyle{ \beta.}\)
Przypomnijmy, dowodem formalnym formuły \(\displaystyle{ \alpha}\) nazywamy skończony ciąg formuł \(\displaystyle{ \alpha _{1}, \alpha _{2}, \ldots, \alpha _{n}}\), gdzie \(\displaystyle{ \alpha _{n}}\) jest tym samym napisem co formuła \(\displaystyle{ \alpha}\), a każda formuła \(\displaystyle{ \alpha _{i}}\) z tego ciągu formuł jest jednym z aksjomatów rachunku predykatów lub powstaje z dwóch formuł występujących wcześniej w tym ciągu formuł przez zastosowanie do nich reguły Modus Ponens (to ostatnie oznacza, że istnieją \(\displaystyle{ j,k=1,2,\ldots, n}\),takie, że \(\displaystyle{ j,k<i}\), i takie, że formuła \(\displaystyle{ \alpha _{i}}\) powstaje przez zastosowanie reguły Modus Ponens do formuł \(\displaystyle{ \alpha _{j}}\) i \(\displaystyle{ \alpha _{k}.}\)
Twierdzeniem formalnym rachunku predykatów nazywamy dowolną formułę dla której istnieje jej dowód formalny.
Spróbuję teraz wytłumaczyć, że twierdzenia formalne rachunku predykatów są to dokładnie konsekwencje logiczne aksjomatów (względem reguły Modus Ponens).
Jeśli formuła \(\displaystyle{ \alpha}\) jest twierdzeniem formalnym, to istnieje jej dowód formalny.
Tzn., jest to skończony ciąg formuł \(\displaystyle{ \left( \alpha _{1}, \alpha _{2}, \ldots, \alpha _{n}= \alpha \right).}\) Przyjrzyjmy się po kolei formułom tego ciągu.
Formuła \(\displaystyle{ \alpha _{1}}\) nie może powstać przez zastosowanie reguły Modus Ponens do formuł wcześniejszych z tego ciągu formuł, gdyż nie ma formuł wcześniejszych (formalnie: nie istnieją \(\displaystyle{ j,k<1,}\) tak, aby formuła \(\displaystyle{ \alpha _1}\) powstała przez zastosowanie reguły Modus Ponens do formuł \(\displaystyle{ \alpha _j, \alpha _k}\) ), a zatem musi zajść przypadek przeciwny (gdyż ta własność z definicji dowodu formalnego zachodzi dla każdego \(\displaystyle{ i=1,2,\ldots, n}\)), a więc w szczególności zachodzi dla \(\displaystyle{ i=1}\), wobec czego formuła \(\displaystyle{ \alpha _1}\) musi być aksjomatem.
Dalej, formuła \(\displaystyle{ \alpha _2}\) (o ile taka występuje, czyli o ile ten dowód formalny ma długość większą niż jeden) albo jest aksjomatem, albo powstaje przez zastosowanie reguły Modus Ponens do pary formuł \(\displaystyle{ (\alpha _1, \alpha _{1})}\), a wiemy już, że formuła \(\displaystyle{ \alpha _{1}}\) jest aksjomatem, wobec czego formuła \(\displaystyle{ \alpha _2}\) jest konsekwencją tego aksjomatu.
Itd., aż do \(\displaystyle{ i=n}\). Wtedy formuła \(\displaystyle{ \alpha _n = \alpha}\) jest konsekwencją logiczną aksjomatów, co należało uzasadnić.
Objaśnię jeszcze definicję wartościowania termów, gdyż zauważyłem, że parę razy o to pytano na forum (a tak naprawdę chcę po prostu się tym podzielić):
Jeśli \(\displaystyle{ M= \left( D,I\right)}\) jest dowolnym modelem, gdzie \(\displaystyle{ D}\) jest niepustym zbiorem, a \(\displaystyle{ I}\) jest interpretacją symboli języka,to:
Przypomnijmy najpierw:
Wartościowanie zmiennych, to funkcja, która zmiennym przypisuje wartości dziedziny.
Przypomnijmy, że termami, są wszystkie symbole stałych oraz wszystkie symbole zmiennych oraz wszystkie napisy postaci \(\displaystyle{ \alpha _{n} \left( t_1, t_2, \ldots, t_n\right)}\), gdzie \(\displaystyle{ \alpha _{n}}\) jest \(\displaystyle{ n}\)-argumentowym symbolem funkcyjnym, a \(\displaystyle{ t_1, \ldots, t_n}\) są dowolnymi termami.
W dowolnym ustalonym modelu \(\displaystyle{ M= \left( D,I\right),}\) dowolne ustalone wartościowanie zmiennych \(\displaystyle{ \alpha}\) możemy rozszerzyć na wszystkie termy, w następujący sposób (rozszerzenie oznaczymy jako \(\displaystyle{ \beta}\) ):
Jeśli term \(\displaystyle{ t}\) jest stałą, to \(\displaystyle{ \beta \left( t\right) = I\left( t\right)}\), (stale wartościujemy, tymi samymi elementami przypisanymi tym symbolom stałych, zgodnie z interpretacją w modelu),
a jeśli term \(\displaystyle{ t}\) jest postaci \(\displaystyle{ f\left( t_1, \ldots, t_n \right)}\), gdzie \(\displaystyle{ f}\) jest \(\displaystyle{ n}\)-argumentowym symbolem funkcyjnym, a \(\displaystyle{ t_1, t_2,\ldots, t_n}\) są (pod)termami, to:
\(\displaystyle{ \beta \left( f\left( t_1,\ldots , t_n\right) \right) = I\left( f\right) \left( \beta \left( t_1\right),\ldots, \beta \left( t_n\right) \right);}\)
czyli aby poznać wartość termu \(\displaystyle{ \beta \left( f\left( t_1,\ldots , t_n\right) \right)}\) najpierw wyznaczamy wartości podtermów \(\displaystyle{ \beta \left( t_1\right) ; \beta \left( t_2\right); \ldots, \beta \left( t_n\right)}\), a potem wyznaczamy wartość funkcji odpowiadającej interpretacji symbolu \(\displaystyle{ f}\) (czyli \(\displaystyle{ I\left( f\right)}\) ) na wartościach tych podtermów.
Na koniec podam coś prostszego, dwa zadania z ważniaka:
Oto pierwsze takie zadanie:
Czy dla każdej formuły \(\displaystyle{ \alpha}\) rachunku predykatów można utworzyć formułę jej równoważną, w której nie występuje symbol kwantyfikatora \(\displaystyle{ \forall }\)??
Odpowiedź na to pytanie zależy od tego, czym jest alfabet języka, a dokładniej: czy jako kwantyfikator mamy tylko kwantyfikator ogólny \(\displaystyle{ \forall}\), (a kwantyfikator szczegółowy traktujemy jako skrót), czy może możemy również tutaj używać kwantyfikatora 'istnieje' \(\displaystyle{ \exists}\).
W pierwszym przypadku trzeba by było formułę z kwantyfikatorami \(\displaystyle{ \forall}\) zapisać bez tego kwantyfikatora, a więc bez żadnych kwantyfikatorów, a więc nie dało by się tego zrobić (tak mi się wydaje).
Skupmy się na drugiej wersji.
Zauważmy, że jeśli mamy formułę postaci: \(\displaystyle{ \forall_{x} \alpha \left( x\right)}\), to możemy ją zapisać równoważnie:
\(\displaystyle{ \Leftrightarrow \neg \left( \neg \left( \forall x \quad \alpha \left( x\right)\right) \ \right) \Leftrightarrow \neg \exists x\quad \neg \left( \alpha \left( x\right) \right). }\)
A zatem wyeliminowaliśmy symbol kwantyfikatora 'dla każdego' formułą równoważną (dla formuł postaci \(\displaystyle{ \forall x \quad \alpha \left( x\right)\ }\)).
Niech teraz \(\displaystyle{ \alpha}\) będzie dowolną formułą rachunku predykatów.
Wtedy występuje w niej skończona ilość symboli kwantyfikatora 'dla każdego' \(\displaystyle{ \forall}\). Postępując z każdym takim kwantyfikatorem, tak, jak powyżej, otrzymamy formułę bez kwantyfikatora ogólnego, formułę równoważną formule \(\displaystyle{ \alpha .\square}\)
I jeszcze jedno ciekawe zadanie z ważniaka:
Czy istnieje model z predykatem dwuargumentowym \(\displaystyle{ \left( =\right)}\) w którym formuła: \(\displaystyle{ \forall y \forall x \left( x=y\right)}\) jest prawdziwa??
ROZWIĄZANIE:
Tak, ja wziąłbym: \(\displaystyle{ M= \left\{ 0\right\} .}\)
Wtedy, dla każdego \(\displaystyle{ y}\) (w naszym modelu \(\displaystyle{ M}\), czyli dla \(\displaystyle{ y \in \left\{ 0\right\}}\), czyli dla \(\displaystyle{ y=0}\)), oraz dla każdego \(\displaystyle{ x}\) w naszym modelu, czyli dla \(\displaystyle{ x=0,}\) mamy niewątpliwie \(\displaystyle{ x=y(=0). \square}\)
