Class forcing and second-order arithmetic

Abstract

We provide a framework in a generalization of Gödel-Bernays set theory for performing class forcing. The forcing theorem states that the forcing relation is a (definable) class in the ground model (definability lemma) and that every statement that holds in a class-generic extension is forced by a condition in the generic filter (truth lemma). We prove both positive and negative results concerning the forcing theorem. On the one hand, we show that the definability lemma for one atomic formula implies the forcing theorem for all formulae in the language of set theory to hold. Furthermore, we introduce several properties which entail the forcing theorem. On the other hand, we give both counterexamples to the definability lemma and the truth lemma. In set forcing, the forcing theorem can be proved for all forcing notions by constructing a unique Boolean completion. We show that in class forcing the existence of a Boolean completion is essentially equivalent to the forcing theorem and, moreover, Boolean completions need not be unique. <br /> The notion of pretameness was introduced to characterize those forcing notions which preserve the axiom scheme of replacement. We present several new characterizations of pretameness in terms of the forcing theorem, the preservation of separation, the existence of nice names for sets of ordinals and several other properties. Moreover, for each of the aforementioned properties we provide a corresponding characterization of the Ord-chain condition.<br /> Finally, we prove two equiconsistency results which compare models of <strong>ZFC</strong> (with large cardinal properties) and models of second-order arithmetic with topological regularity properties (and determinacy hypotheses). We apply our previous results on class forcing to show that many important arboreal forcing notions preserve the boldface <strong>Pi_1^1</strong>-perfect set property over models of second-order arithmetic and also give an example of a forcing notion which implies the boldface <strong>Pi_1^1</strong>-perfect set property to fail in the generic extension.

Wir führen Klassenforcing im axiomatischen Rahmen einer Verallgemeinerung von Gödel- Bernays-Mengenlehre ein. Das Forcing-Theorem besagt, dass die Forcingrelation eine (definierbare) Klasse im Grundmodell ist (Definierbarkeitslemma), und dass jede Aussage in einer generischen Erweiterung von einer Bedingung im generischen Filter erzwungen wird (Wahrheitslemma). Wir beweisen sowohl positive als auch negative Resultate über das Forcing-Theorem. Einerseits zeigen wir, dass das Definierbarkeitslemma für eine einzige atomare Formel reicht, um das Forcing-Theorem für alle Formeln in der Sprache der Mengenlehre zeigen. Außerdem stellen wir mehrere kombinatorische Eigenschaften von Klassenforcings vor, welche das Forcing-Theorem implizieren. Andrerseits präsentieren wir Gegenbeispiele für das Definierbarkeitslemma sowie für das Wahrheitslemma im Kontext von Klassenforcing. Im Mengenforcing ist das Forcing-Theorem eine Konsequenz der Existenz einer eindeutigen Booleschen Vervollständigung. Wir zeigen, dass im Klassenforcing die Existenz einer Booleschen Vervollständigung im Wesentlichen äquivalent zum Forcing-Theorem ist, und dass Boolesche Vervollständiungen im Allgemeinen nicht eindeutig sind. <br /> Pretameness ist eine Eigenschaft von Klassenforcings, welche definiert wurde um die Erhaltung des Ersetzungsaxioms zu charakterisieren. Wir beweisen mehrere neue Charakterisierungen von Pretameness anhand des Forcing-Theorems, der Erhaltung des Aussonderungsaxioms, der Existenz von Nice Names für Mengen von Ordinalzahlen sowie weiteren Eigenschaften von Klassenforcings. Des Weiteren verwenden wir alle diese Eigenschaften um die Ord-Kettenbedingung zu charakterisieren. <br /> Zu guter Letzt geben wir zwei Äquikonsistenzresultate an, welche Modelle von <strong>ZFC</strong> (mit grossen Kardinalzahlen) und Modelle der zweistufigen Arithmetik mit topologischer Regularität (und Determiniertheit) vergleichen. Wir wenden unsere Resultate über Klassenforcing an um nachzuweisen, dass zahlreiche wichtige Beispiele von Baumforcings die <strong>Π¹₁</strong>-perfekte-Teilmengeneigenschaft über Modelle der zweistufigen Arithmetik erhalten. Andrerseits erläutern wir ein Beispiel eines Klassenforcings, welches die <strong>Π¹₁</strong>-perfekte- Teilmengeneigenschaft in generischen Erweiterungen zerstört.