Blog

一階直観主義論理

(Single-sortedな)一階直観主義論理(first-order intuitionistic logic with equality)のシークエント計算LJを与える。

定義（シグネチャ）

シグネチャ(signature)は、以下のデータΣ=(F,R)\Sigma = (F, R)から成る。

  1. 集合FFと関数ar:F→N\mathsf{ar} : F \to \N
    • FFの要素を関数記号(function symbol)と呼ぶ。
    • 各f∈Ff \in Fについて、ar(f)∈N\mathsf{ar}(f) \in \Nはffのarity、つまり引数の数を示す。
  2. 集合RRと関数ar:R→N\mathsf{ar} : R \to \N
    • RRの要素を関係記号(relation symbol)と呼ぶ。
    • 各r∈Rr \in Rについて、ar(r)∈N\mathsf{ar}(r) \in \Nはrrのarityを示す。

シグネチャの定義において、FFやRRは無限集合になり得るが、関数記号や関係記号のarityは有限個に制限されていることに注意。

仮定（変数）

本稿では、可算無限集合Var\mathsf{Var}が存在すると仮定する。Var\mathsf{Var}の要素を変数(variable)と呼ぶ。

定義（項文脈）

項文脈(term context) Γ\Gammaとは、変数の有限集合のことである。

定義（項）

シグネチャΣ=(F,R)\Sigma = (F, R)を固定する。項文脈Γ\Gammaに対して、集合Term(Γ)\mathsf{Term}(\Gamma)を次のように帰納的に定義する。

  1. x∈Γx \in \Gammaならば、x∈Term(Γ)x \in \mathsf{Term}(\Gamma)
  2. f∈Ff \in Fかつn=ar(f)n = \mathsf{ar}(f)であり、任意の1≤i≤n1 \le i \le nについてMi∈Term(Γ)M_i \in \mathsf{Term}(\Gamma)であるならば、f(M1,…,Mn)∈Term(Γ)f(M_1, \ldots, M_n) \in \mathsf{Term}(\Gamma)

Term(Γ)\mathsf{Term}(\Gamma)の要素を「項文脈Γ\Gammaにおける項(term)」と呼ぶ。

補題

M∈Term(Γ)M \in \mathsf{Term}(\Gamma)かつΓ⊆Γ′\Gamma \subseteq \Gamma'ならば、M∈Term(Γ′)M \in \mathsf{Term}(\Gamma')となる。

定義（命題）

シグネチャΣ=(F,R)\Sigma = (F, R)を固定する。項文脈によってインデックス付けされた命題(proposition)を次のように帰納的に定義する。

r∈RMi∈Term(Γ) (for 1≤i≤ar(r))Γ⊢r(M1,…,Mar(r)) prop\frac{ r \in R \quad M_i \in \mathsf{Term}(\Gamma)\ \text{(for $1 \le i \le \mathsf{ar}(r)$)} }{ \propJd{\Gamma}{r(M_1, \ldots, M_{\mathsf{ar}(r)})} }
Γ⊢A propΓ⊢B propΓ⊢A∧B prop\frac{ \propJd{\Gamma}{A} \quad \propJd{\Gamma}{B} }{ \propJd{\Gamma}{A \land B} }
Γ⊢A propΓ⊢B propΓ⊢A∨B prop\frac{ \propJd{\Gamma}{A} \quad \propJd{\Gamma}{B} }{ \propJd{\Gamma}{A \lor B} }
Γ⊢⊤ propΓ⊢⊥ prop\frac{ }{ \propJd{\Gamma}{\top} } \quad \frac{ }{ \propJd{\Gamma}{\bot} }
Γ⊢A propΓ⊢B propΓ⊢A⇒B prop\frac{ \propJd{\Gamma}{A} \quad \propJd{\Gamma}{B} }{ \propJd{\Gamma}{A \Rightarrow B} }
Γ,x⊢A propΓ⊢∀xA propΓ,x⊢A propΓ⊢∃xA prop\frac{ \propJd{\Gamma, x}{A} }{ \propJd{\Gamma}{\forall x A} } \quad \frac{ \propJd{\Gamma, x}{A} }{ \propJd{\Gamma}{\exists x A} }
M∈Term(Γ)N∈Term(Γ)Γ⊢M=N prop\frac{ M \in \mathsf{Term}(\Gamma) \quad N \in \mathsf{Term}(\Gamma) }{ \propJd{\Gamma}{M = N} }

