Języki pierwszego rzędu

Zaczniemy od przypomnienia podstawowych informacji dotyczących budowy języków pierwszego rzędu. Mówimy o językach, gdyż na gruncie logiki rozwa-ża się tylko ogólny schemat języka, w którym oprócz zmiennych indywidu-owych, używamy schematycznych symboli oznaczających nazwy (termy) lub własności i relacje (predykaty). Konkretne języki uzyskujemy wprowadzając zamiast nieokreślonych symboli (w istocie zmiennych, choć nie poddawanych kwantyfikacji) konkretne stałe pozalogiczne.

1 Podstawowe informacje o logikach wyższych rzędów, czy o teorii typów stanowiącej ich ogólne ujęcie, można znaleźć np. w Mostowski [100] lub Andrews [5], a wykorzystanie do nich RS w Takeuti [143].

8.1. ZAGADNIENIA SYNTAKTYCZNE 163 Definicja 8.1 (Słownik języka pierwszego rzędu) jest to suma rozłącz-nych zbiorów:

• V AR = {x, y, z, ...} – przeliczalny zbiór zmiennych indywiduowych • CON = {a, b, c, ...} – przeliczalny zbiór symboli nazw indywiduowych • F U N = {f, g, h, ...} – przeliczalny zbiór symboli funkcyjnych

• P RED = {A, B, C, ...} – przeliczalny zbiór symboli predykatów • LOG = {¬, ∧, ∨, →, ↔, ∀, ∃, =}

• AU X = {(, ), [, ]}

Uwaga 8.1: Zbiór V AR jest stały we wszystkich językach, jego elemen-ty mają za zadanie reprezentować nieokreślone obiekelemen-ty oraz występować w powiązaniu z kwantyfikatorami. Niektórzy autorzy, w tym Gentzen, wprowa-dzają konwencję graficznego rozróżnienia między (meta)zmiennymi niezwią-zanymi, a związanymi przez kwantyfikator. Dyskusję nad zaletami i wadami obu rozwiązań przeprowadzimy w rozdziale 9. Symboli ‘x’, ‘y’, (jak również ‘a’, ‘f’, ‘A’) będziemy też w dalszym ciągu, dla uproszczenia zapisu, używać jako metazmiennych w definicjach, zapisach schematów reguł itp. gdyż w rozważanych przez nas kontekstach nie prowadzi to do nieporozumień. Uży-wać będziemy jedynie dodatkowych metazmiennych τ_idla dowolnych termów (tak jak ϕ, ψ dla dowolnych formuł).

Uwaga 8.2: Kwantyfikatory zawsze występują w połączeniu z konkretnymi zmiennymi, np. ∀x, ∃y (dla dowolnego x, dla jakiegoś y) oraz z formułami, w których takie zmienne winny się znajdować (choć nie jest to konieczne, dopuszczamy przypadek tzw. pustej kwantyfikacji). Toteż oba kwantyfika-tory należą do grupy wyrażeń zwanych operatorami, których zadaniem jest “wiązanie” zmiennych w wyrażeniach.

Uwaga 8.3: W konkretnych językach zbiory CON, F U N, P RED są zazwy-czaj skończone i mogą być puste – zawierają one stałe pozalogiczne (nazwy, operacje, relacje). Elementy F U N i P RED mają określoną argumentowość (lub arność), którą często zaznacza się w górnym indeksie, np. f², A¹. Za-zwyczaj będziemy te indeksy pomijać wtedy, gdy argumentowość symbolu jest jasna z kontekstu. Intuicyjnie argumentowość predykatu oznacza, że re-prezentuje on relację zachodzącą między obiektami reprezentowanymi przez jego argumenty (predykaty dwu- i więcej argumentowe) lub własność obiek-tu (predykaty jednoargumentowe). Analogicznie dla symboli funkcyjnych.

W szczególności, identyczność = też jest predykatem dwuargumentowym. Zauważmy, że symbolu = będziemy dalej używać dwuznacznie zarówno dla reprezentowania stałej logicznej w rozważanych językach, jak i metajęzykowo – np. powyżej dla zaznaczenia, że pewien napis jest nazwą jakiegoś zbioru. Nie powinno to prowadzić do nieporozumień.

Uwaga 8.4: Zbiór CON można zredukować do zbioru F U N traktując na-zwy jako funkcje zero-argumentowe (analogicznie nie wyróżniamy jako osob-nej kategorii symboli zdaniowych traktując je jako predykaty zero-argumentowe). Zostawiamy je jako osobną kategorię, gdyż wygodnie będzie je wykorzystać dla reprezentacji systemu Gentzena jako symboli zmiennych nie związanych przez kwantyfikatory – por. rozdział 9.

Uwaga 8.5: Symbole w CON, F U N, P RED mają charakter parametrycz-ny, gdyż nie oznaczają konkretnych pozalogicznych stałych odpowiednich ka-tegorii. Operowanie nimi jest przydatne w ogólnych rozważaniach nad logiką pierwszego rzędu i dowolnymi językami. W konkretnych językach elemen-ty zbiorów CON, F U N, P RED będą oznaczane specjalnymi symbolami zamiast liter a, b, f, P itp.

