Heyting valued universes of intuitionistic set theory

Author(s):  
Gaisi Takeuti ◽  
Satoko Titani
1985 ◽  
Vol 50 (4) ◽  
pp. 895-902 ◽  
Author(s):  
R. C. Flagg

In [6] Gödel observed that intuitionistic propositional logic can be interpreted in Lewis's modal logic (S4). The idea behind this interpretation is to regard the modal operator □ as expressing the epistemic notion of “informal provability”. With the work of Shapiro [12], Myhill [10], Goodman [7], [8], and Ščedrov [11] this simple idea has developed into a successful program of integrating classical and intuitionistic mathematics.There is one question quite central to the above program that has remained open. Namely:Does Ščedrov's extension of the Gödel translation to set theory provide a faithful interpretation of intuitionistic set theory into epistemic set theory?In the present paper we give an affirmative answer to this question.The main ingredient in our proof is the construction of an interpretation of epistemic set theory into intuitionistic set theory which is inverse to the Gödel translation. This is accomplished in two steps. First we observe that Funayama's theorem is constructively provable and apply it to the power set of 1. This provides an embedding of the set of propositions into a complete topological Boolean algebra . Second, in a fashion completely analogous to the construction of Boolean-valued models of classical set theory, we define the -valued universe V(). V() gives a model of epistemic set theory and, since we use a constructive metatheory, this provides an interpretation of epistemic set theory into intuitionistic set theory.


1999 ◽  
Vol 64 (2) ◽  
pp. 486-488 ◽  
Author(s):  
John L. Bell

By Frege's Theorem is meant the result, implicit in Frege's Grundlagen, that, for any set E, if there exists a map υ from the power set of E to E satisfying the conditionthen E has a subset which is the domain of a model of Peano's axioms for the natural numbers. (This result is proved explicitly, using classical reasoning, in Section 3 of [1].) My purpose in this note is to strengthen this result in two directions: first, the premise will be weakened so as to require only that the map υ be defined on the family of (Kuratowski) finite subsets of the set E, and secondly, the argument will be constructive, i.e., will involve no use of the law of excluded middle. To be precise, we will prove, in constructive (or intuitionistic) set theory, the followingTheorem. Let υ be a map with domain a family of subsets of a set E to E satisfying the following conditions:(i) ø ϵdom(υ)(ii)∀U ϵdom(υ)∀x ϵ E − UU ∪ x ϵdom(υ)(iii)∀UV ϵdom(5) υ(U) = υ(V) ⇔ U ≈ V.Then we can define a subset N of E which is the domain of a model of Peano's axioms.


Author(s):  
Jaykov Foukzon

In this paper intuitionistic set theory INC#∞# in infinitary set theoretical language is considered. External induction principle in nonstandard intuitionistic arithmetic were derived. Non trivial application in number theory is considered.The Goldbach-Euler theorem is obtained without any references to Catalan conjecture. Main results are: (i) number ee is transcendental; (ii) the both numbers e + π and e − π are irrational.


Sign in / Sign up

Export Citation Format

Share Document