第6章シークェント計算(3)

一階言語の部分集合Sについての構造みたいな感じのMについて
Mがエルブラン構造で、V(x)=x for all x ∈ Var_s
なら、I=(M,V)はエルブラン解釈

例
S={∀xP(f(x),f(f(x))),P(f(a),y)}とすると
Fun_s = {f,a}
Pre_s = {P}
Var_s = {y}
H_s = T(Fun_s, Var_s)
　　= {a,f(a),f(f(a)), ... , y,f(y),f(f(y)), ... }

M［[a]］=a
M［[f]］(f^i(a)) = f^(i+1)(a)
M［[P]］= (?,?) = true|false iff ? (任意に定義可能)
V(y)=y

以下のような導出木Πを公平な導出木という。

Πは終了している
- 可能性1：葉が公理になっている
- 可能性2：葉が非公理の原子論理式になっている
- 可能性3：無限の導出木になっている。
Πのすべての無限の経路に対してそれらのラベルの無限系列Π(pi)=Γi⇒Δi(i=0,1,2,...)は次の条件を満たす
1. Φ^∞（無限系列においてあるところから上は必ず存在する左辺の論理式）は原子論理式であるか∀xBの形の論理式である
2. Ψ^∞（無限系列においてあるところから上は必ず存在する右辺の論理式）は原子論理式であるか∃xBの形の論理式である
3. Φ（無限系列において左辺に現れる論理式）について∀xA∈Φならばa[t/x]∈Φである。
4. Ψ（無限系列において右辺に現れる論理式）について∃xA∈Ψならばa[t/x]∈Ψである。

補題：任意の導出木に対して公平な導出木が必ず存在する。
Hsの要素をまんべんなく利用すればよい。それだけ。
作成手順としては、順番に適用する。

難しい。
エルブラン構造をうまく利用するとうまくいく。