演繹付きインスティチューション
演繹付きインスティチューション〈institution with deduction〉を定義する。
普通のインスティチューションに、指標Σごとの演繹性判断〈deducibility judgement〉|-Σが付いている。
- |-Σは、Pow(Sen[Σ])とSen[Σ]のあいだの（二項）関係
演繹性判断は、次の公理を満たす。
- {a} |- a 反射性
- A |- a, A⊆B ならば B |- a 単調性
- Ai |- ai ならば、∪({ai}|i∈I) |- b ならば、∪(Ai|i∈I) |- b 推移性
A⊆Sen[Σ]に対して、モデルMod[Σ]の部分圏 (Mod[Σ] s.t. A) を次のように定義する。
- すべてのa∈Aに対して X |= a であるような対象Xの全体を |Mod[Σ] s.t. A| として、この対象類から誘導される充満部分圏を(Mod[Σ] s.t. A)とする。
帰結性判断〈consequence judgement〉 A |⇒ a を次にように定義する。
- (A |⇒ a) iff (すべての X∈|Mod[Σ] s.t. A| に対して、X |= a)
演繹付きインスティチューションにおいて、|-Σ が健全であることは、次のように定義される。
- A |- a ならば、A |⇒ a
インスティチューションにもともと付いていある充足性判断〈satisfaction judgement〉、充足性判断から導かれる帰結性判断、それとは独立な演繹性判断の3つの判断のあいだの関係を考える。
健全性以外に問題となる性質は、
- 適切性〈adequacy〉
- 完全性（健全かつ適切）
- コンパクト性
コンパクト性は次の意味
- A |- a ならば、Aの有限部分集合A'があり、A' |- a
より強い有限性は、
- A |- a ならば、Aは有限集合
演繹付きインスティチューションとハイパードクトリンを組み合わせると、構文論と意味論の両方を扱えそうだ。ハイパードクトリンを指標の上に展開するのが最初の作業かな。
コマンドとブロック
BLKと書いてあるのはブロック、そうでなければコマンド。
| 論理記号 | 導入 | 削除 |
|---|---|---|
| ∧ | make conjunction of/with | select - from |
| ∨ | make disjunction of/with | case of BLK |
| ¬ | contradiction of BLK | found inconsistency of/with |
| ⊃ | use assumption - to | appy - to |
| ∀ | for BLK | instanciate - with |
| ∃ | witness of BLK | choice - of BLK |
- conjunction, disjunction の動詞はないようだ。
- contradiction は proof by contradiction から。
- forはfixに変えるかも知れない。
- absurdは the absurd で名詞に使える。
ブロックには引数命題と最終命題と結論命題がある。
| ブロック | 引数命題 | 最終命題 | 結論命題 |
|---|---|---|---|
| proof of | P | P | P |
| contradiction | P | absurd | ¬P |
| for x:X | なし | P(x) | ∀x:X.P(x) |
| case of | P∨Q | R | R |
| choice a:X | ∃x:X.P(x) | Q | Q |
| witness of | x:X, P(x) | P(t) | ∃x:X.P(x) |
直前のブロックから結論命題を取り出すコマンドがtherefor。
コマンド構文
make conjunction コマンド
- [make] conjunction [of P] with Q ...
- 出力： 結論命題 P∧Q
select コマンド
- select e [from P] eはパス式
- 出力： パスで選択された命題
make disjunction コマンド
- [make] disjunction [of P] with Q ...
- 出力： 結論命題 P∨Q
found inconsistency コマンド
- [found] inconsistency [of P] with Q
- 出力： absurd
assume コマンド
- assume P
- 出力： なし
use assumption コマンド
- [use] assumption P [to Q]
- 出力： 結論命題 P⊃Q
instanciate コマンド
- instanciate [∀x:X.P(x)] with t
- 出力： 結論命題 P(t)
apply コマンド
- apply P⊃Q [to P]
- 出力：結論命題 Q
therefor コマンド
- therefor
- 出力： ブロックの結論命題
ブロック構文
proof ブロック
- proof [of P] end
- 自動仮定： なし
- 要求最終命題： P
- 結論： P 最終命題
contradiction ブロック
- contradiction [of P] / end
- 自動仮定： ¬P
- 要求最終命題： absurd
- 結論：P 最終命題
case ブロック
- case [of P∨Q ...] / whenブロック ... / end
- 自動仮定： なし
- 要求最終命題： すべてのwhenブロックで同じ結論R
- 結論： R 最終命題
for ブロック
- for x:X / end
- 自動仮定： なし
- 要求最終命題： なし だがPとする
- 結論： ∀x:X.P
witness ブロック
- withness [of P(x)] / end
- 自動仮定： なし
- 要求最終命題： P(t)
- 結論： ∃x:X.P(x)
choice ブロック
- choice a:X [from ∃x:X.P(x)] / end
- 自動仮定： P(a)
- 要求最終命題： aを含まないQ
- 結論： Q 最終命題
