theorem, proposition, statement 色々

• A proposition is a well-typed term of type prop, a theorem is a proven proposition.
• theoremはproven propositionsとか言っているが、
• thmデータをtheoremと言っていることが一番多い感じ。
• ポールソンは、theoremはruleだ、と言っているし、
• ウェンツェルは、goalはtheoremだ、とも言っている。
• ということは、goalはtheoremだ、となり、何の区別もなくなる。
• 全称が入った命題の the body proposition という言い方がある。
• Thm.add_axiom ctxt (name, A) declares an arbitrary proposition as axiom, and retrieves it as a theorem from the resulting theory.
• ということは、axiomはpropositonでいいのね。itは公理だとすると、公理は定理とみなす、ってこと。まー、そうかも知れない。theoryは定理の集合と同一視することもあるし。
• the proof of Γ |- φ のような言い方もしていて、Γもφもpropositionだと言っている。
• 証明可能性判断 Γ |- φ の右は proposition でいい？
• atomic propositions of the framework って言っている。atomicって定義あったか？
• theoremのpropositionとは言ってるな。うーん？ theoremがproven propositionsだとしたら、theoremのpropositionとは、provenを忘れるだけ。実体は同じ？？
• There is no distinction of term vs. proposition. これは、porpositonがtermだからだろう。
• the statement of a theorem とも言っている。statement＝propositon か？
• rule statements -- ？？はぁーー？ なに、どこ、どれ
• the main statement -- ？？はぁーー？
• the statement of theorem thm -- ？？はぁーー？
• goal statement うーーーん。
• an atomic formula、atomic propositionと同じだとは思うが、、、

A proposition is a well-typed term of type prop は信用していいだろう。だが、a theorem is a proven proposition は信用出来ない。propositionを構文的に捉えれば、それはformulaだろう。

構文範疇のstmtは命題（おそらく論理式と同義）をキーワードandで繋いだリストの意味しかない。リストの長さが1なら stmpとpropositonは同義。theoremコマンドって、andで繋げたっけ？

いずれにしても、次が混じる。

• Isarの構文範疇としての stmt, statement
• Isarのコマンド、キーワード
• 実装内のMLのデータ型、データ構造。cterm, thmなどがある。
• 論理学の伝統的な用語としての theory, formula, theorem, axiom
• 説明のための地の文のインフォーマルな用法