Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

1.1 Inventar und Syntax

Definition 1-5. Stelligkeit

μ ist i-stellig

gdw

(i) μ ∈ FUNK und es gibt j ∈ N, so dass μ = f oder

(ii) μ ∈ PRA und es gibt j ∈ N, so dass μ = ^rPij¹ oder

(iii) μ = ' ¹ und i = 2 oder

(iv) μ = ^r— und i = 1 oder

(v) μ ∈ JUNK∖{ r— } und i = 2 oder

(vi) Es gibt Π ∈ QUANT und ξ ∈ VAR und μ = ^rΠξ^^l und i = 1 oder

(vii) μ ∈ PERF und i = 1.

Definition 1-6. DieMenge der Terme (TERM; Metavariablen: θ, θ', θ*, ...)

TERM = ∩{R | R ⊆ AUS und

(i) KONST ∪ PAR ∪ VAR ⊆ R und

(ii) Wenn {θ₀, ., θ_n_-ι} ⊆ R und φ ∈ FUNK n-stellig, dann ⅛(θ₀, ., θ_n_-∣)^π ∈
R}.

Hinweis: Leerzeichen dienen hier und im Folgenden nur der besseren Lesbarkeit, sie sind

kein Teil der Ausdrucke. So steht etwa T₃.₁(c₀, c₀, c₁)^^l fur rf₃.₁(c₀,c₀,c₁)^^l.

Definition 1-7. Atomare und funktorale Terme (ATERMundFTERM)

(i) ATERM = KONST ∪ PAR ∪ VAR,

(ii) FTERM = TERM∖ATERM.

Definition 1-8. Die Menge der Quantoren (QUANTOR)

QUANTOr = {^rΠξ' | Π ∈ QUANT und ξ ∈ VAR}.

Definition 1-9. Die Menge der Formeln (FORM; Metavariablen: Α, Β, Γ, Δ, Α', Β', Γ', Δ', Α*,
Β*, Γ*, Δ*, .)

FORM = ∩{R | R ⊆ AUS und

(i) Wenn {θ₀, ., θ_n_-1} ⊆ TERM und Φ ∈ PRA n-stellig, dann rφ(θ₀, ., θ_n,₁)^^l

∈ R,

(ii) Wenn Δ ∈ R, dann r—Δ ∈ R,

(iii) Wenn Δ₀, Δ₁ ∈ R und ψ ∈ JUNK∖{ ^r—¹}, dann r(Δ₀ ψ Δι)^^l ∈ R, und

(iv) Wenn Δ ∈ R und ξ ∈ VAR und Π ∈ QUANT, dann ^rΠξΔ"¹ ∈ R}.