暫定！
$`\newcommand{\derive}{ \vdash }%
\newcommand{\deduce}{ \mathop{\|\!-} }%
\newcommand{\afford}{ \mathrel{\|} }%
\newcommand{\Sign}[1]{ \mathscr{#1} }
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\In}{ \text{ in } }
\newcommand{\ImpL}{ \Leftarrow }
\newcommand{\sto}{ \longrightarrow }
%`$
- $`\text{the prerequisites }: \Sign{A}`$ 予備知識、背景指標
- $`\text{the assumptions }: \Gamma`$ シーケントの仮定部分
- $`\text{the generated category }: \cat{C}`$ これは $`\mathrm{MultiDeriv}[\Sign{A}]`$ または $`\mathrm{PolyDeriv}[\Sign{A}]`$ あるいは両方を含む構造
定理の記述：
$`\text{define }\varphi : \Gamma \to P \In \mathrm{MultiDeriv}[\Sign{A}] :=\\
\quad \text{begin derivation} \\
\quad \cdots \\
\quad \text{end derivation}
`$
we, now, already はフィラー〈filler〉語。カンマも出現位置によってはフィラー語。
トートロジー
仮定より
$`\text{by the assumption }a\\
\text{we get }A \text{ named }a'
`$
$`\Gamma[a] = A\\
\text{i.e. }a: (,) \to A \In \cat{C}
`$
前提より
$`\text{by the prerequisite }\alpha \\
\text{we assert }
\Phi \sto P \text{ named }\alpha'
`$
$`\Sign{A}[\alpha] = \Phi \sto P\\
\text{i.e. }\alpha: \Phi \to P \In \cat{C}
`$
連言系
- デカルトモノイド積： $`\land`$
- 単位対象兼終対象〈ターミナルユニット〉： $`\top`$
終対象
$`\text{we have } A \\
\text{by termination}\\
\text{we get }\top
`$
右連言構成
$`\text{we alreay have } \Gamma \\
\text{we have } A \\
\text{begin conjunction}\\
\quad\text{begin factor}\\
\qquad \varphi_1 : \Gamma, A \sto B_1\\
\qquad \text{we get }B_1\\
\quad\text{end factor}\\
\quad\text{begin factor}\\
\qquad \varphi_2 : \Gamma, A \sto B_2\\
\qquad \text{we get }B_2\\
\quad\text{end factor}\\
\text{end conjunction}\\
\text{Now, we assert } \Gamma, A \sto B_1 \land B_2
`$
右全称構成
$`\text{we alreay have } \Gamma \\
\text{we have }A\\
\text{begin universal}\\
\quad\text{variable }x\in X\\
\quad \varphi : \Gamma, A \sto Q(x)\\
\quad \text{we get }P(x)\\
\text{end universal}\\
\text{Now, we assert } \Gamma, A \sto \forall x\in X.Q(x)
`$
射影
$`\text{we have }\forall x\in X.P(x)\\
\text{by instantiation } x \leftarrow a\\
\text{we get }P(a)
`$
選言系
- デカルトモノイド積： $`\lor`$
- 単位対象兼始対象〈イニシャルユニット〉： $`\bot`$
始対象
$`\text{we have }\bot\\
\text{by initialization}\\
\text{we get } B
`$
左連言構成
$`\text{we alreay have } \Gamma \\
\text{we have } A_1 \lor A_2\\
\text{begin disjunction}\\
\quad\text{begin case}\\
\qquad \psi_1 : \Gamma, A_1 \sto B\\
\qquad \text{we get }B\\
\quad\text{end case}\\
\quad\text{begin case}\\
\qquad \psi_2 : \Gamma, A_2 \sto B\\
\qquad \text{we get }B\\
\quad\text{end case}\\
\text{end disjunction}\\
\text{Now, we assert } \Gamma , A_1 \lor A_2 \sto B
`$
左存在構成
$`\text{we alreay have } \Gamma \\
\text{we have }\exists x\in X.P(x)\\
\text{begin existential}\\
\quad\text{variable }x\in X\\
\quad\text{condition }P(x)\\
\quad \psi : \Gamma, P(x) \sto B\\
\quad \text{we get }B\\
\text{end existential}\\
\text{Now, we assert } \Gamma , \exists x\in X.P(x) \sto B
`$
入射
$`\text{we have }Q(a)\\
\text{by witness } a \to x\\
\text{we get }\exists x\in X.Q(x)
`$
仮言系
仮言 ＝ hypothesis、仮言的 ＝ Hypothetical 。
含意
$`\text{we already have }\Gamma \\
\text{begin implication }\ImpL\\
\quad \text{assume }A \\
\quad \varphi : \Gamma, A \sto B\\
\quad \text{we get }B\\
\text{end implication}\\
\text{Now, we assert }\Gamma \sto B \ImpL A
`$
適用
$`\text{we have }B \ImpL A, A\\
\text{by application }\ImpL\\
\text{we get }B
`$
具体例
実例の再掲 - (新) 檜山正幸のキマイラ飼育記 メモ編 にあった例。
begin division prerequisites Γ reserve a, x in Nat theorem exists-minimum : (,) --→ ∃a.∀x.a≦x in MultiDeriv := begin derivation begin universal variable u in Nat by prerequisite we get 0 + u@1 = u by witness t ← u@1 we get ∃t.0 + t = u named p1 by prerequisite we assert ∃t.0 + t = u --→ 0 ≦ u using Imp-Intro we assert (,) --→ ∃t.0 + t = u ⇒ 0 ≦ u names s1 // simple reasoning we have ∃t.0 + t = u ⇒ 0 ≦ u named p2 we have p1, p2 by application 0 ≦ u end universal now, we assert (,) --→ ∀x.(0 ≦ x) // simple reasoning we have ∀x.(0 ≦ x) by witness a ← 0 we get ∃a.∀x.(a ≦ x) end derivation end division
