- 現在 `Schema` と `Theory` という似ているが異なる種類のものがあり紛らわしい． - `Schema` は証明論的な本体，`Theory` はその意味論的な対応物として使い分ける． - `Schema` を理論の公理として，`Theory` をその公理系から証明可能な文の集合として（`Modal` や `Propositional` でやっているように）定める． - 公理（`Schema`）`𝓢` の証明を `(l : {l : List F // ∀ φ ∈ l, φ ∈ 𝓢}) × Derivation (φ :: ∼l)` として定める．
SchemaとTheoryという似ているが異なる種類のものがあり紛らわしい．Schemaは証明論的な本体，Theoryはその意味論的な対応物として使い分ける．Schemaを理論の公理として，Theoryをその公理系から証明可能な文の集合として（ModalやPropositionalでやっているように）定める．Schema）𝓢の証明を(l : {l : List F // ∀ φ ∈ l, φ ∈ 𝓢}) × Derivation (φ :: ∼l)として定める．