A sequence of decidable finitely axiomatizable intermediate logics with the disjunction property
A sequence of decidable finitely axiomatizable intermediate logics with the disjunction property
复制标题
具有析取性质的可判定有限公理化中间逻辑序列
DOI：
10.2307/2272344
复制
发表时间：
1974
影响因子：
0.6
通讯作者：
D. D. Jongh
中科院分区：
文献类型：
--
作者：
D. Gabbay;D. D. Jongh
直觉主义命题逻辑I具有以下（析取）性质。我们感兴趣的直觉逻辑的扩展，这是既可判定的，并具有析取属性。具有析取性质的系统是已知的，例如Kreisel-Putnam系统[1]，它是I +（→（α））→（（→）（→α））和Scott系统I +（（→）→（））→（）。在[3c]中表明，第一个系统具有有限模型性质。在本文中，我们将构造一个具有以下性质的中间逻辑序列Dn：这些系统在语义和句法上都是利用偏序集的性质与直觉逻辑的公理模式之间的显著对应来表示的。这种对应，除了本身是有趣的（为给予几何意义的直觉公理），也是有用的独立性证明和获得证明理论结果的直觉系统（例如，见C。Smorynski，论文，伊利诺伊大学，1972年，独立性和证明理论的结果在海廷算术）。
The intuitionistic propositional logic I has the following (disjunction) property . We are interested in extensions of the intuitionistic logic which are both decidable and have the disjunction property. Systems with the disjunction property are known, for example the Kreisel-Putnam system [1] which is I + (∼ϕ → (ψ ∨ α))→ ((∼ϕ→ψ) ∨ (∼ϕ→α)) and Scott's system I + ((∼ ∼ϕ→ϕ)→(ϕ ∨ ∼ϕ))→ (∼∼ϕ ∨ ∼ϕ). It was shown in [3c] that the first system has the finite-model property. In this note we shall construct a sequence of intermediate logics Dn with the following properties: These systems are presented both semantically and syntactically, using the remarkable correspondence between properties of partially ordered sets and axiom schemata of intuitionistic logic. This correspondence, apart from being interesting in itself (for giving geometric meaning to intuitionistic axioms), is also useful in giving independence proofs and obtaining proof theoretic results for intuitionistic systems (see for example, C. Smorynski, Thesis, University of Illinois, 1972, for independence and proof theoretic results in Heyting arithmetic).