A Logic Stronger Than Intuitionism
A Logic Stronger Than Intuitionism
复制标题
逻辑比直觉更强
DOI：
10.2307/2270260
复制
发表时间：
1971
期刊：
影响因子：
--
通讯作者：
Sabine Gornemann
中科院分区：
文献类型：
--
作者：
Sabine Gornemann
S. a . Kripke给出了直觉谓词逻辑的一个非常简单的模型概念。Kripke的模型由一个拟序（C,≤）和一个函数ψ组成，该函数赋给每个C∈C一个经典逻辑模型，使得如果C≤C ', ψ (C ')大于或等于ψ (C)。Grzegorczyk[3]描述了一类更简单的模型：他对每个ψ (c)取同一个宇宙。Grzegorczyk的语义学不适用于直觉主义逻辑，因为公式中，在α中，x不是自由的。在他的模型中成立，但不能凭直觉证明。对于Grzegorczyk的语义，由公理方案(D)加强的直觉谓词演算是正确和完备的，这是D. Klemke的一个猜想。这已经被D. Klemke和我用类似henkin的方法独立地证明了；D. Gabbay b[1]给出了另一个证明。我们的证明使用格理论方法。
S. A. Kripke has given [6] a very simple notion of model for intuitionistic predicate logic. Kripke's models consist of a quasi-ordering ( C , ≤) and a function ψ which assigns to every c ∈ C a model of classical logic such that, if c ≤ c′ , ψ ( c′ ) is greater or equal to ψ ( c ). Grzegorczyk [3] described a class of models which is still simpler: he takes, for every ψ ( c ), the same universe. Grzegorczyk's semantics is not adequate for intuitionistic logic, since the formula where х is not free in α . holds in his models but is not intuitionistically provable. It is a conjecture of D. Klemke that intuitionistic predicate calculus, strengthened by the axiom scheme (D), is correct and complete with respect to Grzegorczyk's semantics. This has been proved independently by D. Klemke [5] by a Henkinlike method and me; another proof has been given by D. Gabbay [1]. Our proof uses lattice-theoretical methods.