Weak Logical Constants and Second Order Definability of the Full-Strength Logical Constants
スポンサーリンク
概要
- 論文の詳細を見る
In [5] Prawitz gave a second order definability result on some logical constants, more precisely, he showed that all the intuitionistic logical constants conjunction (∧), the first order and the second order existential quantifier (∃), and disjunction (∨), are definable on the basis of the intuitionistic implication (⊃), the first order and the second order universal quantifier (∀). (Here we should remark that definability of the intuitionistic logical constants implies definability of the classical logical constants via, for example, Godel's negative interpretation [2]). The use of the full strength intuitionistic implication and universal quantifier as the basis were very essential in Prawitz's method, and one cannot replace those basic constants by the others, e.g. the existential quantifiers and conjunction. In this situation it seems interesting to study a different method of second order definability of the logical constants, especially definability of implication and universal quantifiers, based on the existential quantifiers. In this note, we remark that if we assume very weak logical constants, the full-strength intuitionistic (hence classical) logical constants, including implication and universal quantifiers, are definable by the help of the intuitionistic second order existential quantifier and conjunction. The weak logical constants introduced here are called "simple" logical constants. As a corollary of our definability result, though the first order system for simple logical constants are extremely weak, the second order extension of that system has the same logical strength as the intuitionistic second order logic (hence as the classical second order logic, via Godel's negative interpratation). We shall also analyze our simple implication and simple universal quantifier, in terms of Kripke-type possible world models.
- 科学基礎論学会の論文
- 1989-03-05