論理では、命題だけではなくてメタ命題も扱います。メタ命題で使う記号〈メタ記号〉に ’$`\vdash`$’ や ’$`\models`$’ があります。どちらも「命題はほんとうだ」という意味で使います（が、ほんとうである根拠は違います）。「‥‥という命題はほんとうだ」というメタな文は平叙文〈declarative sentence〉ですが、メタな疑問文〈interrogative sentence〉を使う場合もあります。（[追記]今の話の文脈では、メタでない疑問文（オブジェクトレベルの疑問文）ってないですね。[/追記]）
メタな平叙文と疑問文の区別を付けないとダメでしょ、という話は次の過去記事に書きました。
この過去記事で、$`\vdash!`$（アスキー文字なら |-!）と $`\vdash?`$（アスキー文字なら |-?）という記号で平叙文と疑問文を区別しています。今回のこの記事では、疑問文に対して、可読性・視認性が良い記法を紹介します。上記過去記事にちょっと追加事項があるだけです。不明なことがあったら過去記事も参照してください。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\Imp}{\Rightarrow}
`$
内容：
命題とメタ命題
命題とは、（原理的には*1）真偽が決定可能な文です。命題を自然言語で書くと曖昧性があるので、記号論理学の論理式〈formula〉で書くことにします。例えば、次はゴールドバッハ予想（「4以上の全ての偶数は、二つの素数の和で表すことができる。」）を表す論理式です。
$`\quad \forall n\in {\bf N}.(\\
\qquad n \ge 4 \land \mrm{isEven}(n) \Imp \\
\qquad \exists p, q\in {\bf N}.( \mrm{isPrime}(p) \land \mrm{isPrime}(q) \land p +q = n)\\
\quad )
`$
ゴールドバッハ予想を表す論理式を一文字 $`G`$ で表すことにすれば、「ゴールドバッハ予想はほんとうだ」というメタ命題は次のように書けます。
$`\quad \vdash G`$
しかし現時点では、ゴールドバッハ予想がほんとうかどうか（真か偽か）は誰も分からないので、上記のメタ命題の真偽もまた不明です。誰も「ゴールドバッハ予想はほんとうだ」と断言できません。
しかし、「ゴールドバッハ予想はほんとうですか？」と問うこと／聞くことはできます。その疑問文を次のように書くことにします。
$`\quad \vdash?\; G`$
疑問文は、質問文〈question〉とか問題文〈problem〉、問い合わせ文〈query〉とか言っても同じです。語感やニュアンスに拘ることはしないで、「質問、問題、問い合わせ」は同義だとします。
命題〈論理式〉に対する疑問文は、その論理式を証明せよという命令的意図が含まれていることもあります。なので、過去記事「証明の“お膳立て”のやり方」では証明要求〈proof requirement〉という言葉を使っています。これも同義語です。
質問の前提
前節のゴールドバッハ予想（を表す論理式）は、単一の論理式なのでゴチャゴチャしていました。前提と結論に分けましょう（ただし、分け方には恣意性が入ります）。
前提部分：
$`\quad n \in {\bf N},\\
\quad n \ge 4, \\
\quad \mrm{isEven}(n)`$
結論部分：
$`\quad \exists p, q\in {\bf N}.( \mrm{isPrime}(p) \land \mrm{isPrime}(q) \land p +q = n)`$
すると、質問〈問題 | 問い合わせ | 要求〉のメタ命題は次のように書けます。
$`\quad n \in {\bf N},\\
\quad n \ge 4, \\
\quad \mrm{isEven}(n) \\
\vdash? \\
\quad \exists p, q\in {\bf N}.( \mrm{isPrime}(p) \land \mrm{isPrime}(q) \land p +q = n)`$
1行だと長くなり過ぎるので複数行に分けて、可読性のためにインデントしています。
ここに出てくる述語記号 $`\mrm{isEven}, \mrm{isPrime}`$ の意味は想像できるでしょうが、述語記号の定義も前提にちゃんと入れるなら次のようになります。
$`\quad \mrm{isEven} := \lambda\, m\in {\bf N}.(\exists k\in {\bf N}. m = 2k), \\
\quad \mrm{isPrime} := \lambda\, m\in {\bf N}.(\\
\qquad m \ne 1 \land \\
\qquad (\exists a, b\in {\bf N}. m = ab) \Imp (a = 1 \lor b = 1) \\
\quad ), \\
\quad n \in {\bf N},\\
\quad n \ge 4, \\
\quad \mrm{isEven}(n) \\
\vdash? \\
\quad \exists p, q\in {\bf N}.( \mrm{isPrime}(p) \land \mrm{isPrime}(q) \land p +q = n)`$
前提のなかには、仮定する命題だけではなくて、後で使う記号（関数記号や述語記号）の定義や変数の宣言（例： $`n\in {\bf N}`$）を入れてもかまいません。前提として明示的に書かなくても、暗黙の文脈に定義や宣言が含まれることも多いです。
読みやすいメタ疑問文
メタな疑問文〈質問 | 問題 | 問い合わせ | 要求〉を読みやすく書いてみます。過去記事「保証と要求： カリー／ハワード対応も添えて」とほぼ同じですが、少しだけ追加・変更しています。$`\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\For}{\Keyword{For } }
\newcommand{\Let}{\Keyword{Let } }
\newcommand{\When}{\Keyword{When } }
\newcommand{\DoesHold}{\Keyword{DoesHold? } }
\newcommand{\HoldsQ}{\Keyword{Holds? } }
\newcommand{\Question}{\text{❓}\Keyword{Question } }`$
$`\Question\\
\Let \mrm{isEven} := \lambda\, m\in {\bf N}.(\exists k\in {\bf N}. m = 2k)\\
\Let \mrm{isPrime} := \lambda\, m\in {\bf N}.(\\
\qquad m \ne 1 \land \\
\qquad (\exists a, b\in {\bf N}. m = ab) \Imp (a = 1 \lor b = 1) \\
\quad )\\
\For n \in {\bf N},\\
\When n \ge 4, \\
\When \mrm{isEven}(n) \\
\HoldsQ \\
\quad \exists p, q\in {\bf N}.( \mrm{isPrime}(p) \land \mrm{isPrime}(q) \land p +q = n)`$
過去記事との違いは：
- 疑問文〈質問 | 問題 | 問い合わせ | 要求〉の先頭に、絵文字の疑問符と $`\Keyword{Question}`$ を付けて目立つようにした。
- 前提（コンテキストともいう）のなかに、$`\Keyword{Let}`$ で必要な定義も書いている。
- $`\DoesHold`$の代わりに $`\HoldsQ`$でもいいことにした。
絵文字の疑問符 ❓ は視認性向上に効果があります。ちなみに、次の絵文字も使うとなかなか具合がいいです。
- 定義の先頭に 🔴
- 公理や定理などの主張・判断の先頭に ❗
*1:神様ならば、という意味です。人間は真偽を決定できないかも知れません。
