Metoda aksjomatyczna

Metoda aksjomatyczna

Jerzy Pogonowski

Zakªad Logiki i Kognitywistyki UAM www.kognitywistyka.amu.edu.pl http://logic.amu.edu.pl/index.php/Dydaktyka

pogon@amu.edu.pl

MDTiAR 27x2015

Wst¦p

Plan na dzi±

Dzisiaj wykorzystamy zaªo»enie, »e studenci przeszli kursy: Logika I oraz Logika II.

Przypomnimy, na czym polega aksjomatyczna metoda dowodzenia twierdze«.

Udowodnimy twierdzenie o dedukcji (KRZ).

Udowodnimy twierdzenia o trafno±ci oraz peªno±ci metody aksjomatycznej (KRZ).

Przypomnimy operacje na relacjach.

Podamy aksjomatyk¦ Tarskiego dla rachunku relacji.

Dla t¦skni¡cych za logik¡ pierwszego rz¦du: chi«skie przysªowie mówi, »e cierpliwy dostaje wszystko na czas.

Metoda aksjomatyczna w KRZ

Dawno temu, w odlegªej galaktyce. . .

Metoda Aksjomatyczna w KRZ

Metoda aksjomatyczna w KRZ Uwagi historyczne

Pionierzy

Gottlob Frege: Begrisschrift (1879)

Alfred N. Whitehead, Bertrand Russell: Principia Mathematica (19101913)

David Hilbert, Wilhelm Ackermann: Grundzüge der Theoretischen Logik (1928)

David Hilbert, Paul Bernays: Grundlagen der Mathematik (1934, 1939)

David Hilbert: Grundlagen der Geometrie (1899)

Postulaty±ci Ameryka«scy (Edward V.Huntington, Oswald Veblen) Polscy logicy (Stanisªaw Le±niewski, Adolf Lindenbaum, Jan

Šukasiewicz, Alfred Tarski)

Metoda aksjomatyczna w KRZ Metoda aksjomatyczna: poj¦cie dowodu

Konsekwencja aksjomatyczna

W ustalonym j¦zyku wybieramy:

zestaw aksjomatów (przyjmowanych bez dowodu) zestaw (pierwotnych) reguª wnioskowania.

Oba te zbiory musz¡ by¢ podane w sposób efektywny.

Dowodem w systemie aksjomatycznym A jest dowolny sko«czony ci¡g formuª (ψ1, ψ₂, . . . , ψ_n) taki, »e ka»da formuªa ψi jest b¡d¹

aksjomatem, b¡d¹ wnioskiem reguªy wnioskowania o przesªankach wyst¦puj¡cych wcze±niej w tym ci¡gu.

Wyprowadzeniem ze zbioru formuª S w systemie aksjomatycznym A jest dowolny sko«czony ci¡g formuª (ψ₁, ψ₂, . . . , ψ_n) taki, »e ka»da formuªa ψ_i jest b¡d¹ aksjomatem, b¡d¹ elementem zbioru S, b¡d¹ wnioskiem reguªy wnioskowania o przesªankach wyst¦puj¡cych wcze±niej w tym ci¡gu.

Metoda aksjomatyczna w KRZ Metoda aksjomatyczna: poj¦cie dowodu

Konsekwencja aksjomatyczna: komentarze

Tez¡ systemu aksjomatycznego A jest ka»da formuªa ψ, która jest ostatnim elementem jakiego± dowodu. Piszemy wtedy: `Aψ.

Formuªa ψ jest A-konsekwencj¡ zbioru formuª S, gdy ψ jest ostatnim elementem jakiego± wyprowadzenia z S. Piszemy wtedy: S `Aψ

Za aksjomaty przyjmujemy formuªy b¡d¹ schematy formuª. W pierwszym przypadku w±ród reguª wnioskowania uwzgl¦dniamy reguª¦

podstawiania RP: _ϕ[p^ϕ_i/ψ] (formuªy ψ za zmienn¡ p_i w formule ϕ).

W razie potrzeby, korzysta si¦ z reguªy zast¦powania denicyjnego.

Aksjomaty charakteryzuj¡ znaczenie staªych logicznych.

Wzbogacamy ±rodki inferencyjne systemu poprzez pokazanie, »e pewne reguªy s¡ w nim wyprowadzalne (wtórne).

