Related papers: An introdution to forcing
The purpose of this article is to give a presentation of the method of forcing aimed at someone with a minimal knowledge of set theory and logic. The emphasis will be on how the method can be used to prove theorems in ZFC.
This is an introduction to the set-theoretic method of forcing, including its application in proving the independence of the Continuum Hypothesis from the Zermelo-Fraenkel axioms of set theory. I presuppose no particular mathematical…
The foundations of forcing theory are reworked to streamline the presentation and to show how the most basic results are applicable in very general contexts.
In the present paper we are interested in simple forcing notions and Forcing Axioms. A starting point for our investigations was the article [JR1] in which several problems were posed. We answer some of those problems here.
This expository paper, aimed at the reader without much background in set theory or logic, gives an overview of Cohen's proof (via forcing) of the independence of the continuum hypothesis. It emphasizes the broad outlines and the intuitive…
The forcing theorem is the most fundamental result about set forcing, stating that the forcing relation for any set forcing is definable and that the truth lemma holds, that is everything that holds in a generic extension is forced by a…
These are lecture notes from a course I gave at the University of Wisconsin during the Spring semester of 1993. Part 1 is concerned with Borel hierarchies. Section 13 contains an unpublished theorem of Fremlin concerning Borel hierarchies…
We deal with an iteration theorem of forcing notion with a kind of countable support of nice enough forcing notion which is proper aleph_2-c.c. forcing notions. We then look at some special cases (Q_D 's preceded by random forcing).
It was realized early on that topologies can model constructive systems, as the open sets form a Heyting algebra. After the development of forcing, in the form of Boolean-valued models, it became clear that, just as over ZF any…
We bring forward a logical system of transition algebras that enhances many-sorted first-order logic using features from dynamic logics. The sentences we consider include compositions, unions, and transitive closures of transition…
The purpose of this paper is to investigate forcing as a tool to construct universal models. In particular, we look at theories of initial segments of the universe and show that any model of a sufficiently rich fragment of those theories…
What are the most general principles in set theory relating forceability and truth? As with Solovay's celebrated analysis of provability, both this question and its answer are naturally formulated with modal logic. We aim to do for…
We lay the ground for an Isabelle/ZF formalization of Cohen's technique of forcing. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize the definition of forcing notions as…
The modal logic of forcing arises when one considers a model of set theory in the context of all its forcing extensions, interpreting necessity as "in all forcing extensions" and possibility as "in some forcing extension". In this modal…
We give a brief survey on the interplay between forcing axioms and various other non-constructive principles widely used in many fields of abstract mathematics, such as the axiom of choice and Baire's category theorem. First of all we…
We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper generic extension and show that the latter also satisfies…
In this article we present a technique for selecting models of set theory that are complete in a model-theoretic sense. Specifically, we will apply Robinson infinite forcing to the collections of models of ZFC obtained by Cohen forcing.…
We investigate how set-theoretic forcing can be seen as a computational process on the models of set theory. Given an oracle for information about a model of set theory $\langle M,\in^M\rangle$, we explain senses in which one may compute…
The technique of "classical realizability" is an extension of the method of "forcing"; it permits to extend the Curry-Howard correspondence between proofs and programs, to Zermelo-Fraenkel set theory and to build new models of ZF, called…
A central theme in set theory is to find universes with extreme, well-understood behaviour. The case we are interested in is assuming GCH and has a strong forcing axiom of higher order than usual. Instead of "for every suitable forcing…