Zastosowania

Funkcje ancestralne i układy twierdzeń podstawowych, którym one czynią zadość, znajdują obszerne zastosowania w rozbudowie systemu semantyki. Ograniczymy się tutaj do podania przykładu funkcji ancestralnych w czterech najprostszych wypadkach: I (n = 1, m = 1), II (n = 1, m - 2), III (n = 2, m = 1), IV (n = 2, m = 2), z którymi spotykamy się najczęściej.

Oznaczmy przez A (λ), B(α, λ) sądy: = λ0, = λ ∗ αα, Sądy te określają pewną funkcję ancestralną Φ (λ), którą w naszym wypadku możemy przyjąć jako definicję liczby naturalnej i oznaczać: Nat λ. Twierdzenia 1a, 2a przyjmują po dokonaniu elementarnych przekształceń następujący kształt:

⊦ Nat 0, ⊦ ⊃ Nat α Nat ∗ αα.

Podobnie Tw. 4 a prowadzi natychmiast do zasady indukcji arytmetycznej: Jeśli zachodzą twierdzenia: ⊦ Ψ (0), ⊦ ⊃ Ψ (α) Ψ (∗ α α), to zachodzi również twierdzenie ⊦ ⊃ Nat λ Ψ (λ).

Układ twierdzeń 1b - 4b odgrywa fundamentalną rolę w badaniach metamatematycznych. Pojęcie twierdzenia opisywanego systemu wprowadzamy tam jako funkcję ancestralną przy czym sąd A (λ) oznacza, że λ jest aksjomatem naszego systemu, a sąd B (α β, λ) stwierdza, że jego reguły postępowania prowadzą od twierdzeń α, β, do twierdzenia λ. Pragnę tu zaznaczyć, że we wszystkich niemal dowodach metamatematycznych opieramy się na Tw. 4b.

Widzieliśmy, że pojęcie liczby naturalnej stanowi szczegółowy przykład funkcji ancestralne] (n = 1, m = 1), Wykażemy obecnie, że również działania na liczbach naturalnych możemy wprowadzić przy pomocy funkcji ancestralnych (n = 1, m = 2). Konstrukcją pojęcia liczby naturalnej i działań arytmetycznych zajmowałem się w "Arytmetyce semantycznej". Podstawowe twierdzenia opisujące indukcyjną strukturę danego działania otrzymujemy natychmiast z Tw. 1c i 2c. Twierdzenia o istnieniu wyniku danego działania i jego jednoznaczności uzyskamy łatwo, stosując indukcję arytmetyczną i wykorzystując ponadto Tw. 3c. przy dowodzie jednoznaczności. Ograniczymy się tu do omówienia działania dodawania, gdyż działania dalsze nie przynoszą nic istotnie nowego. Oznaczamy przez A(λ 1 λ 2), B (α 1 α 2, λ 1 λ 2) sądy:

Sądy te wyznaczają nam pewną funkcję ancetralną Φ(λ 1 λ 2).

Wprowadzamy teraz skrót +λ λ 1 λ 2 na oznaczenie sądu ∧ Nat λ Φ (λ 1 λ 2). Sąd +λ λ 1 λ 2 czytamy: λ 2 jest sumą liczb naturalnych λ λ 1".

Tw. 1c, 2c, 3c przyjmują po dokonaniu elementarnych przekształceń następujący kształt:


⊦ ⊃ Nat λ+λ0λ
⊦ ⊃+λα1α2+λ∗α1α1∗ α2α2
⊦ ⊃+λ∗α1α1α2∃a2∧+λα1a22a2a2

Istnienie wyniku dodawania i jego jednoznaczność wynikają już łatwo z powyższych twierdzeń przez zastosowanie indukcji arytmetycznej.

IV. Niech będą dane dwa dowolne sądy kształtu:

A(λ), B1 α 21 β 2; λ )

Oznaczamy przez A'1 λ 2), B'1 α 21 β 2; λ 1λ 2) sądy: ∧ = λ 1 0 A2), ∧ = λ 1∗ α 1β 1 B1 α 21 β 2; λ 2).


⊦ ⊃ A2) Φ(0λ2)
⊦ ⊃ ∧ Φ(α1α2) ∧ Φ(β1β2) B1 α 21 β 2; λ2 ) Φ(∗α 1β 1λ2)
⊦ ⊃ Φ(∗α 1β 1λ2)∃a2b2∧Φ(α 1a2)∧Φ(β 1b2)B1 a 21 b 2; λ2 )

Konstrukcją funkcji spełniającej powyższy układ twierdzeń zajmowałem się w "Podstawach semantyki". Twierdzenia te pozwalają już łatwo wyprowadzić dalsze związki, które tam uzyskałem. Widzimy zatem, że rekursja semantyczna sprowadza się również do funkcji ancestralnej, tylko nieco bardziej zawiłej (n = 2, m = 2).

Funkcje ancestralne odpowiadające wypadkom bardziej złożonym (n > 2, m > 2) znalazły liczne zastosowanie w pracy p. Herzberga o podstawach rachunku prawdopodobieństwa, która wkrótce ukaże się w druku.