Teorie aksjomatyczne

Ważnym, historycznym przykładem teorii aksjomatycznej jest tzw. Aksjomatyka Euklidesa. Próbował on określić pewne podstawowe zasady geometrii, z których można by wyprowadzić całą resztę faktów jedynie poprzez rozumowanie. W dzisiejszym rozumieniu, takie zasady stanowiłyby aksjomatykę geometrii płaszczyzny.

Oto reguły zaproponowane przez Euklidesa:

1. Dowolne dwa punkty można połączyć odcinkiem.
2. Dowolny odcinek można przedłużyć nieograniczenie (uzyskując prostą).
3. Dla danego odcinka można zaznaczyć okrąg o środku w jednym z jego końców punkcie i promieniu równym jego długości.
4. Wszystkie kąty proste są przystające.
5. Dwie proste, które przecinają trzecią w taki sposób, że suma kątów wewnętrznych po jednej stronie jest mniejsza od dwu kątów prostych, przetną się z tej właśnie strony.

Z dzisiejszego punktu widzenia te reguły nie są jeszcze aksjomatami, gdyż ich sposób formułowania nie jest całkiem ścisły (np. co to znaczy przedłużyć?). Jednak można je wyrażać w sposób bardziej jednoznaczny.

Gdy spojrzeć na te aksjomaty, dość szybko dostrzec można że ostatni z nich jest znacznie bardziej skomplikowany niż pierwsze cztery. W oparciu o to spostrzeżenie, sam Euklides postawił problem, czy może ten aksjomat wynika z pozostałych. Wtedy nie trzeba by go było umieszczać na liście i stała by się ona prostsza. Problem ten, nazywamy problemem V aksjomatu Euklidesa był przez długi czas badany.

Dopiero w XIX wieku pokazano, że aksjomat piąty nie wynika z poprzednich. Sposób rozumowania był taki, że można wskazać model dla pierwszych czterech aksjomatów, w którym piąty nie jest prawdziwy. Modele takie to geometrie nieeuklidesowe.

Badania aksjomatyki Euklidesa były kontynuowane, okazało się na przykład, że z podanych pięciu aksjomatów nie wynika, że (mówiąc nieściśle) prosta dzieli płaszczyznę na dwa kawałki. Jest to tzw. aksjomat Pascha. W 1899 roku David Hilbert poprawił aksjomaty Euklidesa, formułując listę 21 aksjomatów dla geometrii płaszczyzny. Pokazał on przy okazji niesprzeczność swoich aksjomatów.

Aktualnie, w geometrii, silnie wykorzystuje się kartezjański układ współrzędnych, przez co dowodzone twierdzenia opierają się na własnościach liczb. W związku z tym aksjomaty płaszczyzny (czy to te Euklidesa, czy też Hilberta) nie są używane.

Domknięcie semantyczne

Po głębszym zastanowieniu, okazuje się że na operację która Φ zamienia w Th(Mod(Φ)) można patrzeć jak na pewnego rodzaju domknięcie Φ. Nazywamy to domknięciem semantycznym Φ i oznaczamy \(\overline{\Phi}\). Powyżej pokazane było, że \(\overline{\Phi}\), zawiera Φ. Pewnego zastanowienia wymaga dostrzeżenie, że \(\overline{\left(\overline{\Phi}\right)}=\overline{\Phi}\), czyli podwójne domknięcie jest równe po prostu domknięciu. Temat ten zostanie rozwinięty w sekcji Definicje prawdy.

Przykład:

Rozważmy sygnaturę Σ zawierającą tylko relację dwuargumentową \(\leq\). Weźmy też rodzinę zdań Φ zawierającą wypisane wcześniej aksjomaty porządku liniowego oraz dodatkowo zdanie:

\(\forall_x\exists_y x\leq y\wedge x\neq y\),

mówiące że od każdego elementu istnieje ściśle większy. W takiej sytuacji, Φ składa się w sumie z 5 zdań. Zauważmy że Mod(Φ) to klasa wszystkich porządków liniowych które nie mają elementu największego. Porządki takie to na przykład liczby naturalne, liczby wymierne, czy liczby rzeczywiste. Natomiast ujemne liczby całkowite nie są takim porządkiem, bo nie ma wśród nich liczby ściśle większej niż − 1.

