よく分からん用語

いつものことだが、証明支援系や論理の話が、だいたいイイカゲンで論理的でもフォーマルでもない記述が多くて困る。[追記]研究対象→曖昧な用語法の研究 - 檜山正幸のキマイラ飼育記 メモ編[/追記]

テクニカルタームと説明の地の文の区別がつかない。at show time って洒落で言ってんのか？ 技術的な解説？ showは証明コマンドだけど。

conclusioとresultは違うのか。exportってテクニカルターム？ 単なる説明？ discharge, unfoldもどっち（テクニカルターム or 地の文）か分からん。

backward reasoning, forward reasoning、これは分かる。

変数に関しては、fixed variable, meta-variable、メタ変数って何？ 何に対してメタ？ スキーマ変数とか?変数とは別？

proof step、なにが一ステップなんだ？

localナントカが頻出。ローカルって何だ？ ブロック構造のスコープのことを指しているのか？

χ |- φ をリザルトと呼んでいるな。これは証明可能を意味するメタ言明だが、それをリザルトというのか？ひょっとしてメタじゃない？

assumption commandって何を意味する。assumeという具体的なコマンドのことか？ 一群のコマンドの集まり・類を指しているのか？

soloveって動詞は何の意味だ。solove a goalだから、ゴールと関係するのだろう。goalが証明されたってことか。ってことは、goalは証明するもの。statementとgoalは区別する。定理とgoalは同じ、違うならその関係は？

premise of the goalって言ってるぞ。ってことはgoalは単なる命題じゃないな。シーケンとか、または含意にパターンマッチする命題か。

- を使った式（メタな言明）には名前が付いてない。なんて言えばいいんだ？ 証明可能性の主張だけど、シーケントというべきか？ いずれにしても χ

- はリザルトと言っている。何のリザルトなんだ？

local variable、またローカルだよ。だからローカルって何？ 何と比較してローカル？ じゃ、グローバルは何？ スコーピングをハッキリさせろよ。んん？ ローカル変数って、fixed変数と同義か。

let文はstatementと言ってるな、しかしこれは束縛を作るのではなくて、略記（abbreviation）と言っている。略記は束縛とは別？ それとも、束縛と同義？

ふと思い出したが、含意の左右は前件と後件と呼ぶことにしたのだった。→「ならば」記号の部分 - 檜山正幸のキマイラ飼育記 メモ編

出たー、hypothesis来たよ。だーから、premise, assumptionとどう違うんだって？

factは、assumptionか、local statementのproofで導入される、って。仮説的な仮定か、または証明済みの命題。いずれにしても命題のことか。contextを構成する要素のことか。current factはcurrent contextと同じ、違う？

れれれ、lemma, theorem, corollary, proposition, have, show, hence, thusなどまとめてゴールって呼んでるぞ。さっきまでと話が合わない。多義的なんだろう。何の説明もないが。ゴールって、手続き証明あるいは状態遷移モデルの概念で、それに対応する構文的な範疇もゴールって呼んでいるのか？

毎度毎度、、、、→型推論に関わる論理の概念と用語 その6：substitutionの記法 - 檜山正幸のキマイラ飼育記 →絵算（ストリング図）における池袋駅問題の真相 - 檜山正幸のキマイラ飼育記 疲れるよなーー、勘弁してくれ。