Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

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φ(θ₀, .., θ,,_-∣f ∈ FTERM, dann

TA(^rφ(θo, ..., θn-ɪ)ɔ) = {^rφ(θo, ..., θ^-ɪ)ɔ, φ} ∪ U{TA(θ_j) | i < n},

(iii) Wenn ^rΠξ^¹ ∈ QUANTOR, dann TA( ^rΠξ^π) = {^rΠξ^π, Π, ξ},

(iv) Wenn ^rΦ(θ₀, .., θ,,_-∣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(Δ₀ ψ Δ₁)^^l ∈ JFORM, dann

TA(^r(Δo ψ Δ1D = { ^r(Δo ψ ʌɪ)ɔ, ψ} ∪ TA(Δo) ∪ TA(Δ1),

(vii) Wenn ^rΠξΔ"¹ ∈ 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.

<<   26   27   28   29   30   31   32   >>

More intriguing information