中間述語論理における選言特性と存在特性およびKripke完全性に関する注意 (証明論とその周辺)

Abstract

An intermediate predicate logic L is said to have the disjunction property (DP) if for every A and every B, L├A∨B implies that L├A or L├B. An intermediate predicate logic L is said to have the existence property (EP) if for every ∃xA(x), L├∃xA(x) implies that there is av such that L├A(v). These properties are proof-theoretically interesting and are regarded as characteristic features of constructivity of intuitionistic theories such as intuitionistic logic H* At present, we have limited knowledge of DP and EP of intermediate predicate logics. In this note, we report some results on Kripke completeness in connection with DP and EP. We have two concepts of Kripke completeness: Kripke-basecompleteness and Kripke-frame-completeness. These two concepts are shown to have different effects in relation to DP and EP.