これを「ウソ記事」と呼ぶ。最近の用語法と比較。
| ウソ記事 | 最近 |
|---|---|
| Prop(LL) | LL-Sentence |
| 命題 | 閉論理式, 論理文 |
| Formula(LL) | LL-Formula |
| Proof(LL) | LL-ProofReazoning |
| Prog(PL) | PL-Program |
| 集合D | 集合D |
| Compile | 使わない |
| Code | Encode, g |
| Exec | Run |
| 【-】 | 〚-〛 |
プログラミングシステムにおいて、1プレース（プレースホルダー変数が1つ）のプログラムPが正常終了して、値rを結果とすることを、
- ExecM(P, d) ↓= a
と書く。
演繹システムにおいて、1プレースの述語論理式Aが証明されることを、
- ProveS(A, d) ↓= R
と書く。Rは証明リーズニング図。
特定のP, dに対して次の性質を持つAが欲しい。
- ExecM(P, d) ↓= true (⇒) ProveS(A, d) ↓= R
さらに、
- PからAは具体的に構成可能である。構成手続きをTとして、A = T(P) と書く。
- PとdからRは具体的に構成可能である。
一方で、
- Prove0S(A) ↓= R (⇒) ExecM(P, g(A)) ↓= true
となるPも存在するとする。
- Prove0S(A) ↓= R (⇒) ExecM(P, g(A)) ↓= true (⇒) ProveS(T(P), g(A)) ↓
T(P) を provable-0 とする。provable-1(x, y) := provable0(x[y]) などで、provable-k も定義できる。provable-kは、kプレースの述語論理式が、k個の実データで埋めて証明可能であること。
一般法則を一般的に証明することと、一般法則の個別事例を個別的に確認することはまったく違う。要求される能力がまったく違う。その違いは外部から見れば明らかなんだが、なかなか区別しにくいのかも知れない。
