論理用語

論理：

矢印	左	右
含意〈implication〉 ⊃	前件〈antecedent〉	後件〈succedent〉
伴意〈entailment〉→	仮定〈assumption〉	結論〈conclusion〉
証明可能性〈be-provable〉判断	仮定〈assumption〉	結論〈conclusion〉
妥当性〈validity〉判断	モデル〈model〉	文〈sentence〉
意味的帰結	前提〈premise〉	帰結〈consequence〉

論理：

論理	Lean	左	右
含意〈implication〉 ⊃	含意 →	前件〈antecedent〉	後件〈succedent〉
伴意〈entailment〉→	プロファイル :	引数リスト	ターゲット型
なし	ゴール	コンテキスト＝仮説〈hypothesis〉リスト	証拠項とターゲット型
証明可能性〈be-provable〉判断	なし	-	-
妥当性〈validity〉判断	なし	-	-

関連する言葉：

1. [Lean] テレスコープ{リスト}?
2. [Lean] タクティク [論理]シーケント推論規則の逆
3. [Lean] 環境＝大域コンテキスト [論理] 前提〈premise〉、予備知識〈prerequisite〉
4. [Lean] ライブラリ [論理] 前提、予備知識、セオリー〈theory〉
5. [Lean] パッケージ [論理] セオリー〈theory〉
6. [Lean] ファイル＝モジュール [論理] セオリー〈theory〉
7. 帰結〈consequence〉
8. リーズニング〈reasoning〉

整理するために：

• ゴール＝クエリーは、Γ |-? _:B 。Γは仮定＝コンテキスト、_ はワイルドカードまたはプレースホルダ、Bはターゲット。
• アサーション＝ジャッジメント＝シーケントは、Γ |-! f:B 。Γは仮定＝コンテキスト、f は証拠式〈witness {expression | term}〉、Bはターゲット。
• 名前付きで格納されたアサーションが定理。格納場所は、Lean環境またはLeanライブラリ。LeanライブラリからLean環境に import でロードする。
• アサーション＝ジャッジメント＝シーケント＝ビリーフは、ファクトとルールに分けられるが、仮定があるかどうかだけ。