本稿では、束縛変数名による違いを同一視する。

定義（命題文脈）

シグネチャΣ\Sigmaを固定する。項文脈Γ\Gammaにおける命題文脈(proposition context) Δ\Deltaとは、Γ\Gammaにおける命題の有限列のことである。

定義(理論)

理論(theory) T=(Σ,A)T = (\Sigma, \mathcal{A})は、次のデータから成る。

  1. シグネチャΣ=(F,R)\Sigma = (F, R)
  2. 「項文脈Γ\Gamma、Γ\Gammaにおける命題文脈、Γ\Gammaにおける命題」の3項関係A\mathcal{A}
    • 各要素(Γ,Δ,A)∈A(\Gamma, \Delta, A) \in \mathcal{A}を公理と呼ぶ。
定義（Entailment）

理論T=(Σ,A)T = (\Sigma, \mathcal{A})に対して、「項文脈Γ\Gamma、Γ\Gammaにおける命題文脈、Γ\Gammaにおける命題」の3項関係として、entailment judgmentを次のように帰納的に定義する。

(Γ,Δ,A)∈AΓ∣Δ⊢A(Ax)Γ∣Δ⊢AΓ,x∣Δ⊢A(T-Weak)% axiom \frac{ (\Gamma, \Delta, A) \in \mathcal{A} }{ \entailJd{\Gamma}{\Delta}{A} } \text{(Ax)} \quad % t-weaken \frac{ \entailJd{\Gamma}{\Delta}{A} }{ \entailJd{\Gamma, x}{\Delta}{A} } \text{(T-Weak)}
Γ,x,y∣Δ⊢AΓ,x∣[x/y]Δ⊢[x/y]A(T-Contr)Γ∣Δ⊢BΓ∣Δ,A⊢B(P-Weak)% t-contr \frac{ \entailJd{\Gamma, x, y}{\Delta}{A} }{ \entailJd{\Gamma, x}{[x/y]\Delta}{[x/y]A} } \text{(T-Contr)} \quad % p-weaken \frac{ \entailJd{\Gamma}{\Delta}{B} }{ \entailJd{\Gamma}{\Delta, A}{B} } \text{(P-Weak)}
Γ∣Δ,A,A⊢BΓ∣Δ,A⊢B(P-Contr)Γ∣Δ,B,A,Δ′⊢CΓ∣Δ,A,B,Δ′⊢C(P-Ex)% p-contr \frac{ \entailJd{\Gamma}{\Delta, A, A}{B} }{ \entailJd{\Gamma}{\Delta, A}{B} } \text{(P-Contr)} \quad % p-exch \frac{ \entailJd{\Gamma}{\Delta, B, A, \Delta'}{C} }{ \entailJd{\Gamma}{\Delta, A, B, \Delta'}{C} } \text{(P-Ex)}
Γ∣Δ,A⊢A(Id)Γ∣Δ⊢AΓ∣Δ′,A⊢BΓ∣Δ,Δ′⊢B(Cut)% ident \frac{ }{ \entailJd{\Gamma}{\Delta, A}{A} } \text{(Id)} \quad % cut \frac{ \entailJd{\Gamma}{\Delta}{A} \quad \entailJd{\Gamma}{\Delta', A}{B} }{ \entailJd{\Gamma}{\Delta, \Delta'}{B} } \text{(Cut)}
Γ,x∣Δ⊢AM∈Term(Γ′)Γ,Γ′∣[M/x]Δ⊢[M/x]A(Subst)% subst \frac{ \entailJd{\Gamma, x}{\Delta}{A} \quad M \in \mathsf{Term}(\Gamma') }{ \entailJd{\Gamma, \Gamma'}{[M/x]\Delta}{[M/x]A} } \text{(Subst)}
Γ∣Δ⊢AΓ∣Δ⊢BΓ∣Δ⊢A∧B(∧R)Γ∣Δ⊢AΓ∣Δ⊢A∨B(∨R1)Γ∣Δ⊢BΓ∣Δ⊢A∨B(∨R2)% and R \frac{ \entailJd{\Gamma}{\Delta}{A} \quad \entailJd{\Gamma}{\Delta}{B} }{ \entailJd{\Gamma}{\Delta}{A \land B} } \text{($\mathord\land$R)} \quad % or R 1 \frac{ \entailJd{\Gamma}{\Delta}{A} }{ \entailJd{\Gamma}{\Delta}{A \lor B} } \text{($\mathord\lor$R1)} \quad % or R 2 \frac{ \entailJd{\Gamma}{\Delta}{B} }{ \entailJd{\Gamma}{\Delta}{A \lor B} } \text{($\mathord\lor$R2)}
Γ∣Δ,A⊢CΓ∣Δ,B⊢CΓ∣Δ,A∨B⊢C(∨L)Γ∣Δ,A⊢CΓ∣Δ,A∧B⊢C(∧L1)Γ∣Δ,B⊢CΓ∣Δ,A∧B⊢C(∧L2)% or L \frac{ \entailJd{\Gamma}{\Delta, A}{C} \quad \entailJd{\Gamma}{\Delta, B}{C} }{ \entailJd{\Gamma}{\Delta, A \lor B}{C} } \text{($\mathord\lor$L)} \quad % and L 1 \frac{ \entailJd{\Gamma}{\Delta, A}{C} }{ \entailJd{\Gamma}{\Delta, A \land B}{C} } \text{($\mathord\land$L1)} \quad % and L 2 \frac{ \entailJd{\Gamma}{\Delta, B}{C} }{ \entailJd{\Gamma}{\Delta, A \land B}{C} } \text{($\mathord\land$L2)}
Γ∣Δ⊢⊤(⊤R)Γ∣Δ,⊥⊢A(⊥L)% top R \frac{ }{ \entailJd{\Gamma}{\Delta}{\top} } \text{($\top$R)} \quad % bot L \frac{ }{ \entailJd{\Gamma}{\Delta, \bot}{A} } \text{($\bot$L)}
Γ∣Δ,A⊢BΓ∣Δ⊢A⇒B(⇒R)Γ∣Δ⊢AΓ∣Δ,B⊢CΓ∣Δ,A⇒B⊢C(⇒L)% impl R \frac{ \entailJd{\Gamma}{\Delta, A}{B} }{ \entailJd{\Gamma}{\Delta}{A \Rightarrow B} } \text{($\mathord\Rightarrow$R)} \quad % impl L \frac{ \entailJd{\Gamma}{\Delta}{A} \quad \entailJd{\Gamma}{\Delta, B}{C} }{ \entailJd{\Gamma}{\Delta, A \Rightarrow B}{C} } \text{($\mathord\Rightarrow$L)}
Γ,x∣Δ⊢Ax∉fv(Δ)Γ∣Δ⊢∀xA(∀R)M∈Term(Γ)Γ∣Δ⊢[M/x]AΓ∣Δ⊢∃xA(∃R)% forall R \frac{ \entailJd{\Gamma, x}{\Delta}{A} \quad x \notin \fv(\Delta) }{ \entailJd{\Gamma}{\Delta}{\forall xA} } \text{($\mathord\forall$R)} \quad % exists R \frac{ M \in \mathsf{Term}(\Gamma) \quad \entailJd{\Gamma}{\Delta}{[M/x]A} }{ \entailJd{\Gamma}{\Delta}{\exists xA} } \text{($\mathord\exists$R)}
Γ,x∣Δ,A⊢Bx∉fv(Δ,B)Γ∣Δ,∃xA⊢B(∃L)M∈Term(Γ)Γ∣Δ,[M/x]A⊢BΓ∣Δ,∀xA⊢B(∀L)% exists L \frac{ \entailJd{\Gamma, x}{\Delta, A}{B} \quad x \notin \fv(\Delta,B) }{ \entailJd{\Gamma}{\Delta, \exists xA}{B} } \text{($\mathord\exists$L)} \quad % forall L \frac{ M \in \mathsf{Term}(\Gamma) \quad \entailJd{\Gamma}{\Delta, [M/x]A}{B} }{ \entailJd{\Gamma}{\Delta, \forall xA}{B} } \text{($\mathord\forall$L)}
Γ,x∣[x/y]Δ⊢[x/y]AΓ,x,y∣Δ,x=y⊢A(=LF1)Γ,x,y∣Δ,x=y⊢AΓ,x∣[x/y]Δ⊢[x/y]A(=LF2)% Lawvere with Frobenius 1 \frac{ \entailJd{\Gamma, x}{[x/y]\Delta}{[x/y]A} }{ \entailJd{\Gamma, x, y}{\Delta, x = y}{A} } \text{($\mathord=$LF1)} \quad % Lawvere with Frobenius 2 \frac{ \entailJd{\Gamma, x, y}{\Delta, x = y}{A} }{ \entailJd{\Gamma, x}{[x/y]\Delta}{[x/y]A} } \text{($\mathord=$LF2)}

