Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie



1.2 Substitution


39


Sei Δ = rΠξΔoπ QFORM. Angenommen ξ = θ+. Dann ist [θ*, θ+, Δ] = [θ*, θ+,
'HξΔ I = rΠξΔoπ = [β, θ+, rΠξΔoπ] = [β, θ+, Δ]. Dann ist β TT([β, θ+, Δ]) = TT(Δ).
Also [θ*, θ+, Δ] = [β, θ+, Δ] = [θ*, β, [β, θ+, Δ]]. Angenommen ξ
θ+. Der Fall verlauft
analog zum Negatorfall.

Zu (iii): Der Fall verlauft analog zum Negatorfall. ■

Theorem 1-25. Eine hinreichende Bedingung fur die Kommutativitat einer Substitution in
Termen und Formeln

Wenn θ*o, θ*ι GTERM, θo, θι ATERM, θo ≠ θɪ, θɪ TT(θ*o) und θo TT(θ*ι), dann:
(i) Wenn θ+
TERM, dann [θ*1, θ1, [θ*o, θo, θ+]] = [θ*o, θo, [θ*1, θ1, θ+]], und
(ii) Wenn Δ
FORM, dann [θ*ι, θ1, [θ*o, θo, Δ]] = [θ*o, θo, [θ*ι, θι, Δ]].

Beweis: Seien θ*o, θ*1 GTERM, θo, θ1 ATERM, θo ≠ θ1, θ1 TT(θ*o) und θo
TT(θ*1). Zu (i): Sei θ+ TERM. Der Beweis wird mittels Induktion uber den Termaufbau
von θ+ gefuhrt. Sei θ+
ATERM. Angenommen θ+ = θo. Dann ist θ+ ≠ θ1 und [θ*1, θ1,
[θ*
o, θo, θ+]] = [θ*1, θ1, θ*o]. Weil θ1 TT(θ*o) gilt [θ*1, θ1, θ*o] = θ*o. Andererseits ist
[θ*
o, θo, [θ*1, θ1, θ+]] = [θ*o, θo, θ+] = θ*o. Also [θ*1, θ1, [θ*o, θo, θ+]] = [θ*o, θo, [θ*1, θ1,
θ+]]. Sei nun θ+ ≠ θ
o. Angenommen θ+ = θ1. Dann ist [θ*1, θ1, [θ*o, θo, θ+]] = [θ*1, θ1, θ+]
= θ*
1. Weil θo TT(θ*1) gilt [θ*o, θo, θ*1] = θ*1. Damit ist [θ*o, θo, [θ*1, θ1, θ+]] = [θ*o,
θ
o, θ*1] = θ*1. Also [θ*1, θ1, [θ*o, θo, θ+]] = [θ*o, θo, [θ*1, θ1, θ+]]. Angenommen θ+ ≠ θ1.
Dann ist [θ*
1, θ1, [θ*o, θo, θ+]] = [θ*1, θ1, θ+] = θ+ und [θ*o, θo, [θ*1, θ1, θ+]] = [θ*o, θo, θ+]
= θ+. Also auch [θ*
1, θ1, [θ*o, θo, θ+]] = [θ*o, θo, [θ*1, θ1, θ+]].

Gelte die Behauptung fur {θ'o, ..., θ'r-1} TERM und sei θ+ = rφ(θ'o, ..., θ'r-1)^l
FTERM. Dann ist [θ*ι, θ1, [θ*o, θo, θ+]] = [θ*ι, θι, [θ*o, θo, rφ(θ'o, ., θ'r)π]] = rφ([θ*ι,
θ
ι, [θ*o, θo, θ'o]], ., [θ*ι, θι, [θ*o, θo, θ'r]])π. Mit I.V. gilt [θ*1, θι, [θ*o, θo, θ'i]] = [θ*o,
θ
o, [θ*ι, θι, θ'i]] fur alle ir. Also [θ*ι, θι, [θ*o, θo, θ+]] = rφ([θ*o, θo, [θ*ι, θι, θ'o]], .,
[θ*
o, θo, [θ*ι, θι, θ'r]])π = [θ*o, θo, [θ*ι, θι, rφ(θ'o, . θ¼)π]] = [θ*o, θo, [θ*ι, θι, θ+]].

Zu (ii): Sei Δ FORM. Der Beweis wird mittels Induktion uber den Formelaufbau von
Δ gefuhrt. Sei Δ =
rΦ(θ'o, . θ'r)π AFORM. Dann ist [θ*ι, θι, [θ*o, θo, Δ]] = [θ*ι, θι,
[θ*
o, θo, rΦ(θ'o, ., θ'r-1)π ]] = rΦ([θ*ι, θι, [θ*o, θo, θ'o]], ., [θ*1, θι, [θ*o, θo, θ'r-1]])π. Mit
(i) gilt [θ*
1, θ1, [θ*o, θo, θ'i]] = [θ*o, θo, [θ*1, θ1, θ'i]] fur alle i r. Also [θ*1, θ1, [θ*o, θo,
Δ]] =
rΦ([θ*o, θo, [θ*ι, θι, θ'o]], ., [θ*o, θo, [θ*ι, θι, θ'r-1]])π = [θ*o, θo, [θ*ι, θι, rΦ(θ'o,
. θ'
r-1)π ]] = [θ*o, θo, [θ*ι, θι, Δ]].



More intriguing information

1. HOW WILL PRODUCTION, MARKETING, AND CONSUMPTION BE COORDINATED? FROM A FARM ORGANIZATION VIEWPOINT
2. THE DIGITAL DIVIDE: COMPUTER USE, BASIC SKILLS AND EMPLOYMENT
3. The name is absent
4. The Formation of Wenzhou Footwear Clusters: How Were the Entry Barriers Overcome?
5. Dual Inflation Under the Currency Board: The Challenges of Bulgarian EU Accession
6. Dementia Care Mapping and Patient-Centred Care in Australian residential homes: An economic evaluation of the CARE Study, CHERE Working Paper 2008/4
7. Towards Learning Affective Body Gesture
8. WP 1 - The first part-time economy in the world. Does it work?
9. The name is absent
10. TOWARDS THE ZERO ACCIDENT GOAL: ASSISTING THE FIRST OFFICER MONITOR AND CHALLENGE CAPTAIN ERRORS