Let us define the intuitionistic part of a classical theory T as the intuitionistic theory whose proper axioms are identical with the proper axioms of T. For example, Heyting arithmetic HA is the intuitionistic part of classical Peano arithmetic PA. It's a well-known fact, proved by Heyting and Myhill, that ZF is identical with its intuitionistic part. In this paper, we mainly prove that TT, Russell's Simple Theory of Types, and NF, Quine's "New Foundations," are not equal to their intuitionistic (...) part. So, an intuitionistic version of TT or NF seems more naturally definable than an intuitionistic version of ZF. In the first section, we present a simple technique to build Kripke models of the intuitionistic part of TT (with short examples showing bad properties of finite sets if they are defined in the usual classical way). In the remaining sections, we show how models of intuitionistic NF 2 and NF can be obtained from well-chosen classical ones. In these models, the excluded middle will not be satisfied for some non-stratified sentences. (shrink)

We show how to interpret Heyting's arithmetic in an intuitionistic version of TT, Russell's Simple Theory of Types. We also exhibit properties of finite sets in this theory and compare them with the corresponding properties in classical TT. Finally, we prove that arithmetic can be interpreted in intuitionistic TT, the subsystem of intuitionistic TT involving only three types. The definitions of intuitionistic TT and its finite sets and natural numbers are obtained in a straightforward way from the classical definitions. This (...) is very natural and seems to make intuitionistic TT an interesting intuitionistic set theory to study, beside intuitionistic ZF. (shrink)

We present a technique to extend a Kripke structure into an elementary extension satisfying some property which can be “axiomatized” by a family of sets of sentences, where, most often, many constant symbols occur. To that end, we prove extended theorems of completeness and compactness. Also, a section of the paper is devoted to the back-and-forth construction of isomorphisms between Kripke structures.

In this paper, we prove that Heyting's arithmetic can be interpreted in an intuitionistic version of Russell's Simple Theory of Types without extensionality.

A sentence of the usual language of set theory is said to be stratified if it is obtained by “erasing” type indices in a sentence of the language of Russell's Simple Theory of Types. In this paper we give an alternative presentation of a proof the ambiguity theorem stating that any provable stratified sentence has a stratified proof. To this end, we introduce a new set of ambiguity axioms, inspired by Fraïssé's characterization of elementary equivalence; these axioms can be naturally (...) used to give different proofs of the ambiguity theorem . MSC: 03B15, 03F50, 03F55. (shrink)