$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\H}{\text{-} }
\newcommand{\Iff}{ \Leftrightarrow }
`$
昔の記述をコピー
$`L\H\mrm{Formula}_{(\$1\in D)}`$ に属する論理式 $`\mrm{lie}`$を次のように定義する。
$`\quad \mrm{lie} := \lnot (\mrm{prov}_S[\$2/\$1])`$ （対角述語の構成）
$`d\in D`$ に対して、$`\mrm{lie}[d/\$1]`$ は $`\lnot(\mrm{prov_S}[d/\$1, d/\$1])`$ のことになる。
$`\mrm{lie}[d/\$1], \mrm{prov}_S[d/\$1, d/\$2]`$ をそれぞれ $`\mrm{lie}(d), \mrm{prov}_S(d, d)`$ と書けば：
$`\quad \mrm{lie}(d) := \lnot\mrm{prov}_S(d, d)`$ （対角述語の構成）
と略記できる。
閉論理式 $`\mrm{lie}( \mbf{g}(\mrm{lie}) )`$ に注目する。正確には、
$`\quad \mrm{lie}(\mbf{g}(\mrm{lie})) = \mrm{lie}[\mbf{g}(\mrm{lie})/\$1] = \lnot(\mrm{prov}_S[\mbf{g}(\mrm{lie})/\$1, \mbf{g}(\mrm{lie})/\$2])
`$
$`S`$ は**演繹完全**だと仮定しているので、次のいずれかが成立する（他の可能性はない）。
- $`\vdash_S \mrm{lie}(\mbf{g}(\mrm{lie}))`$
- $`\vdash_S \lnot(\mrm{lie}(\mbf{g}(\mrm{lie})))`$
$`S`$ は**無矛盾**だから、1 と 2 が同時に成立することもない。2つの排他的場合に分けて考えればよい。
- $`\mrm{lie}(\mbf{g}( \mrm{lie}))`$ が $`S`$ で証明可能なとき
- $`\lnot \mrm{lie}(\mbf{g}( \mrm{lie}))`$ が $`S`$ で証明可能なとき
新しい定式化
計算システムとその言語の名前を $`S`$ とする。$`S`$ はホモアイコニックとする。したがって、ゲーデルコーディングは不要。$`\mbf{D}`$ を全データ領域とする。$`\mbf{D}`$ の型付き自由変数を1つだけ持つ論理式の集合を $`\mrm{Formula}[\mbf{D}]`$ とする。
次の模倣原理が成立している、とする。$`p`$ は論理式をラムダ抽象した述語式。$`x`$ は個体データ。
$`\quad \vdash_S p(x) \Iff {\vdash_S} \mbf{S}(p, x)`$
二変数の述語項 $`\mbf{S}`$ は $`S`$ を模倣する。
$`\mrm{Formula}[\mbf{D}] \times \mbf{D}`$ は、意味論的真偽割り当てにより、二分割されているとする。この2分割は、述語式 $`\mbf{S}`$ で実現されるとする。$`\mbf{S}`$ は：
- 決定性であり、全域である。（$`\bot`$ を返すことは許されない）
- 論理式 $`A`$ と $`\lnot A`$ に異なる値を返す。（無矛盾）
論理式 $`\mrm{lie}`$ を次のように定義する。否定的自己言及（ウソツキ命題）を使う。
$`\quad \mrm{lie}(d) := \lnot\mrm{S}(d, d)`$ （対角述語の構成）
ラムダ抽象すれば一引数述語式になる。$`\mrm{lie}`$ の解釈は、データであるところの命題 $`d`$ はウソ（偽な命題）である。「じゃ、お前はどうなんだ？」に対して、$`\mrm{lie}(\mrm{lie})`$ がスタック〈stuck〉する。