Zbiór Th(Mod(Φ)) jest znacznie większy od Φ. Skoro rozpatrywane porządki nie mają elementu największego, to w szczególności muszą mieć nieskończenie wiele elementów. Więc Th(Mod(Φ)) zawiera między innymi zdanie mówiące, że w danej strukturze są przynajmniej trzy różne elementy:

\(\exists_{x_1}\exists_{x_2}\exists_{x_3}x_1\neq x_2\wedge x_2\neq x_3\wedge x_3\neq x_1\).

jak również podobne zdania, mówiące że w strukturze jest przynajmniej \(4,5,6,\ldots\) różnych elementów. Czyli Th(Mod(Φ)) zawiera nieskończenie wiele zdań. Są tam między innymi zdania trywialne, jak \(\top\), czy \(\exists_x\top\). Nie ma tam natomiast zdania \(\exists_x\forall_y x\leq y\), mówiącego że istnieje element najmniejszy. Wynika to z faktu, że jednym z modeli są liczby rzeczywiste, a tam to zdanie nie jest prawdziwe.

Domknięcie klasy struktur

Analogicznie do domknięcia semantycznego zbioru zdań, można zdefiniować domknięcie klasy struktur \(\mathcal M\), jako \(\overline{\mathcal M}=Mod(Th(\mathcal M))\). Znowu, wiemy że \(\mathcal M\subseteq\overline{\mathcal M}\) i można pokazać że \(\overline{\left(\overline{\mathcal M}\right)}=\mathcal M\). Spostrzeżenie to ma swoje silne konsekwencje w algebrze ogólnej, gdzie bada się rodziny struktur o pewnych własnościach.

Definicje prawdy

Gdy nie trzymamy w ręku jednej, ustalonej struktury nad którą pracujemy, pojęcie prawdy się komplikuje. Kluczowa trudność jest taka, że nawet przy ustalonej aksjomatyce, na ogół istnieje wiele różnych struktur ją spełniających. I jedne z nich mogą spełniać daną formułę, a inne nie.

Weźmy na przykład aksjomatykę porządków liniowych opisaną powyżej. Wtedy zdanie \(\forall_x\forall_y x=y\) jest spełnione w strukturze \(<\{0\},\leq>\), bo ma on tylko jeden element, ale nie jest prawdziwe w strukturze \(<\{0,1\},\leq>\).

Przyjętym rozwiązaniem jest następująca definicja:

Powyższy przykład pokazuje, że zdanie \(\phi\equiv\forall_x\forall_y x=y\) nie jest prawdą, przy założeniu aksjomatów porządku liniowego. Ale jego zaprzeczenie też nie jest prawdą, bo w pewnych strukturach φ jest prawdą! Inny przykład to zdanie \(\exists_x \forall_y x\leq y \vee y = 0\), które jest prawdą przy założeniu aksjomatów liczb naturalnych, szukana liczba x, to 1. Jak to udowodnić opisane jest w sekcji Dowody.

Aby uniknąć problemów opisanych na początku tej sekcji, dowodzone twierdzenia (na przykład na temat liczb naturalnych) nie mówią:

zdanie φ jest prawdą w danej od Pana Boga, ustalonej strukturze liczb naturalnych,

tylko zamiast tego, mówią:

zdanie φ jest prawdą przy założeniu aksjomatyki liczb naturalnych.

Można podaną wyżej definicję prawdziwości, widzieć następująco:

Zdanie φ jest prawdą przy założeniu Φ, jeśli \(\phi\in Th(Mod(\Phi))=\overline{\Phi}\).

Jest to równoważne podejście, gdyż zdanie φ jest prawdą w każdej strukturze w której prawdą jest Φ wtedy i tylko wtedy, gdy należy do teorii Mod(Φ), czyli gdy należy do \(\overline{\Phi}\). Uzasadnia to określenie domknięcie semantyczne, gdyż \(\overline{\Phi}\) to wszystkie zdania prawdziwe, przy założeniu Φ.

Wygodne oznaczenie jest następujące: \(\Phi\models\phi\) mówiące dokładnie tyle, co \(\phi\in\overline{\Phi}\), czyli równoważnie ,φ jest prawdziwe przy założeniu Φ'. Można to czytać następująco: φ jest konsekwencją semantyczną Φ.