理論間の関係

シグネチャの定義において、「集合XXと関数X→NX \to \N」という形が出てきたが、これはスライス圏Set/N\Set/\Nの対象である。したがって、シグネチャとは積圏Sign≡defSet/N×Set/N\Sign \defeq \Set/\N \times \Set/\Nの対象のことである。この圏の射(F,R)→(F′,R′)(F, R) \to (F', R')は、関数F→F′F \to F'と関数R→R′R \to R'であって、両方ともarityを保存するようなものである。

定義（シグネチャのextension）

シグネチャの圏Sign\Signにおいて、モノ射Σ→Σ′\Sigma \to \Sigma'が存在するとき、Σ′\Sigma'をΣ\Sigmaのextensionと呼ぶ。

既存の文献においては、シグネチャ(あるいはlanguage)のextensionは部分集合を用いて定義されることもある。しかし、「部分集合である」ということは同型によって保たれないので、ここではモノ射を使った。

定義（理論の圏）

理論の圏Th\Thを次のように定義する。

  1. Th\Thの対象は理論である。
  2. Th\Thの射(Σ,A)→(Σ′,A′)(\Sigma, \mathcal{A}) \to (\Sigma', \mathcal{A}')は、Sign\Signの射ϕ:Σ→Σ′\phi : \Sigma \to \Sigma'であって、任意の(Γ,Δ,A)∈A(\Gamma, \Delta, A) \in \mathcal{A}について、
    Γ∣ϕΔ⊢ϕA\entailJd{\Gamma}{\phi \Delta}{\phi A}
    が理論(Σ′,A′)(\Sigma', \mathcal{A}')において導出可能であるようなものである。

理論(Σ,A)(\Sigma, \mathcal{A})からシグネチャΣ\Sigmaを取り出す操作は、忘却関手U:Th↪SignU : \Th \hookrightarrow \Signの対象の部分を成す。この関手UUはfibrationになるらしいが、本稿ではそれを示すことはしない。

定義（理論のextension）

理論T′T'が理論TTのextensionであるとは、Th\Thの射f:T→T′f : T \to T'が存在して、Uf:UT→UT′Uf : UT \to UT'がシグネチャのextensionになることである。

アウトロ

シグネチャの圏Sign\Signの射は関数記号を関数記号に写したが、より便利な概念としてtranslationがあり、これは関数記号を項に写す。このtranslationはKleisli圏の射として表されるが、これを記述するには意味論とinitial modelについて話す必要がある。また、上記でextensionの定義はしたがconservative extensionの話はしなかった。この記事 よく見たらauthorがMax Newだ。 を見る限り、conservative extensionもinitial modelを使って定義できそうだ。