1.1 Inventar und Syntax 25
Definition 1-24. Menge der (Satz)Sequenzen (SEQ)
SEQ = {й | й ist eine Sequenz}.
Definition 1-25. Konklusionszuordnung (K)
K = {(й, Γ) | й ∈ SEQ∖{0} und Γ = A‰)-ι)}.
Hinweis: Aus dieser Definition ergibt sich direkt, dass K eine Funktion auf SEQ∖{0} ist.
Definition 1-26. Zuordnung der Teilmenge einer Sequenz й, deren Glieder die Annahmesatze
von й sind (ANS)
ANS = {(й, X) | й ∈ SEQ und X = {(i, й,) | i ∈ Dom($) und й,. ∈ ASATZ}}.
Definition 1-27. Zuordnung der Menge der Annahmen (AN)
AN = {(й, X) | й ∈ SEQ und X = {Γ | Es gibt ein i ∈ Dom(ANS(φ)), so dass Γ = A(¾)}}.
Definition 1-28. Zuordnung der Teilmenge einer Sequenz й, deren Glieder die Folgerungs-
satze von й sind (FS)
FS = {(й, X) | й ∈ SEQ und X = {(i, й,) | i ∈ Dom($) und й, ∈ FSATZ}}.
Hinweis: Aus diesen Definitionen ergibt sich direkt, dass ANS, AN und FS Funktionen
auf SEQ sind.
Definition 1-29. Zuordnung der Menge der Teilterme der Glieder einer Sequenz й (TTSEQ)
TTSEQ = {(й, X) | й ∈ SEQ und X = U{TT(⅛i) | i ∈ Dom(£)}}.
Hinweis: Aus dieser Definition ergibt sich direkt, dass TTSEQ eine Funktion auf SEQ ist.
Definition 1-30. Zuordnung der Menge der Teilterme der Elemente einer Formelmenge X
(TTFM)
TTFM = {(X, Y) | X ⊆ FORM und Y = U{TT(Α) | Α ∈ X}}.
Hinweis: Aus dieser Definition ergibt sich direkt, dass TTFM eine Funktion auf
Pot(FORM) ist.