$`\newcommand{\mrm}[1]{\mathrm{#1}}\newcommand{\mbf}[1]{\mathbf{#1}}`$
$`A`$ を導出系として、構文ソートとして、formula, true-formula, false-formula を持つとする。
次は最外メタレベルで意味を持つ命題：
- $`x \in \mrm{Term}^\infty(A)_{\text{formula}}`$
- $`t \in \mrm{Term}^\infty(A)_{\text{true-formula}}`$
- $`f \in \mrm{Term}^\infty(A)_{\text{false-formula}}`$
ターンスタイル記法で書けば：
- $`\Vdash_A x \text{ as formula}`$
- $`\Vdash_A t \text{ as true-formula}`$
- $`\Vdash_A f \text{ as false-formula}`$
これは次を意味する。
- $`x`$ は、$`A`$ において、well-formed な論理式である。
- $`t`$ は、$`A`$ において、真であると証明可能な論理式である。
- $`f`$ は、$`A`$ において、偽であると証明可能な論理式である。
つまり、通常の provable, disprovable も、ソート付き導出可能性〈sorted derivability〉で説明できる。証明による真偽と構文的整合性〈整形式性〉は同じ土俵で議論できる。
- $`x`$ は formula としてソート付け可能〈sortable〉である ⇔ $`x`$ は整形式な論理式である。
- $`t`$ は true-formula としてソート付け可能〈sortable〉である ⇔ $`t`$ は証明可能な論理式である。
- $`f`$ は false-formula としてソート付け可能〈sortable〉である ⇔ $`f`$ は反証可能な論理式である。
次の状況もありえる。
- $`x`$ は証明も反証（否定の証明）も出来ない論理式である。
- $`x`$ は証明も反証（否定の証明）も出来る論理式である。
完全な導出系では、整形式な論理式は次のどちらか
- $`x`$ は証明可能であり、反証可能ではない。
- $`x`$ は反証可能であり、証明可能ではない。
証明可能性と反証可能性は、well-sortedness の特殊ケース。well-formedness も well-sortedness の特殊ケース。結局、すべては、well-sorted derivability に帰着する。