Metoda aksjomatyczna w KRZ Dla uciechy

Aksjomatyka w stylu Hilberta-Bernaysa

Kurs Logika I wykorzystywaª zapewne tego rodzaju aksjomatyk¦ KRZ:

Reguªy wnioskowania: MP ^{ϕ ϕ→ψ}_ψ , RP _ϕ[p^ϕ_i/ψ]

Aksjomaty:

p₁ → (p₂→p₁)

(p1→ (p2 →p3)) → ((p1 →p2) → (p1 →p3))

(p1→p2) → (¬p2 → ¬p1)

¬¬p₁ →p₁ p₁ → ¬¬p₁

Metoda aksjomatyczna w KRZ Dla uciechy

Aksjomatyka w stylu Hilberta-Bernaysa

(p₁∧p₂) →p₁ (p₁∧p₂) →p₂

(p1→p2) → ((p1→p3) → (p1 → (p2∧p3))) p₁ → (p₁∨p₂)

p₂ → (p₁∨p₂)

(p₁→p₂) → ((p₃→p₂) → ((p₁∨p₃) →p₂))

(p₁≡p₂) → (p₁→p₂) (p1≡p2) → (p2→p1)

(p₁→p₂) → ((p₂→p₁) → (p₁ ≡p₂))

Metoda aksjomatyczna w KRZ Dla uciechy

Dwa polskie przykªady

Aksjomatyka Jana Šukasiewicza (implikacyjno-negacyjna) (ϕ → ψ) → ((ψ → χ) → (ϕ → χ))

(¬ϕ → ϕ) → ϕ ϕ → (¬ϕ → ψ)

Reguªa wnioskowania MP: ^{ϕ ϕ→ψ}_ψ

Aksjomatyka Adama Wiegnera (pierwotne: ∧ oraz ¬) p → (p ∧ p)

(p ∧ q) → p (p ↑ q) → (q ↑ p)

(p → q) → ((q ↑ r) → (p ↑ r))

Reguªy wnioskowania: MP, RP, zast¦powanie denicyjne

Aksjomatyka KRZ w Fitting 1990 Aksjomaty

Propozycja w Fitting 1990

Schematy aksjomatów:

1 ϕ → (ψ → ϕ)

2 (ϕ → (ψ → χ)) → ((ϕ → ψ) → (ϕ → χ))

3 ⊥→ ϕ

4 ϕ → >

5 ¬¬ϕ → ϕ

6 ϕ → (¬ϕ → ψ)

7 α → α₁

8 α → α₂

9 (β₁→ ϕ) → ((β₂→ ϕ) → (β → ϕ))

Reguªa wnioskowania: ^{ϕ ϕ→ψ}_ψ (modus ponens, reguªa odrywania, MP)

Aksjomatyka KRZ w Fitting 1990 Przykªad dowodu

Prawo to»samo±ci: p → p

1 (p → ((p → p) → p)) → ((p → (p → p)) → (p → p)) Ax.2

2 p → ((p → p) → p) Ax.1

3 (p → (p → p)) → (p → p) MP: 1,2

4 p → (p → p) Ax. 1

5 p → p MP: 3,4

W dowodzie korzystano tylko z dwóch pierwszych aksjomatów.

Tak samo dowodzimy schematu prawa to»samo±ci: ψ → ψ.

Ten prosty dowód ukazuje dwie trudno±ci metody aksjomatycznej:

Jak zacz¡¢ dowód aksjomatyczny?

W dowodzie wyst¦puj¡ formuªy bardziej zªo»one od dowodzonej tezy.

Aksjomatyka KRZ w Fitting 1990 Przykªad dowodu

Jeszcze jeden przykªad: (¬ϕ → ϕ) → ϕ

Za β-formuª¦ w schemacie aksjomatów 9 we¹my formuª¦: ¬ϕ → ϕ.

Wtedy β1 jest formuª¡ ¬¬ϕ, a β2 formuª¡ ϕ. Otrzymujemy wi¦c:

(¬¬ϕ → ϕ) → ((ϕ → ϕ) → ((¬ϕ → ϕ) → ϕ)).

¬¬ϕ → ϕpodpada pod schemat aksjomatów 5.

ϕ → ϕjest tez¡ (jak ju» pokazali±my), czyli doª¡czy¢ mo»na w tym miejscu kroki dowodu ϕ → ϕ.

