以下の内容はhttps://m-hiyama-memo.hatenablog.com/entry/2025/07/01/162644より取得しました。


最外表明と対象化引用符

最外表明〈outer-most assertion〉とは、それ以上はファクトチェックをしないで信じることにする命題と極性〈{logical}? porality〉のペア。次の2つの形式で書く。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\Iff}{ \Leftrightarrow }
\newcommand{\OQ}[1]{``(#1)"}
`$

  • $`\text{Holds } P \text{ on }X`$
  • $`\text{NotHolds } P \text{ on }X`$

論理式 $`P`$ には、$`X`$ を走る変数が入っていてもいなくてもいい。入ってなくても水増し〈thinning | weakening〉解釈できる。$`X`$ 以外の変数・名前は(省略されている)コンテキスト $`\Gamma`$ で宣言または定義されているとする。コンテキストも書けば:

  • $`\Gamma \mid \text{Holds } P \text{ on }X`$
  • $`\Gamma \mid \text{NotHolds } P \text{ on }X`$

最外表明を対象レベルに落として議論したいときは、対象化引用符〈objectification quote〉で囲む。

  • $`\OQ{\text{Holds } P \text{ on }X}`$
  • $`\OQ{\text{NotHolds } P \text{ on }X}`$

これで、最外表明の資格は奪われて、単なる命題になる。次のような最外表明を書ける。

$`\text{NotHold }\OQ{\text{Hold} P \text{ on }X} \text{ on }\mbf{1}`$

なお、$`\text{on }\mbf{1}`$ は省略してよい。

次はメタな命題となる。

$`\OQ{\text{Holds } P \Iff Q \text{ on }X} \Iff \OQ{ P \equiv Q \text{ on }X}
`$

次はメタな命題を肯定的に表明〈affirmatively assert〉している。

$`\text{Holds }\OQ{\;\OQ{\text{Holds } P \Iff Q \text{ on }X} \Iff \OQ{ P \equiv Q \text{ on }X}\;}
`$

これはメタな同値記号 $`\equiv`$ を使って、次のように書いても同じ。

$`\OQ{\text{Holds } P \Iff Q \text{ on }X} \equiv \OQ{ P \equiv Q \text{ on }X}
`$




以上の内容はhttps://m-hiyama-memo.hatenablog.com/entry/2025/07/01/162644より取得しました。
このページはhttp://font.textar.tv/のウェブフォントを使用してます

不具合報告/要望等はこちらへお願いします。
モバイルやる夫Viewer Ver0.14