Intuitionistic Version of the Los-Tarski-Robinson Theorem
スポンサーリンク
概要
- 論文の詳細を見る
In his book, A. Robinson gives a generalized form of a theorem proved by Los and Tarski. The generalized theorem can be stated as follows: Let A and B be two sentences of the first order predicate logic. If any extension of any model of A is a model of B, then there exists a universal sentence M such that A→M and M→B are provable in the classical predicate logic of first order. The purpose of this paper is to prove the fact that the same theorem holds also for the intuitionistic predicate logic of first order. Our proof is purely syntactical and is based on the idea of Gentzen's cut-elimination theorem, which has been used on Motohashi's another proof of the Los-Tarski-Robinson theorem. The author express his heartly gratitude to Prof. S. Maehara who gave him valuable advice in the course of this work and Dr. N. Motohashi who directed his attention to this problem.
- 科学基礎論学会の論文
- 1975-03-25