Przykłady słowników konkretnych języków:

Teoria grup: CON = {1} , F U N = {·} (dwuargumentowy)

Teoria krat: CON = {1} , F U N = {×, +} (oba dwuargumentowe) Teoria mnogości: P RED = {∈} (dwuargumentowy)

Arytmetyka: CON = {0} , F U N = {s} (jednoargumentowy)

Oczywiście, w praktyce tak oszczędne języki są niewygodne i wprowa-dza się definicyjnie kolejne stałe pozalogiczne. Np. w teorii mnogości stałe ∅, operacje ∩, ∪, −, P i predykaty ⊆, ⊂ itp., w arytmetyce stałe 1, 2, 3, ... operacje +, ×, predykaty ≤, < itd.

Definicja 8.2 (zbioru termów (wyrażeń nazwowych) T ERM ) 1. V AR ∪ CON ⊆ T ERM ;

2. jeżeli fⁿ ∈ F U N , to fn(τ₁, ..., τ_n) ∈ T ERM , gdzie τ_i ∈ T ERM dla dowolnego i ≤ n (przy czym termy τ₁, ..., τn nie muszą być różne); 3. nic więcej nie należy do zbioru termów.

Uwaga 8.6: W praktyce będziemy pomijali zarówno indeks górny charak-teryzujący argumentowość f jak i nawiasy, jeżeli nie będzie to prowadzić do

8.1. ZAGADNIENIA SYNTAKTYCZNE 165 nieporozumień – ale nie zawsze da się tego uniknąć np. f xgya jest dwuznacz-ne. Można jednoznacznie je zapisać jako f xg(ya), gdy f² i g², lub f xg(y)a gdy f³, a g¹. Zauważmy też, że zazwyczaj dla konkretnych języków stosu-je się zapis infiksowy, a nie prefiksowy, tzn. zamiast ×xy napiszemy x × y. Przykłady termów w konkretnych językach:

sx, ssO, s(x + sy) + s(ss0 + z) – w arytmetyce x ∩ (y ∪ −z), P(x ∩ y) – w teorii mnogości Definicja 8.3 (zbioru formuł F OR)

1. jeżeli Pⁿ ∈ P RED, to Pn(τ₁, ..., τ_n) ∈ F OR, gdzie τ_i ∈ T ERM dla dowolnego i ≤ n (przy czym termy τ₁, ..., τ_n nie muszą być różne); 2. jeżeli τ₁, τ₂ ∈ T ERM , to τ₁ = τ₂ ∈ F OR;

3. jeżeli ϕ ∈ F OR, to ¬ϕ ∈ F OR;

4. jeżeli ϕ, ψ ∈ F OR, to (ϕ ∧ ψ), (ϕ ∨ ψ), (ϕ → ψ) ∈ F OR;

5. jeżeli ϕ ∈ F OR, to dla dowolnej x ∈ V AR, ∀x(ϕ), ∃x(ϕ) ∈ F OR; 6. nic więcej nie należy do zbioru formuł.

Formuła składająca się z predykatu i jego argumentów to formuła ato-mowa. Natomiast formuła ϕ występująca w formule ∀x(ϕ) to zasięg kwanty-fikatora ∀x (analogicznie dla ∃x).

Uwaga 8.7: W praktyce będziemy pomijali zarówno indeks górny charak-teryzujący argumentowość P jak i nawiasy, jeżeli nie będzie to prowadzić do nieporozumień, analogicznie jak w przypadku wyrażeń funkcyjnych (ale np. P f xy jest dwuznaczne – P f (xy) lub P f (x)y). Konwencje pomijania nawia-sów w formułach złożonych są takie same jak w języku KRZ, w szczególności kwantyfikatory traktujemy analogicznie jak negację, czyli zachowujemy na-wias jeżeli zasięg kwantyfikatora jest formułą złożoną, a pomijamy jeżeli jest formułą atomową. Będziemy też stosować konwencję pomijania symboli ta-kich samych kwantyfikatorów, jeżeli występują w bezpośrednim sąsiedztwie, tzn. zamiast ∀x∀y∀z(ϕ) napiszemy ∀xyz(ϕ).

Uwaga 8.8: W praktyce, dla konkretnych języków stosuje się zapis infiksowy, tzn. zamiast ≤ xy napiszemy x ≤ y. Przykłady formuł:

sx ≤ ssO, x ≤ sy → y = x, ∀xy(x + sy ≤ sx + sy) – w arytmetyce x ∈ y, x ⊆ x ∩ y, ∃x(x = y ∩ ∅) – w teorii mnogości

Uwaga 8.9: Dla powyższej definicji języka można przyjąć prostą definicję podformuły, tzn. dla formuły Qxϕ jej jedyną właściwą bezpośrednią podfor-mułą jest ϕ. Nie jest to jednak rozwiązanie wygodne dla naszych rozważań dlatego w następnym rozdziale zmodyfikujemy definicję podformuły dla for-muł z kwantyfikatorami.