22 1 Zum grammatischen Rahmen
freien Variablen eines Terms oder einer Formel und auf dieser Basis in Definition 1-16
die Satze bestimmt werden.
Definition 1-13. Zuordnung der Menge der Variablen, die in einem Term θ oder einer Formel
Γ frei vorkommen (FV)
FV ist eine Funktion auf TERM ∪ FORM und
(i) Wenn α ∈ KONST, dann FV(α) = 0,
(ii) Wenn β ∈ PAR, dann FV(β) = 0,
(iii) Wenn ξ ∈ VAR, dann FV(ξ) = {ξ},
(iv) Wenn rφ(θ0, .., θn-∣)π ∈ FTERM, dann
FV(rφ(θo, . ., θn-ɪ)ɔ) = U{FV(θ.,) | i < n},
(v) Wenn rΦ(θ0, ., θn-∣)π ∈ AFORM, dann
FV(rΦ(θo, ., θn-ɪ)ɔ) = U{FV(θi) | i < n},
(vi) Wenn r—Δ"1 ∈ JFORM, dann FV(r- Δπ) = FV(Δ),
(vii) Wenn r(Δ0 ψ Δ1)^l ∈ JFORM, dann FV(r(Δ0 ψ Δ1)^l) = FV(Δ0) ∪ FV(Δ1),
und
(viii) Wenn rΠξΔπ ∈ QFORM und, dann FV( rΠξΔπ) = FV(Δ)∖{ξ}.
Definition 1-14. Die Menge der geschlossenen Terme (GTERM)
GTERM = {θ | θ ∈ TERM und FV(θ) = 0}.
Hinweis: Man beachte, dass Parameter nach Definition ∣-∣4 geschlossene Terme sind.
Definition 1-15. Die Menge der geschlossenen Formeln (GFORM)
GFORM = {Δ | Δ ∈ FORM und FV(Δ) = 0}.
Geschlossene Formeln werden auch als Aussagen angesprochen. Man beachte, dass ge-
schlossene Formeln durchaus Parameter zum Teilausdruck (siehe Definition ∣-20) haben
konnen.
Definition 1-16. Die Menge der Satze (SATZ; Metavariablen: Σ, Σ', Σ*, .)
SATZ = {rΞΓ, | Ξ ∈ PERF und Γ ∈ GFORM}.
Definition 1-17. Annahme- und Folgerungssatze (ASATZ und FSATZ)
(i) ASATZ = {rSei Γ | Γ ∈ GFORM},
(ii) FSATZ = {rAlso Γ1 | Γ ∈ GFORM}.