Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

5.1 Erfullungsrelation und modelltheoretische Konsequenz 213

Definition 5-5. Termdenotationsfunktionen fur Modelle und Belegungen

F ist eine Termdenotationsfunktion fur D, I, b
gdw

(D, I) ist ein Modell und b eine Belegung fur D und F ist eine Funktion auf GTERM und:

(i) Wenn α ∈ KONST, dann F (α) = I (α),

(ii) Wenn β ∈ PAR, dann F (β) = b (β), und

(iii) Wenn φ ∈ FUNK und φ r-stellig ist und θ₀, ..., θ_r-1 ∈ GTERM, dann
F(^rφ(θo, ..., θr,ɪ)ɔ) = I(φ)(<F(θo), ..., F(θ,₄)>).

Theorem 5-1. Fur jedes Modell (D, I) und Belegung b fur D gibt es genau eine Termdenota-
tionsfunktion

Wenn (D, I) ein Modell und b eine Belegung fur D ist, dann gibt es genau ein F, so dass F
eine Termdenotationsfunktion fur D, I, b ist.

Beweis: Sei (D, I) ein Modell und b eine Belegung fur D. Dann gibt es mit den Theore-
men uber eindeutige Lesbarkeit (Theorem ɪ-ɪ0 und Theorem ɪ-ɪɪ) genau eine Funktion
F auf GTERM, so dass Klauseln (i) bis (iii) von Definition 5-5 fur F erfullt sind und da-
mit nach Definition 5-5 genau eine Termdenotationsfunktion fur D, I, b. ■

Definition 5-6. Termdenotationsoperation (TD)

TD(θ, D, I, b) = a

gdw

(i) Es gibt eine Termdenotationsfunktion F fur D, I, b und θ ∈ GTERM und a = F(θ)
oder

(ii) Es gibt keine Termdenotationsfunktion fur D, I, b oder θ ∉ GTERM und a = 0.

Das folgende Theorem spiegelt die ubliche Definition von Termdenotaten fur Modelle
und Belegungen wider:

<<   184   185   186   187   188   189   190   >>

More intriguing information