Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

2.1 Abschnitte und Abschnittsfolgen

Theorem 2-11. Bijektivitat passender Folgen naturlicher Zahlen

Wenn й ∈ SEQ, ЭД ⊆ й und g eine passende Folge naturlicher Zahlen fur ЭД ist, dann ist g eine
Bijektion zwischen Dom(g) und Dom(2l).

Beweis: Sei й ∈ SEQ, ЭД ⊆ й und sei g eine passende Folgen naturlicher Zahlen fur ЭД.
Dann ist Ran(g) = Dom(2l) und g somit eine Surjektion von Dom(g) auf Dom(2l). Ferner
gilt, da g eine streng monotone Folge naturlicher Zahlen ist, dass g eine Injektion von
Dom(g) in Dom(2l) ist und somit ist g insgesamt eine Bijektion zwischen Dom(g) und
Dom(2l). ■

Theorem 2-12. Eindeutigkeit passender Folgen naturlicher Zahlen

Wenn й ∈ SEQ, ЭД ⊆ й und g, g' passende Folgen naturlicher Zahlen fur ЭД sind, dann: g = g'.

Beweis: Sei й ∈ SEQ, ЭД ⊆ й und seien g, g' passende Folgen naturlicher Zahlen fur ЭД.
Dann ist Ran(g) = Dom(2l) = Ran(g'). Ferner gilt mit Theorem 2-11 dass Dom(g) =
|Ran(g)| = |Ran(g')| = Dom(g'). Nun sind aber streng monoton wachsende Folgen naturli-
cher Zahlen mit gleichem Definitions- und Wertebereich identisch. Also ist g = g'. ■

Theorem 2-13. Nicht-rekursive Charakterisierung der passenden Folge fur einen Abschnitt
Wenn ЭД ein Abschnitt in й ist, dann ist {(l, min(Dom(2l))+l) | l < ∣Dom(2l)∣} eine passende
Folge naturlicher Zahlen fur ЭД.

Beweis: Sei й ∈ SEQ und ЭД ein Abschnitt in й. Dann ist ЭД ≠ 0. Der Beweis wird induk-
tiv uber die Machtigkeit von Dom(2l) gefuhrt. Sei Dom(2l) = 1. Dann ist Dom(2l) =
{min(Dom^))} und {(0, min(Dom^)))} ist eine passende Folge naturlicher Zahlen fur
ЭД und {(0, min(Dom(2l)))! = {(l, min(Dom^))+l) | l < 1} = {(l, min(Dom^))+l) | l <
∣Dom(a)∣}.

Gelte die Behauptung nun fur k ≥ 1 und sei ∣Dom(¾)∣ = k+1. Da ЭД eine endliche Funk-
tion ist, ist ЭД\ {(max(Dom( ЭД)), ⁴2l_max( ∣ >_om<a ,))J∣ = k. Auβerdem ist ЭД* = ЭД\{(max(Dom(ЭД)),
ЭДтахда^эд))} ein Abschnitt in й. Also ist nach I.V. g = {(l, min(Dom^*))+l) ∣ l <
∣Dom(¾*)∣} = {(l, min(Dom^))+l) ∣ l < ∣Dom^)∣-1} eine passende Folge naturlicher
Zahlen fur ЭД*. Sei g' = g ∪ {(|Dom(&)|-1, max(Dom^)))}. Dann ist Ran(g') = Dom^*)
∪ {max(Dom^))} = Dom(2l) und es ist Dom(g') = Dom(g) ∪ {Dom(g)} = Dom(g)+1 =
|Dom^*)|+1 = |Dom(&)|. Da ЭД ein Abschnitt in й ist, gilt sodann, dass
max(Dom^*))+1 = max(Dom^)). Damit ist g'(|Dom^)|-1) = max(Dom^*))+1 =

<<   55   56   57   58   59   60   61   >>

More intriguing information