Dwukrotne zastosowanie reguªy odrywania daje (¬ϕ → ϕ) → ϕ.

‚wiczenie. Zapisz powy»sz¡ argumentacj¦ w postaci formalnego dowodu.

Czy pami¦tasz, »e (¬ϕ → ϕ) → ϕ to consequentia mirabilis (prawo Claviusa)?

Twierdzenie o dedukcji Twierdzenie

Twierdzenie o dedukcji wprost (KRZ)

Oznaczenia: niech `_ph b¦dzie relacj¡ konsekwencji wyznaczon¡ przez podany wy»ej zestaw aksjomatów i reguª¦ odrywania.

Twierdzenie o dedukcji.

S ∪ {ϕ} `<sub>ph</sub> ψ wtedy i tylko wtedy, gdy S `_ph (ϕ → ψ).

Uwagi.

Implikacja odwrotna wynika z monotoniczno±ci `_ph (Fitting pisze: jest trywialna).

W dowodzie implikacji prostej wykorzystamy pierwsze dwa aksjomaty systemu (oraz reguª¦ odrywania).

Twierdzenie o dedukcji udowodnili (niezale»nie od siebie) Herbrand i Tarski.

Twierdzenie o dedukcji Dowód twierdzenia o dedukcji

Dowód twierdzenia o dedukcji

Zaªó»my, »e S ∪ {ϕ} `_phψ.

Niech χ₁, χ₂, . . . , χ_n b¦dzie wyprowadzeniem ψ z S ∪ {ϕ}.

Wtedy χ_n jest identyczna z ψ.

Ka»dy element ci¡gu (χ₁, χ₂, . . . , χ_n)jest b¡d¹ aksjomatem, b¡d¹ elementem S, b¡d¹ wnioskiem reguªy odrywania o przesªankach b¦d¡cych wcze±niejszymi elementami tego ci¡gu.

Tworzymy ci¡g formuª (∗): (ϕ → χ₁, ϕ → χ₂, . . . , ϕ → χ_n).

Ostatnim jego elementem jest zatem ϕ → ψ.

Ci¡g ten nie musi by¢ wyprowadzeniem, ale:

Rozszerzymy ten ci¡g do ci¡gu, który b¦dzie wyprowadzeniem ϕ → ψ z S, co zako«czy dowód twierdzenia o dedukcji.

Twierdzenie o dedukcji Dowód twierdzenia o dedukcji

Dowód twierdzenia o dedukcji

χ_i jest aksjomatem lub elementem S. Wtedy przed formuª¡ ϕ → χ_i wstawiamy do ci¡gu (∗) formuªy: χi oraz χi → (ϕ → χ_i).

χ_i jest formuª¡ ϕ. Wtedy przed formuª¡ ϕ → χ_i wstawiamy do ci¡gu (∗)formuªy tworz¡ce dowód formuªy ϕ → ϕ.

χ_i jest wnioskiem reguªy odrywania o przesªankach b¦d¡cych wcze±niejszymi elementami tego ci¡gu, czyli istniej¡ χ_j, χ_k takie, »e j, k < i oraz χ_k jest formuª¡ χ_j → χ_i (czyli ϕ → χ_k jest formuª¡

ϕ → (χ_j → χ_i)).

Wtedy przed formuª¡ ϕ → χi wstawiamy do ci¡gu (∗) formuªy:

(ϕ → (χ_j → χ_i)) → ((ϕ → χ_j) → (ϕ → χ_i))(aksjomat) oraz (ϕ → χ_j) → (ϕ → χ_i).

Wtedy ϕ → χ_i jest wnioskiem reguªy odrywania o przesªankach wyst¦puj¡cych wcze±niej w tak rozszerzonym ci¡gu.

Twierdzenie o dedukcji Wykorzystanie twierdzenia o dedukcji

Korzy±ci z twierdze« o dedukcji

Zauwa»my, »e dowód twierdzenia o dedukcji byª konstruktywny:

podano przepis, jak wyprowadzenie ψ z {ϕ} przeksztaªci¢ na dowód ϕ → ψ.

Korzystanie z twierdzenia o dedukcji bardzo uªatwia dowodzenie w systemach aksjomatycznych.

‚wiczenia. Wykorzystuj¡c twierdzenie o dedukcji, poka», »e:

`_ph (ϕ → (ψ → χ)) → (ψ → (ϕ → χ)) prawo komutacji

