Forcing (mathematics) explained
to a larger universe
by introducing a new "generic" object
.
Forcing was first used by Paul Cohen in 1963, to prove the independence of the axiom of choice and the continuum hypothesis from Zermelo–Fraenkel set theory. It has been considerably reworked and simplified in the following years, and has since served as a powerful technique, both in set theory and in areas of mathematical logic such as recursion theory. Descriptive set theory uses the notions of forcing from both recursion theory and set theory. Forcing has also been used in model theory, but it is common in model theory to define genericity directly without mention of forcing.
Intuition
Forcing is usually used to construct an expanded universe that satisfies some desired property. For example, the expanded universe might contain many new real numbers (at least
of them), identified with
subsets of the set
of natural numbers, that were not there in the old universe, and thereby violate the
continuum hypothesis.
of the set theory, which is itself a set in the "real universe"
. By the
Löwenheim–Skolem theorem,
can be chosen to be a "bare bones" model that is
externally countable, which guarantees that there will be many subsets (in
) of
that are not in
. Specifically, there is an
ordinal
that "plays the role of the
cardinal
" in
, but is actually countable in
. Working in
, it should be easy to find one distinct subset of
per each element of
. (For simplicity, this family of subsets can be characterized with a single subset
.)
However, in some sense, it may be desirable to "construct the expanded model
within
". This would help ensure that
"resembles"
in certain aspects, such as
being the same as
(more generally, that
cardinal collapse does not occur), and allow fine control over the properties of
. More precisely, every member of
should be given a (non-unique)
name in
. The name can be thought as an expression in terms of
, just like in a
simple field extension
every element of
can be expressed in terms of
. A major component of forcing is manipulating those names within
, so sometimes it may help to directly think of
as "the universe", knowing that the theory of forcing guarantees that
will correspond to an actual model.
A subtle point of forcing is that, if
is taken to be an
arbitrary "missing subset" of some set in
, then the
constructed "within
" may not even be a model. This is because
may encode "special" information about
that is invisible within
(e.g. the
countability of
), and thus prove the existence of sets that are "too complex for
to describe".
Forcing avoids such problems by requiring the newly introduced set
to be a
generic set relative to
. Some statements are "forced" to hold for any generic
: For example, a generic
is "forced" to be infinite. Furthermore, any property (describable in
) of a generic set is "forced" to hold under some
forcing condition. The concept of "forcing" can be defined within
, and it gives
enough reasoning power to prove that
is indeed a model that satisfies the desired properties.
Cohen's original technique, now called ramified forcing, is slightly different from the unramified forcing expounded here. Forcing is also equivalent to the method of Boolean-valued models, which some feel is conceptually more natural and intuitive, but usually much more difficult to apply.
The role of the model
In order for the above approach to work smoothly,
must in fact be a
standard transitive model in
, so that membership and other elementary notions can be handled intuitively in both
and
. A standard transitive model can be obtained from any standard model through the
Mostowski collapse lemma, but the existence of any standard model of
(or any variant thereof) is in itself a stronger assumption than the consistency of
.
To get around this issue, a standard technique is to let
be a standard transitive model of an arbitrary finite subset of
(any axiomatization of
has at least one
axiom schema, and thus an infinite number of axioms), the existence of which is guaranteed by the reflection principle. As the goal of a forcing argument is to prove
consistency results, this is enough since any inconsistency in a theory must manifest with a derivation of a finite length, and thus involve only a finite number of axioms.
Forcing conditions and forcing posets
Each forcing condition can be regarded as a finite piece of information regarding the object
adjoined to the model. There are many different ways of providing information about an object, which give rise to different
forcing notions. A general approach to formalizing forcing notions is to regard forcing conditions as abstract objects with a
poset structure.
A forcing poset is an ordered triple,
, where
is a
preorder on
, and
is the largest element. Members of
are the
forcing conditions (or just
conditions). The order relation
means "
is
stronger than
". (Intuitively, the "smaller" condition provides "more" information, just as the smaller interval
provides more information about the number
than the interval
does.) Furthermore, the preorder
must be
atomless, meaning that it must satisfy the
splitting condition:
, there are
such that
, with no
such that
.
In other words, it must be possible to strengthen any forcing condition
in at least two incompatible directions. Intuitively, this is because
is only a finite piece of information, whereas an infinite piece of information is needed to determine
.
There are various conventions in use. Some authors require
to also be
antisymmetric, so that the relation is a partial order. Some use the term partial order anyway, conflicting with standard terminology, while some use the term
preorder. The largest element can be dispensed with. The reverse ordering is also used, most notably by
Saharon Shelah and his co-authors.
Examples
Let
be any infinite set (such as
), and let the generic object in question be a new subset
. In Cohen's original formulation of forcing, each forcing condition is a
finite set of sentences, either of the form
or
, that are self-consistent (i.e.
and
for the same value of
do not appear in the same condition). This forcing notion is usually called
Cohen forcing.
The forcing poset for Cohen forcing can be formally written as
(\operatorname{Fin}(S,2),\supseteq,0)
, the finite partial functions from
to
} ~ \ under
reverse inclusion. Cohen forcing satisfies the splitting condition because given any condition
, one can always find an element
not mentioned in
, and add either the sentence
or
to
to get two new forcing conditions, incompatible with each other.
Another instructive example of a forcing poset is
(\operatorname{Bor}(I),\subseteq,I)
, where
and
is the collection of
Borel subsets of
having non-zero
Lebesgue measure. The generic object associated with this forcing poset is a
random real number
. It can be shown that
falls in every Borel subset of
with measure 1, provided that the Borel subset is "described" in the original unexpanded universe (this can be formalized with the concept of
Borel codes). Each forcing condition can be regarded as a random event with probability equal to its measure. Due to the ready intuition this example can provide, probabilistic language is sometimes used with other divergent forcing posets.
Generic filters
Even though each individual forcing condition
cannot fully determine the generic object
, the set
of all true forcing conditions does determine
. In fact, without loss of generality,
is commonly considered to
be the generic object adjoined to
, so the expanded model is called
. It is usually easy enough to show that the originally desired object
is indeed in the model
.
Under this convention, the concept of "generic object" can be described in a general way. Specifically, the set
should be a
generic filter on
relative to
. The "
filter" condition means that it makes sense that
is a set of all true forcing conditions:
, then
, then there exists an
such that
For
to be "generic relative to
" means:
is a "dense" subset of
(that is, for each
, there exists a
such that
), then
.
Given that
is a countable model, the existence of a generic filter
follows from the
Rasiowa–Sikorski lemma. In fact, slightly more is true: Given a condition
, one can find a generic filter
such that
. Due to the splitting condition on
, if
is a filter, then
is dense. If
, then
because
is a model of
. For this reason, a generic filter is never in
.
P-names and interpretations
Associated with a forcing poset
is the
class
of
-
names. A
-name is a set
of the form
A\subseteq\{(u,p)\midu~isa~P-nameand~p\inP\}.
Given any filter
on
, the
interpretation or
valuation map from
-names is given by
\operatorname{val}(u,G)=\{\operatorname{val}(v,G)\mid\existsp\inG:~(v,p)\inu\}.
The
-names are, in fact, an expansion of the
universe. Given
, one defines
to be the
-name
\check{x}=\{(\check{y},1)\midy\inx\}.
Since
, it follows that
\operatorname{val}(\check{x},G)=x
. In a sense,
is a "name for
" that does not depend on the specific choice of
.
This also allows defining a "name for
" without explicitly referring to
:
\underline{G}=\{(\check{p},p)\midp\inP\}
so that
\operatorname{val}(\underline{G},G)=\{\operatorname{val}(\checkp,G)\midp\inG\}=G
.
Rigorous definitions
The concepts of
-names, interpretations, and
may be defined by transfinite recursion. With
the empty set,
the
successor ordinal to ordinal
,
the
power-set operator, and
a
limit ordinal, define the following hierarchy:
\begin{align}
\operatorname{Name}(\varnothing)&=\varnothing,\\
\operatorname{Name}(\alpha+1)&=l{P}(\operatorname{Name}(\alpha) x P),\\
\operatorname{Name}(λ)&=cup\{\operatorname{Name}(\alpha)\mid\alpha<λ\}.
\end{align}
Then the class of
-names is defined as
V(P)=cup\{\operatorname{Name}(\alpha)~|~\alpha~isanordinal\}.
The interpretation map and the map
can similarly be defined with a hierarchical construction.
Forcing
Given a generic filter
, one proceeds as follows. The subclass of
-names in
is denoted
. Let
M[G]=\left\{\operatorname{val}(u,G)~|~u\inM(P)\right\}.
To reduce the study of the set theory of
to that of
, one works with the "forcing language", which is built up like ordinary
first-order logic, with membership as the binary relation and all the
-names as constants.
Define
p\VdashM,P\varphi(u1,\ldots,un)
(to be read as "
forces
in the model
with poset
"), where
is a condition,
is a formula in the forcing language, and the
's are
-names, to mean that if
is a generic filter containing
, then
M[G]\models\varphi(\operatorname{val}(u1,G),\ldots,\operatorname{val}(un,G))
. The special case
is often written as "
" or simply "
". Such statements are true in
, no matter what
is.
What is important is that this external definition of the forcing relation
is equivalent to an
internal definition within
, defined by
transfinite induction (specifically
-induction) over the
-names on instances of
and
, and then by ordinary induction over the complexity of formulae. This has the effect that all the properties of
are really properties of
, and the verification of
in
becomes straightforward. This is usually summarized as the following three key properties:
M[G]\models\varphi(\operatorname{val}(u1,G),\ldots,\operatorname{val}(un,G))
if and only if it is forced by
, that is, for some condition
, we have
p\VdashM,P\varphi(u1,\ldots,un)
.
- Definability: The statement "
p\VdashM,P\varphi(u1,\ldots,un)
" is definable in
.
p\VdashM,P\varphi(u1,\ldots,un)\landq\leqp\impliesq\VdashM,P\varphi(u1,\ldots,un)
.
Internal definition
There are many different but equivalent ways to define the forcing relation
in
. One way to simplify the definition is to first define a modified forcing relation
that is strictly stronger than
. The modified relation
still satisfies the three key properties of forcing, but
and
are not necessarily equivalent even if the first-order formulae
and
are equivalent. The unmodified forcing relation can then be defined as
In fact, Cohen's original concept of forcing is essentially
rather than
.
The modified forcing relation
can be defined recursively as follows:
means
(\exists(w,q)\inv)(q\gep\wedgep
w=u).
means
(\exists(w,q)\inv)(q\gep\wedgep
w\notinu)\vee(\exists(w,q)\inu)(q\gep\wedgep
w\notinv).
means
\neg(\existsq\lep)(q
\varphi).
means
means
(\existsu\inM(P))(p
\varphi(u)).
Other symbols of the forcing language can be defined in terms of these symbols: For example,
means
,
means
\neg\existsx\neg\varphi(x)
, etc. Cases 1 and 2 depend on each other and on case 3, but the recursion always refer to
-names with lesser
ranks, so transfinite induction allows the definition to go through.
By construction,
(and thus
) automatically satisfies
Definability. The proof that
also satisfies
Truth and
Coherence is by inductively inspecting each of the five cases above. Cases 4 and 5 are trivial (thanks to the choice of
and
as the elementary symbols
[1]), cases 1 and 2 relies only on the assumption that
is a filter, and only case 3 requires
to be a
generic filter.
Formally, an internal definition of the forcing relation (such as the one presented above) is actually a transformation of an arbitrary formula
to another formula
p\VdashP\varphi(u1,...,un)
where
and
are additional variables. The model
does not explicitly appear in the transformation (note that within
,
just means "
is a
-name"), and indeed one may take this transformation as a "syntactic" definition of the forcing relation in the universe
of all sets regardless of any countable transitive model. However, if one wants to force over some countable transitive model
, then the latter formula should be interpreted under
(i.e. with all quantifiers ranging only over
), in which case it is equivalent to the external "semantic" definition of
described at the top of this section:
For any formula
there is a theorem
of the theory
(for example conjunction of finite number of axioms) such that for any countable transitive model
such that
and any atomless partial order
and any
-generic filter
over
This the sense under which the forcing relation is indeed "definable in
".
Consistency
The discussion above can be summarized by the fundamental consistency result that, given a forcing poset
, we may assume the existence of a generic filter
, not belonging to the universe
, such that
is again a set-theoretic universe that models
. Furthermore, all truths in
may be reduced to truths in
involving the forcing relation.
Both styles, adjoining
to either a countable transitive model
or the whole universe
, are commonly used. Less commonly seen is the approach using the "internal" definition of forcing, in which no mention of set or class models is made. This was Cohen's original method, and in one elaboration, it becomes the method of Boolean-valued analysis.
Cohen forcing
The simplest nontrivial forcing poset is
(\operatorname{Fin}(\omega,2),\supseteq,0)
, the finite partial functions from
to
} ~ \ under
reverse inclusion. That is, a condition
is essentially two disjoint finite subsets
}[1] and
}[0] of
, to be thought of as the "yes" and "no" parts of with no information provided on values outside the domain of
. "
is stronger than
" means that
, in other words, the "yes" and "no" parts of
are supersets of the "yes" and "no" parts of
, and in that sense, provide more information.
Let
be a generic filter for this poset. If
and
are both in
, then
is a condition because
is a filter. This means that
is a well-defined partial function from
to
because any two conditions in
agree on their common domain.
In fact,
is a total function. Given
, let
Dn=\{p\midp(n)~isdefined\}
. Then
is dense. (Given any
, if
is not in
's domain, adjoin a value for
—the result is in
.) A condition
has
in its domain, and since
, we find that
is defined.
Let
}[1] , the set of all "yes" members of the generic conditions. It is possible to give a name for
directly. Let
\underline{X}=\left\{\left(\check{n},p\right)\midp(n)=1\right\}.
Then
\operatorname{val}(\underline{X},G)=X.
Now suppose that
in
. We claim that
. Let
DA=\{p\mid(\existsn)(n\in\operatorname{Dom}(p)\land(p(n)=1\iffn\notinA))\}.
Then
is dense. (Given any
, find
that is not in its domain, and adjoin a value for
contrary to the status of "
".) Then any
witnesses
. To summarize,
is a "new" subset of
, necessarily infinite.
Replacing
with
, that is, consider instead finite partial functions whose inputs are of the form
, with
and
, and whose outputs are
or
, one gets
new subsets of
. They are all distinct, by a density argument: Given
, let
D\alpha,\beta=\{p\mid(\existsn)(p(n,\alpha) ≠ p(n,\beta))\},
then each
is dense, and a generic condition in it proves that the αth new set disagrees somewhere with the
th new set.
This is not yet the falsification of the continuum hypothesis. One must prove that no new maps have been introduced which map
onto
, or
onto
. For example, if one considers instead
\operatorname{Fin}(\omega,\omega1)
, finite partial functions from
to
, the
first uncountable ordinal, one gets in
a bijection from
to
. In other words,
has
collapsed, and in the forcing extension, is a countable ordinal.
The last step in showing the independence of the continuum hypothesis, then, is to show that Cohen forcing does not collapse cardinals. For this, a sufficient combinatorial property is that all of the antichains of the forcing poset are countable.
The countable chain condition
of
is a subset such that if
and
, then
and
are
incompatible (written
), meaning there is no
in
such that
and
. In the example on Borel sets, incompatibility means that
has zero measure. In the example on finite partial functions, incompatibility means that
is not a function, in other words,
and
assign different values to some domain input.
satisfies the
countable chain condition (c.c.c.) if and only if every antichain in
is countable. (The name, which is obviously inappropriate, is a holdover from older terminology. Some mathematicians write "c.a.c." for "countable antichain condition".)
It is easy to see that
satisfies the c.c.c. because the measures add up to at most
. Also,
satisfies the c.c.c., but the proof is more difficult.
Given an uncountable subfamily
W\subseteq\operatorname{Fin}(E,2)
, shrink
to an uncountable subfamily
of sets of size
, for some
. If
for uncountably many
, shrink this to an uncountable subfamily
and repeat, getting a finite set
\{(e1,b1),\ldots,(ek,bk)\}
and an uncountable family
of incompatible conditions of size
such that every
is in
for at most countable many
. Now, pick an arbitrary
, and pick from
any
that is not one of the countably many members that have a domain member in common with
. Then
p\cup\{(e1,b1),\ldots,(ek,bk)\}
and
q\cup\{(e1,b1),\ldots,(ek,bk)\}
are compatible, so
is not an antichain. In other words,
-antichains are countable.
The importance of antichains in forcing is that for most purposes, dense sets and maximal antichains are equivalent. A maximal antichain
is one that cannot be extended to a larger antichain. This means that every element
is compatible with some member of
. The existence of a maximal antichain follows from
Zorn's Lemma. Given a maximal antichain
, let
D=\left\{p\inP\mid(\existsq\inA)(p\leqq)\right\}.
Then
is dense, and
if and only if
. Conversely, given a dense set
, Zorn's Lemma shows that there exists a maximal antichain
, and then
if and only if
.
Assume that
satisfies the c.c.c. Given
, with
a function in
, one can approximate
inside
as follows. Let
be a name for
(by the definition of
) and let
be a condition that forces
to be a function from
to
. Define a function
, by
} \left \. \right.
By the definability of forcing, this definition makes sense within
. By the coherence of forcing, a different
come from an incompatible
. By c.c.c.,
is countable.
In summary,
is unknown in
as it depends on
, but it is not wildly unknown for a c.c.c.-forcing. One can identify a countable set of guesses for what the value of
is at any input, independent of
.
This has the following very important consequence. If in
,
is a surjection from one infinite ordinal onto another, then there is a surjection
g:\omega x \alpha\to\beta
in
, and consequently, a surjection
in
. In particular, cardinals cannot collapse. The conclusion is that
in
.
Easton forcing
The exact value of the continuum in the above Cohen model, and variants like
\operatorname{Fin}(\omega x \kappa,2)
for cardinals
in general, was worked out by
Robert M. Solovay, who also worked out how to violate
(the generalized continuum hypothesis), for
regular cardinals only, a finite number of times. For example, in the above Cohen model, if
holds in
, then
holds in
.
William B. Easton worked out the proper class version of violating the
for regular cardinals, basically showing that the known restrictions, (monotonicity,
Cantor's Theorem and
König's Theorem), were the only
-provable restrictions (see
Easton's Theorem).
Easton's work was notable in that it involved forcing with a proper class of conditions. In general, the method of forcing with a proper class of conditions fails to give a model of
. For example, forcing with
\operatorname{Fin}(\omega x On,2)
, where
is the proper class of all ordinals, makes the continuum a proper class. On the other hand, forcing with
\operatorname{Fin}(\omega,On)
introduces a countable enumeration of the ordinals. In both cases, the resulting
is visibly not a model of
.
At one time, it was thought that more sophisticated forcing would also allow an arbitrary variation in the powers of singular cardinals. However, this has turned out to be a difficult, subtle and even surprising problem, with several more restrictions provable in
and with the forcing models depending on the consistency of various
large-cardinal properties. Many open problems remain.
Random reals
See main article: article and Random algebra.
Random forcing can be defined as forcing over the set
of all compact subsets of
of positive measure ordered by relation
(smaller set in context of inclusion is smaller set in ordering and represents condition with more information). There are two types of important dense sets:
- For any positive integer
the set
is dense, where
is diameter of the set
.
- For any Borel subset
of measure 1, the set
is dense.
For any filter
and for any finitely many elements
there is
such that holds
. In case of this ordering, this means that any filter is set of compact sets with finite intersection property. For this reason, intersection of all elements of any filter is nonempty. If
is a filter intersecting the dense set
for any positive integer
, then the filter
contains conditions of arbitrarily small positive diameter. Therefore, the intersection of all conditions from
has diameter 0. But the only nonempty sets of diameter 0 are singletons. So there is exactly one real number
such that
.
Let
be any Borel set of measure 1. If
intersects
, then
.
However, a generic filter over a countable transitive model
is not in
. The real
defined by
is provably not an element of
. The problem is that if
, then
"
is compact", but from the viewpoint of some larger universe
,
can be non-compact and the intersection of all conditions from the generic filter
is actually empty. For this reason, we consider the set
of topological
closures of conditions from G (i.e.,
\barp=p\cup\{inf(p)\}\cup\{\sup(p)\}
). Because of
and the finite intersection property of
, the set
also has the finite intersection property. Elements of the set
are bounded closed sets as closures of bounded sets. Therefore,
is a set of compact sets with the finite intersection property and thus has nonempty intersection. Since
\operatorname{diam}(\barp)=\operatorname{diam}(p)
and the ground model
inherits a metric from the universe
, the set
has elements of arbitrarily small diameter. Finally, there is exactly one real that belongs to all members of the set
. The generic filter
can be reconstructed from
as
.
If
is name of
, and for
holds
"
is Borel set of measure 1", then holds
V[G]\models\left(p\VdashPa\in\check{B}\right)
for some
. There is name
such that for any generic filter
holds
\operatorname{val}(a,G)\incupp\in\barp.
Then
V[G]\models\left(p\VdashPa\in\check{B}\right)
holds for any condition
.
Every Borel set can, non-uniquely, be built up, starting from intervals with rational endpoints and applying the operations of complement and countable unions, a countable number of times. The record of such a construction is called a Borel code. Given a Borel set
in
, one recovers a Borel code, and then applies the same construction sequence in
, getting a Borel set
. It can be proven that one gets the same set independent of the construction of
, and that basic properties are preserved. For example, if
, then
. If
has measure zero, then
has measure zero. This mapping
is injective.
For any set
such that
and
"
is a Borel set of measure 1" holds
.
This means that
is "infinite random sequence of 0s and 1s" from the viewpoint of
, which means that it satisfies all statistical tests from the ground model
.
So given
, a random real, one can show that
G=\left\{B~(inV)\midr\inB*~(inV[G])\right\}.
Because of the mutual inter-definability between
and
, one generally writes
for
.
A different interpretation of reals in
was provided by
Dana Scott. Rational numbers in
have names that correspond to countably-many distinct rational values assigned to a maximal antichain of Borel sets – in other words, a certain rational-valued function on
. Real numbers in
then correspond to
Dedekind cuts of such functions, that is,
measurable functions.
Boolean-valued models
See main article: article and Boolean-valued model.
Perhaps more clearly, the method can be explained in terms of Boolean-valued models. In these, any statement is assigned a truth value from some complete atomless Boolean algebra, rather than just a true/false value. Then an ultrafilter is picked in this Boolean algebra, which assigns values true/false to statements of our theory. The point is that the resulting theory has a model that contains this ultrafilter, which can be understood as a new model obtained by extending the old one with this ultrafilter. By picking a Boolean-valued model in an appropriate way, we can get a model that has the desired property. In it, only statements that must be true (are "forced" to be true) will be true, in a sense (since it has this extension/minimality property).
Meta-mathematical explanation
In forcing, we usually seek to show that some sentence is consistent with
(or optionally some extension of
). One way to interpret the argument is to assume that
is consistent and then prove that
combined with the new
sentence is also consistent.
Each "condition" is a finite piece of information – the idea is that only finite pieces are relevant for consistency, since, by the compactness theorem, a theory is satisfiable if and only if every finite subset of its axioms is satisfiable. Then we can pick an infinite set of consistent conditions to extend our model. Therefore, assuming the consistency of
, we prove the consistency of
extended by this infinite set.
Logical explanation
By Gödel's second incompleteness theorem, one cannot prove the consistency of any sufficiently strong formal theory, such as
, using only the axioms of the theory itself, unless the theory is inconsistent. Consequently, mathematicians do not attempt to prove the consistency of
using only the axioms of
, or to prove that
is consistent for any hypothesis
using only
. For this reason, the aim of a consistency proof is to prove the consistency of
relative to the consistency of
. Such problems are known as problems of
relative consistency, one of which proves
The general schema of relative consistency proofs follows. As any proof is finite, it uses only a finite number of axioms:
ZFC+lnot\operatorname{Con}(ZFC+H)\vdash(\existsT)(\operatorname{Fin}(T)\landT\subseteqZFC\land(T\vdashlnotH)).
For any given proof,
can verify the validity of this proof. This is provable by induction on the length of the proof.
ZFC\vdash(\forallT)((T\vdashlnotH) → (ZFC\vdash(T\vdashlnotH))).
Then resolve
ZFC+lnot\operatorname{Con}(ZFC+H)\vdash(\existsT)(\operatorname{Fin}(T)\landT\subseteqZFC\land(ZFC\vdash(T\vdashlnotH))).
By proving the following
it can be concluded that
ZFC+lnot\operatorname{Con}(ZFC+H)\vdash(\existsT)(\operatorname{Fin}(T)\landT\subseteqZFC\land(ZFC\vdash(T\vdashlnotH))\land(ZFC\vdash\operatorname{Con}(T+H))),
which is equivalent to
ZFC+lnot\operatorname{Con}(ZFC+H)\vdashlnot\operatorname{Con}(ZFC),
which gives (*). The core of the relative consistency proof is proving (**). A
proof of
can be constructed for any given finite subset
of the
axioms (by
instruments of course). (No universal proof of
of course.)
In
, it is provable that for any condition
, the set of formulas (evaluated by names) forced by
is deductively closed. Furthermore, for any
axiom,
proves that this axiom is forced by
. Then it suffices to prove that there is at least one condition that forces
.
In the case of Boolean-valued forcing, the procedure is similar: proving that the Boolean value of
is not
.
Another approach uses the Reflection Theorem. For any given finite set of
axioms, there is a
proof that this set of axioms has a countable transitive model. For any given finite set
of
axioms, there is a finite set
of
axioms such that
proves that if a countable transitive model
satisfies
, then
satisfies
. By proving that there is finite set
of
axioms such that if a countable transitive model
satisfies
, then
satisfies the hypothesis
. Then, for any given finite set
of
axioms,
proves
.
Sometimes in (**), a stronger theory
than
is used for proving
. Then we have proof of the consistency of
relative to the consistency of
. Note that
ZFC\vdash\operatorname{Con}(ZFC)\leftrightarrow\operatorname{Con}(ZFL)
, where
is
(the axiom of constructibility).
See also
References
- Book: Bell, John Lane. 1985. Boolean-Valued Models and Independence Proofs in Set Theory. Oxford University Press. Oxford. 9780198532415.
- Book: Cohen, Paul Joseph. 2008. 1966. Set theory and the continuum hypothesis. Mineola, New York City . Dover Publications. 978-0-486-46921-8. 151.
- Book: Jech, Thomas J.. Set Theory: The Third Millennium Edition. . 2013. 1978. 9783642078996.
- Book: Kunen, Kenneth. Set Theory: An Introduction to Independence Proofs. North-Holland Publishing Company. 1980. 978-0-444-85401-8. Set Theory: An Introduction to Independence Proofs.
- Book: Shoenfield, J. R.. Unramified forcing. 1971 . Axiomatic Set Theory . Proc. Sympos. Pure Math.. XIII, Part I. 357–381 . Amer. Math. Soc.. Providence, R.I.. 0280359.
Bibliography
- Chow. Timothy. Timothy Chow. A Beginner's Guide to Forcing. 2008. 0712.1320v2 . A good introduction to the concepts of forcing that avoids a lot of technical detail. It includes a section on Boolean-valued models..
- Cohen. Paul Joseph. The independence of the continuum hypothesis. Proceedings of the National Academy of Sciences of the United States of America. 50. 6. 1143–1148. December 1963. 10.1073/pnas.50.6.1143 . 16578557. 221287. 1963PNAS...50.1143C. free.
- Cohen. Paul Joseph. The independence of the continuum hypothesis, II. Proceedings of the National Academy of Sciences of the United States of America. 51. 1. 105–110. January 1964. 10.1073/pnas.51.1.105 . 16591132. 300611. 1964PNAS...51..105C. free.
- Cohen. Paul Joseph. The Discovery of Forcing. Rocky Mountain J. Math.. 32. 4. 2002. 1071–1100. 10.1216/rmjm/1181070010. free. A historical lecture about how he developed his independence proof..
- Easwaran. Kenny. Kenny Easwaran. A Cheerful Introduction to Forcing and the Continuum Hypothesis. 2007 . math.LO . 0712.2279 . The article is also aimed at the beginner but includes more technical details than .
- Gunther. Emmanuel. Pagano. Miguel. Sánchez Terraf. Pedro. Steinberg. Matías. Formalization of Forcing in Isabelle/ZF. Archive of Formal Proofs. May 2020. 2001.09715 . 20 August 2023.
- Web site: Kanamori. Akihiro. Akihiro Kanamori. Set theory from Cantor to Cohen. 2007.
- Book: Weaver, Nik. 2014. 978-9814566001. 153. World Scientific Publishing Co.. Written for mathematicians who want to learn the basic machinery of forcing. No background in logic is assumed, beyond the facility with formal syntax which should be second nature to any well-trained mathematician.. Forcing for Mathematicians. 10.1142/8962 .
Notes and References
- Notably, if defining
directly instead of
, one would need to replace the
with
in case 4 and
with
in case 5 (in addition to making cases 1 and 2 more complicated) to make this internal definition agree with the external definition. However, then when trying to prove Truth inductively, case 4 will require the fact that
, as a filter, is downward directed, and case 5 will outright break down.