論理の用語法整理の試み 2

形式的に定義しない言葉

• 証明 → 証拠{図 | 式}またはリーズニング{図 | 式}
• 公理 → 原子定理
• 命題 → 論理式、定理
• 推論、推論規則 → 原子証拠{図 | 式}、原子リーズニング{図 | 式}

形式的に定義する言葉

• 項、原子項
• 論理式、原子論理式
• 文脈
• シーケント
• 証拠{図 | 式}、原子証拠{図 | 式}
• リーズニング{図 | 式}、原子リーズニング{図 | 式}
• 論理式定理
• シーケント定理
• 論理式定理ライブラリ
• シーケント定理ライブラリ
• 論理式定理ライブラリ・インターフェイス
• シーケント定理ライブラリ・インターフェイス
• 定理のヘッド（名前はオプショナル）
• 定理のステートメント
• 定理のボディ
• 定理／ライブラリのトランスパイル
• 証拠{図 | 式}モナド 単位：論理式の集合 → 証拠図の集合
• リーズニング{図 | 式}モナド 単位：シーケントの集合 → リーズニング図の集合
• モナド変換子： 証拠図モナド → リーズニング図モナド （ゲンツェン変換子）

パターン

• パターン変数： 原子論理式変数（ラテン文字）、論理式変数（ラテン大文字）、リスト変数（ギリシャ大文字）、証拠変数（ギリシャ小文字）
• 論理式パターン（論理式変数）
• シーケント・パターン（論理式変数、リスト変数）
• 証拠{図 | 式}パターン（論理式変数、リスト変数）
• リーズニング{図 | 式}パターン（論理式変数、リスト変数、証拠変数）
• 論理式定理パターン（名前変数、論理式パターン、証拠パターン）
• シーケント定理パターン（名前変数、シーケント・パターン、リーズニング図パターン）