`_ph (ϕ → (ψ → χ)) → ((ϕ ∧ ψ) → χ) prawo importacji

`_ph (ϕ → ψ) → ((ψ → χ) → (ϕ → χ)) sylogizm hipotetyczny

Twierdzenie o dedukcji Oktawa twierdze« o dedukcji

Studenci poznali wcze±niej nast¦puj¡ce twierdzenia o dedukcji w KRZ (|=_krz to relacja wynikania logicznego w KRZ, `_krz to konsekwencja aksjomatyczna w KRZ, której u»ywano):

Semantyczne twierdzenie o dedukcji wprost: S ∪ {ϕ} |=_krz ψ wtedy i tylko wtedy, gdy S |=_krz (ϕ → ψ).

Syntaktyczne twierdzenie o dedukcji wprost: S ∪ {ϕ} `<sub>krz</sub> ψ wtedy i tylko wtedy, gdy S `_krz (ϕ → ψ).

Semantyczne twierdzenie o dedukcji nie wprost: S ∪ {¬ϕ} |=_krz⊥ wtedy i tylko wtedy, gdy S |=_krz ϕ.

Syntaktyczne twierdzenie o dedukcji nie wprost: S `<sub>krz</sub> ¬ϕwtedy i tylko wtedy, gdy S ∪ {ϕ} `_krz⊥.

Powy»ej udowodnili±my drugie z nich dla `<sub>krz</sub> = `_ph.

W przypadku KRP potrzebne jest dodatkowe zaªo»enie (»e ϕ jest zdaniem) w syntaktycznych twierdzeniach o dedukcji.

Trafno±¢ metody aksjomatycznej

Trafno±¢

Twierdzenie o trafno±ci. Je±li S `_ph ϕ, to S |=_krz ϕ.

Ka»dy aksjomat jest tautologi¡ KRZ. ‚wiczenie: sprawd¹.

Je±li ϕ oraz ϕ → ψ s¡ tautologiami KRZ, to ψ jest tautologi¡ KRZ.

‚wiczenie: sprawd¹. A mo»e pami¦tasz semantyczne twierdzenie o odrywaniu w KRZ?

Tak wi¦c, ka»dy wiersz (w szczególno±ci: ostatni wiersz) dowolnego dowodu jest tautologi¡ w KRZ.

A zatem, je±li ϕ jest tez¡ rozwa»anego sytemu, to jest tautologi¡ KRZ.

Fitting pisze (Fitting 1990, 74): This argument extends easily to derivations as well; we do not give details, co przetªumaczymy tak:

Przez indukcj¦ po dªugo±ci wyprowadzenia ϕ z S ªatwo pokaza¢, »e ka»dy jego krok wynika logicznie z S.

Peªno±¢ metody aksjomatycznej

Peªno±¢

Twierdzenie o peªno±ci. Je±li S |=_krz ϕ, to S `_ph ϕ.

W dowodzie wykorzystamy: pewn¡ zdaniow¡ wªasno±¢ niesprzeczno±ci oraz Twierdzenie o Istnieniu Modelu.

Niech ϕ b¦dzie dowoln¡ formuª¡. Zbiór S nazwiemy Hilbertowsko ϕ-sprzecznym, gdy S `_phϕ. Zbiory, które nie s¡ Hilbertowsko ϕ-sprzeczne nazywamy Hilbertowsko ϕ-niesprzecznymi.

Lemat. Dla dowolnej formuªy ϕ, rodzina wszystkich zbiorów Hilbertowsko ϕ-niesprzecznych jest zdaniow¡ wªasno±ci¡

niesprzeczno±ci.

Dowód. Niech S b¦dzie zbiorem Hilbertowsko ϕ-niesprzecznym. Oznacza to, »e nie zachodzi S `_phϕ. Trzeba pokaza¢, »e S speªnia wszystkie warunki nakªadane na elementy zdaniowej wªasno±ci niesprzeczno±ci.

Peªno±¢ metody aksjomatycznej

Dowód lematu

Proponujemy dowód nie wprost (dla ka»dego warunku).

Gdyby ⊥∈ S, to mieliby±my S `<sub>ph</sub>⊥. Aksjomatem jest ⊥→ ϕ, a zatem mieliby±my S `_ph ϕ, w sprzeczno±ci z zaªo»eniem o Hilbertowskiej ϕ-niesprzeczno±ci S. Tak wi¦c, ⊥/∈ S.

Gdyby ¬> ∈ S, to mieliby±my S `<sub>ph</sub> ¬>. Pod schemat aksjomatu 4 podpada ¬> → >, a zatem S `_ph>. Pod schemat aksjomatu 6 podpada > → (¬> → ϕ), a zatem S `_phϕ, w sprzeczno±ci z zaªo»eniem o Hilbertowskiej ϕ-niesprzeczno±ci S. Tak wi¦c, ¬> /∈ S.

Przypu±¢my, »e S ∪ {ψ} jest Hilbertowsko ϕ-sprzeczny, czyli S ∪ {ψ} `<sub>ph</sub> ϕ. Poka»emy, »e wtedy S ∪ {¬¬ψ} jest Hilbertowsko ϕ-sprzeczny. Aksjomat 5 daje: ¬¬ψ → ψ, a twierdzenie o dedukcji i poczynione przypuszczenie daj¡: S `_ph(ψ → ϕ). Na mocy prawa sylogizmu hipotetycznego: S `<sub>ph</sub> (¬¬ψ → ϕ). Na mocy twierdzenia o dedukcji: S ∪ {¬¬ψ} `_phϕ, czyli S ∪ {¬¬ψ} jest Hilbertowsko ϕ-sprzeczny.

Peªno±¢ metody aksjomatycznej

Dowód lematu

Przypu±¢my, »e S ∪ {α₁, α₂}jest Hilbertowsko ϕ-sprzeczny, czyli:

S ∪ {α₁, α₂} `<sub>ph</sub> ϕ. Poka»emy, »e wtedy S ∪ {α} jest Hilbertowsko ϕ-sprzeczny, czyli »e: S ∪ {α} `_phϕ.

Skoro S ∪ {α₁, α₂} `_ph ϕ, to (twierdzenie o dedukcji!):

S ∪ {α1} `<sub>ph</sub> (α<sub>2</sub>→ ϕ) oraz S `_ph (α₁→ (α₂ → ϕ)). Na mocy prawa importacji (zob. ¢wiczenie) oraz MP:

(α₁ → (α₂ → ϕ)) → ((α₁∧ α₂) → ϕ)mamy S `_ph((α₁∧ α₂) → ϕ) Na mocy aksjomatów α → α1 oraz α → α2, prawa mno»enia

nast¦pników (α → α₁) → ((α → α₂) → (α → (α₁∧ α₂)))oraz MP mamy S `_ph(α → (α₁∧ α₂))

Na mocy prawa sylogizmu hipotetycznego: S `<sub>ph</sub> (α → ϕ). Twierdzenie o dedukcji daje: S ∪ {α} `_phϕ.

Peªno±¢ metody aksjomatycznej

Dowód lematu

Przypu±¢my, »e S ∪ {β₁}oraz S ∪ {β₂}s¡ Hilbertowsko ϕ-sprzeczne.

Oznacza to, »e: S ∪ {β₁} `<sub>ph</sub>ϕoraz S ∪ {β<sub>2</sub>} `_ph ϕ. Poka»emy, »e wtedy S ∪ {β} jest Hilbertowsko ϕ-sprzeczny.

Skoro S ∪ {β1} `<sub>ph</sub> ϕ, to (twierdzenie o dedukcji!) S `_ph (β₁→ ϕ). Skoro S ∪ {β₂} `<sub>ph</sub> ϕ, to (twierdzenie o dedukcji!) S `_ph (β₂→ ϕ). Przypomnijmy schemat aksjomatów 9:

(β₁→ ϕ) → ((β₂→ ϕ) → (β → ϕ))

Dwukrotne zastosowanie reguªy odrywania daje: S `<sub>ph</sub> (β → ϕ). Na mocy twierdzenia o dedukcji: S ∪ {β} `_phϕ, czyli S ∪ {β} jest Hilbertowsko ϕ-sprzeczny.

Peªno±¢ metody aksjomatycznej

Dowód twierdzenia o peªno±ci

Zaªó»my, »e S |=_krz ϕ i przypu±¢my (dla dowodu nie wprost), »e nie zachodzi S `_phϕ.

Oznacza to, »e S jest Hilbertowsko ϕ-niesprzeczny.

Wynika z tego, »e tak»e S ∪ {¬ϕ} jest Hilbertowsko ϕ-niesprzeczny.

Gdyby bowiem tak nie byªo, to mieliby±my S ∪ {¬ϕ} `<sub>ph</sub> ϕ, a zatem tak»e (twierdzenie o dedukcji!) S `_ph(¬ϕ → ϕ). Poniewa» (jak wcze±niej pokazano) tez¡ jest (¬ϕ → ϕ) → ϕ, to wynikaªoby z tego,

»e S `_phϕ, co przeczy Hilbertowskiej ϕ-niesprzeczno±ci S.

Na mocy udowodnionego przed chwil¡ lematu oraz Twierdzenia o Istnieniu Modelu S ∪ {¬ϕ} jest speªnialny.

W konsekwencji, nie zachodzi S |=_krz ϕ, co ko«czy dowód twierdzenia o peªno±ci.

Aksjomatyczne uj¦cie rachunku relacji

Z cyklu: jak Polacy tworzyli logik¦ wspóªczesn¡

Aksjomatyka Rachunku Relacji

Aksjomatyczne uj¦cie rachunku relacji Operacje na relacjach

Operacje na relacjach

Znane z kursu Logika I: operacje mnogo±ciowe na relacjach.

Zªo»eniem relacji R ⊆ X × Y i S ⊆ Y × Z nazywamy relacj¦

R ◦ S ⊆ X × Z zdeniowan¡ wzorem: xR ◦ Sz wtedy i tylko wtedy, gdy istnieje y ∈ Y taki, »e xRy i ySz.

Przechodnim domkni¦ciem relacji R nazywamy relacj¦ R^tr zdeniowan¡ indukcyjnie:

R¹=R Rⁿ⁺¹=Rⁿ◦R R^tr =S

n Rⁿ.

Wzgl¦dna suma: x R†S y wtedy i tylko wtedy, gdy dla ka»dego z zachodzi: xRz lub zSy.

Oswoimy si¦ z tymi operacjami na konwersatorium.

Aksjomatyczne uj¦cie rachunku relacji Operacje na relacjach

Operacje na relacjach a wªasno±ci relacji

Niech R ⊆ X × X . Przez id_X rozumiemy relacj¦ identyczno±ci w X . R jest zwrotna wtedy i tylko wtedy, gdy id_X ⊆R

R jest przeciwzwrotna wtedy i tylko wtedy, gdy R ∩ idX = ∅ R jest symetryczna wtedy i tylko wtedy, gdy R = R⁻¹ R jest asymetryczna wtedy i tylko wtedy, gdy R ∩ R⁻¹= ∅ R jest antysymetryczna wtedy i tylko wtedy, gdy R ∩ R⁻¹ ⊆id_X R jest przechodnia wtedy i tylko wtedy, gdy R ◦ R ⊆ R

R jest przechodnia wtedy i tylko wtedy, gdy R = R^tr

R jest spójna wtedy i tylko wtedy, gdy R ∪ R⁻¹∪id_X =X × X .

‚wiczenie: które wªasno±ci s¡ zachowywane przez operacje na relacjach? Jakie struktury tworz¡: wszystkie porz¡dki (cz¦±ciowe, liniowe), wszystkie równowa»no±ci, itd. na danym zbiorze?

Aksjomatyczne uj¦cie rachunku relacji Aksjomaty

Aksjomaty Tarskiego

Matematyczny rachunek relacji zapocz¡tkowany zostaª w pracach Peirce'a oraz Schrödera. Aksjomatyczne uj¦cie tego rachunku podaª Tarski.

Aksjomatyka Tarskiego zapisana jest w j¦zyku u»ywaj¡cym (oprócz funktorów prawdziwo±ciowych, predykatu identyczno±ci .

=i zmiennych dla relacji) nast¦puj¡cych symboli operacji podanych w kontek±cie ich u»ycia wraz z (zamierzon¡) interpretacj¡ w uniwersum U:

Symbol Interpretacja Symbol Interpretacja

R + S R ∪ S 0 ∅

R · S R ∩ S 1 U × U

R; S R ◦ S 0⁰ di_U = (U × U) − id_U

R‡S R†S 1⁰ id_U

R^g R⁻¹ R (U × U) − R

R .

=S R = S

Aksjomatyczne uj¦cie rachunku relacji Aksjomaty

(1) (R .

=S ∧ R .

=T ) → S .

=T (2) R .

=S → (R + T .

=S + T ∧ R · T .

=S · T ) (3) R + S .

=S + R ∧ R · S .

=S · R (4) (R + S) · T .

= (R · T ) + (S · T ) ∧ (R · S) + T .

= (R + T ) · (S + T ) (5) R + 0 .

=R ∧ R · 1 .

=R (6) R + R .

=1 ∧ R · R .

=0 (7) ¬(1 .

=0) (8) (R^g)^g .

=R (9) (R; S)^g .

= (S)^g; (R)^g (10) R; (S; T ) .

= (R; S); T (11) R; 1⁰ .

=R (12) R; 1 .

=1 ∨ 1; R .

=1 (13) (R; S) · (T )^g .

=0 → (S; T ) · (R)^g .

=0 (14) 0⁰ .

=1⁰ (15) R‡S .

= (R); (S).

Aksjomatyczne uj¦cie rachunku relacji Aksjomaty

Twierdzenie Schrödera-Tarskiego

Twierdzenie Schrödera-Tarskiego. Na bazie aksjomatów (1)(15) ka»de zdanie (j¦zyka rachunku relacji) jest inferencyjnie równowa»ne zdaniu o postaci R .

=1.

Zakªadamy przy tym aksjomatyk¦ KRZ.

Reguªy: modus ponens oraz reguªy dla predykatu identyczno±ci .

=. Niech <(U) oznacza rodzin¦ wszystkich relacji dwuargumentowych na zbiorze U, czyli <(U) = {R : R ⊆ U × U}. Wtedy ukªad

(<(U), ∪, ∩, ◦, †, =,⁻¹, −,U × U, ∅, id_U,di_U) speªnia wszystkie aksjomaty (1)(15), przy interpretacji podanej w powy»szej tabeli.

Teraz rozwa»ymy problem ogólniejszy:

Aksjomatyczne uj¦cie rachunku relacji Algebry relacyjne

‘wiaty relacji

Algebr¡ relacyjn¡ nazywamy ka»dy ukªad o postaci (A, +,⁻, ; ,^∨,1⁰), gdzie A jest zbiorem, 1⁰ elementem A, a operacje +,⁻, ; ,^∨ speªniaj¡ warunki:

(R1) x + y = y + x przemienno±¢ +

(R2) x + (y + z) = (x + y) + z ª¡czno±¢ +

(R3) x + y + x + y = x aksjomat Huntingtona

(R4) x; (y; z) = (x; y); z ª¡czno±¢ ;

(R5) (x + y); z = (x; z) + (y; z) dystrybutywno±¢ ; wzgl¦dem + (R6) x; 1⁰ =x 1⁰ jest elementem identyczno±ciowym wzgl¦dem ;

(R7) (x^∨)^∨=x idempotencja ^∨

(R8) (x + y)^∨=x^∨+y^∨ dystrybutywno±¢ ^∨ wzgl¦dem + (R9) (x; y)^∨ =y^∨;x^∨ inwolucyjna dystrybutywno±¢ ^∨ (R10) (x^∨;x; y) + y = y aksjomat Tarskiego-De Morgana.

Aksjomatyczne uj¦cie rachunku relacji Reprezentowalno±¢

Wielkie pytanie

Je±li (A, +,⁻, ; ,^∨,1⁰) jest algebr¡ relacyjn¡, to deniujemy:

x · y = x + y, x − y = x − y, 0 = 1⁰+1⁰, 1 = 1⁰+1⁰.

Wtedy (A, +, ·,⁻,0, 1) jest algebr¡ Boole'a.

Algebra relacyjna jest reprezentowalna, gdy jest izomorczna z podalgebr¡ algebry <(U) wszystkich relacji dwuargumentowych na jakim± zbiorze U.

Czy ka»dy model aksjomatów (1)(15) jest algebr¡ reprezentowaln¡?

Odpowied¹: NIE (Lyndon). Istniej¡ modele aksjomatów (1)(15), które nie mog¡ by¢ homomorcznie wªo»one w »adn¡ algebr¦ <(U).

Tarski. Równo±ciowa teoria reprezentowalnych algebr relacyjnych jest nierozstrzygalna.