24 1 Zum grammatischen Rahmen
Definition 1-19. Die Menge der eigentlichen Ausdrucke (EAUS)
EAUS = GAUS ∪ QUANTOR ∪ TERM ∪ FORM ∪ SATZ.
Definition 1-20. Die Teilausdruckfunktion (TA)
TA ist eine Funktion auf EAUS und
(i) Wenn τ ∈ GAUS, dann TA(τ) = {τ},
(ii) Wenn rφ(θ0, .., θ,,-∣f ∈ FTERM, dann
TA(rφ(θo, ..., θn-ɪ)ɔ) = {rφ(θo, ..., θ^-ɪ)ɔ, φ} ∪ U{TA(θj) | i < n},
(iii) Wenn rΠξ^1 ∈ QUANTOR, dann TA( rΠξπ) = {rΠξπ, Π, ξ},
(iv) Wenn rΦ(θ0, .., θ,,-∣f ∈ AFORM, dann
TA(rΦ(θo, . ., " ) ■) = { rΦ(θo, . ., " ) ■, Φ} ∪ U{TA(θ.,) | i < n},
(v) Wenn r— Δπ ∈ JFORM, dann TA(r—Δ^l) = {r—Δ^l, r-π} ∪ TA(Δ),
(vi) Wenn r(Δ0 ψ Δ1)^l ∈ JFORM, dann
TA(r(Δo ψ Δ1D = { r(Δo ψ ʌɪ)ɔ, ψ} ∪ TA(Δo) ∪ TA(Δ1),
(vii) Wenn rΠξΔ"1 ∈ QFORM, dann
TA(rΠξΔπ) = {rΠξΔπ} ∪ TA(rΠξπ) ∪ TA(Δ), und
(viii) Wenn rΞΔπ ∈ SATZ, dann TA( rΞΔπ) = {rΞΔπ, Ξ} ∪ TA(Δ).
Definition 1-21. Die Teiltermfunktion (TT)
TT ist eine Funktion auf TERM ∪ FORM ∪ SATZ und fur alle τ ∈ TERM ∪ FORM ∪ SATZ
ist TT(τ) = TA(τ) ∩ TERM.
Definition 1-22. Die Teilformelfunktion (TF)
TF ist eine Funktion auf FORM ∪ SATZ und fur alle τ ∈ FORM ∪ SATZ ist TF(τ) = TA(τ) ∩
FORM.
Die folgenden Definitionen beschreiben die Syntax von L insoweit sie uber die Satzebene
hinausgeht. Wie oben bemerkt, wird - wie schon bei den vorhergehenden Definitionen -
der explizite Bezug auf L unterdruckt. Definition ɪ-23 zeichnet endliche Folgen aus Fol-
gerungs- und Annahmesatzen als (Satz)Sequenzen aus:
Definition 1-23. (Satz)Sequenzen (Metavariablen: ⅛ -6', -6*, .)
fɔ ist eine Sequenz
gdw
fɔ ist eine endliche Folge und fur alle i ∈ Dom(⅛) gilt: ⅛ ∈ SATZ.