論理和記号と存在記号を持たない論理での論理和特性と存在特性

古森雄一 (千葉大学理学部)

論理 L が論理和特性 (disjunction property) を持つとは,

⊢_{L} A ∨ B ⟹⊢_{L} A または ⊢_{L} B

が成立していることである。直観主義論理が論理和特性を持つことはよく知られている。論理和特性を記述するのに論理記号 ∨ が必要かというと必ずしも必要としない。記述の仕方を以下の定理の中で一般化した形で与える。また, 自然演繹の正規化定理を使った証明も易しいので紹介したい。存在特性 (existential property) についても同様である。

直観主義論理の {→, ∀}-断片を ILIA とし, p を new 命題変数とする。次が成り立つ。

1. Γ ⊢_{ILIA} (A → p) → (B → p) → p ⟹ Γ ⊢_{ILIA} A または Γ ⊢_{ILIA} B

2. Γ ⊢_{ILIA} ∀x(A(x) → p) → p ⟹ ある項 t が存在してΓ ⊢_{ILIA} A(t)

上は ILIA を BCK 論理の {→, ∀}-断片としても成り立っている。また, 断片を {→, ∀, ∧}-断片としても成り立っている。

より詳しいことは以下に載せる予定である。 http://www.math.s.chiba-u.ac.jp/˜ komori/gakkai/05-09/