A linear conservative extension of Zermelo-Fraenkel set theory

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.

Download Full-text

Some properties of epistemic set theory with collection

Journal of Symbolic Logic ◽

10.2307/2274028 ◽

1986 ◽

Vol 51 (3) ◽

pp. 748-754 ◽

Cited By ~ 1

Author(s):

Andre Scedrov

Keyword(s):

Set Theory ◽

Intuitionistic Logic ◽

Existential Quantifier ◽

Modal Interpretation ◽

Conservative Extension ◽

Disjunction Property ◽

First Order ◽

Slight Extension ◽

Order Arithmetic ◽

Epistemic Systems

Myhill [12] extended the ideas of Shapiro [15], and proposed a system of epistemic set theory IST (based on modal S4 logic) in which the meaning of the necessity operator is taken to be the intuitive provability, as formalized in the system itself. In this setting one works in classical logic, and yet it is possible to make distinctions usually associated with intuitionism, e.g. a constructive existential quantifier can be expressed as (∃x) □ …. This was first confirmed when Goodman [7] proved that Shapiro's epistemic first order arithmetic is conservative over intuitionistic first order arithmetic via an extension of Gödel's modal interpretation [6] of intuitionistic logic.Myhill showed that whenever a sentence □A ∨ □B is provable in IST, then A is provable in IST or B is provable in IST (the disjunction property), and that whenever a sentence ∃x.□A(x) is provable in IST, then so is A(t) for some closed term t (the existence property). He adapted the Friedman slash [4] to epistemic systems.Goodman [8] used Epistemic Replacement to formulate a ZF-like strengthening of IST, and proved that it was a conservative extension of ZF and that it had the disjunction and existence properties. It was then shown in [13] that a slight extension of Goodman's system with the Epistemic Foundation (ZFER, cf. §1) suffices to interpret intuitionistic ZF set theory with Replacement (ZFIR, [10]). This is obtained by extending Gödel's modal interpretation [6] of intuitionistic logic. ZFER still had the properties of Goodman's system mentioned above.

Download Full-text

Omitting types in set theory and arithmetic

Journal of Symbolic Logic ◽

10.1017/s0022481200051719 ◽

1976 ◽

Vol 41 (1) ◽

pp. 25-32 ◽

Cited By ~ 1

Author(s):

Julia F. Knight

Keyword(s):

Set Theory ◽

Conservative Extension ◽

Alternate Proof ◽

Hanf Number ◽

Omitting Types ◽

Infinite Set ◽

Models Of Set Theory

In [7] it is shown that if Σ is a type omitted in the structure = ω, +, ·, < and complete with respect to Th() then Σ is omitted in models of Th() of all infinite powers. The proof given there extends readily to other models of P. In this paper the result is extended to models of ZFC. For pre-tidy models of ZFC, the proof is a straightforward combination of the methods in [7] and in Keisler and Morley ([9], [6]). For other models, the proof involves forcing. In particular, it uses Solovay and Cohen's original forcing proof that GB is a conservative extension of ZFC (see [2, p. 105] and [5, p. 77]).The method of proof used for pre-tidy models of set theory can be used to obtain an alternate proof of the result for This new proof yields more information. First of all, a condition is obtained which resembles the hypothesis of the “Omitting Types” theorem, and which is sufficient for a theory T to have a model omitting a type Σ and containing an infinite set of indiscernibles. The proof that this condition is sufficient is essentially contained in Morley's proof [9] that the Hanf number for omitting types is so the condition will be called Morley's condition.If T is a pre-tidy theory, Morley's condition guarantees that T will have models omitting Σ in all infinite powers.

Download Full-text

An axiomatic presentation of the nonstandard methods in mathematics

Journal of Symbolic Logic ◽

10.2178/jsl/1190150046 ◽

2002 ◽

Vol 67 (1) ◽

pp. 315-325 ◽

Cited By ~ 2

Author(s):

Mauro Di Nasso

Keyword(s):

Set Theory ◽

Nonstandard Analysis ◽

Strong Form ◽

Conservative Extension ◽

Nonstandard Set Theory

AbstractA nonstandard set theory *ZFC is proposed that axiomatizes the nonstandard embedding *. Besides the usual principles of nonstandard analysis, all axioms of ZFC except regularity are assumed. A strong form of saturation is also postulated. *ZFC is a conservative extension of ZFC.

Download Full-text

Satisfaction relations for proper classes: Applications in logic and set theory

Journal of Symbolic Logic ◽

10.2178/jsl.7802010 ◽

2013 ◽

Vol 78 (2) ◽

pp. 345-368 ◽

Cited By ~ 1

Author(s):

Robert A. Van Wesep

Keyword(s):

Set Theory ◽

Predicate Logic ◽

Conservative Extension ◽

First Order ◽

Recursively Enumerable ◽

Extension Result ◽

First Order Predicate Logic

AbstractWe develop the theory of partial satisfaction relations for structures that may be proper classes and define a satisfaction predicate (⊨*) appropriate to such structures. We indicate the utility of this theory as a framework for the development of the metatheory of first-order predicate logic and set theory, and we use it to prove that for any recursively enumerable extension Θ of ZF there is a finitely axiomatizable extension *Θ′ of GB that is a conservative extension of Θ. We also prove a conservative extension result that justifies the use of ⊨* to characterize ground models for forcing constructions.

Download Full-text