The Forcing Theorem and Formal Consistency Transfer: Examples and Counterexamples

Induct on the sorted pair of membership ranks of x,y to compute equality. If $x=y$, given any entry $⟨\check{u},s⟩\in \check{x}$ and any $q\le p,s$, take the entry $⟨\check{u},q⟩\in \check{y}$ and r=q. The induction hypothesis gives $q⊩\check{u}=\check{u}$, since u is a member of both x and y and both ranks decreased. Thus both subset clauses hold at p. If $x\mathrm{\ne }y$, choose a member u of one of the two differences, say $u\in x\setminus y$. The entry $⟨\check{u},p⟩\in \check{x}$ and common extension q=p have no witness in $\check{y}$: every $v\in y$ differs from u, and the equality induction says no r forces $\check{u}=\check{v}$. The subset clause fails, hence so does equality. The other difference gives the symmetric failure. If both sets are empty the two subset clauses are vacuous, starting the induction.

Suppose $x\in y$. For any $q\le p$, the entry $⟨\check{x},q⟩\in \check{y}$ together with r=q is a membership witness: equality of $\check{x}$ with itself was proved in step 1.1 for every ground x and every condition. Hence p forces membership. If $x\mathrm{\notin }y$, every candidate $v\in y$ differs from x, so step 1.1 excludes its equality witness at every r. The membership witness set is empty and cannot be dense below p, since p itself has no refinement in it. Thus no condition forces membership.

These are exactly both biconditionals. For example, putting $x=\mathrm{\varnothing }$ and $y=\{\mathrm{\varnothing }\}$ gives forced membership and failed equality at every condition, while $x=y=\mathrm{\varnothing }$ gives forced equality and failed membership. The coefficient computations above use no maximal antichain, generic existence or AC.

A nonempty filter in the singleton preorder must be $\{1\}$. Every dense subset contains 1, since 1's only extension is itself. Hence G meets every ground dense subset and is the unique M-generic. Here G=P belongs to M.

For any ground name tau, its valuation recursion using G can be carried out inside M since G is a set in M and M satisfies ZF. It agrees with the external recursion: every subname and its sole possible coefficient are in M, and induction on name rank identifies the predecessor values and their set image at each step. Thus ${\tau }_G\in M$. This gives $M[G]\subseteq M$, while F2 gives $M\subseteq M[G]$. Consequently $M[G]=M$.

F1 says that truth at the valuations is equivalent to a member of G forcing the formula. Its only member is 1, and the extension is exactly M by step 2.1. These substitutions prove the first display; F2 then replaces check-name values by the original parameters. For example empty and singleton names have values $\mathrm{\varnothing }$ and $\{\mathrm{\varnothing }\}$, so 1 forces $\check{\mathrm{\varnothing }}\in \check{\{\mathrm{\varnothing }\}}$ and does not force their equality. No Choice is used.

For the formula $\check{p}\in \dot{G}$, a membership witness r in F1 must lie below one of the three displayed coefficients and force check p equal to that coefficient's check name. By F4, the entries with coefficients 1 and q cannot qualify. The entry with coefficient p qualifies exactly when $r\le p$. Since p is an atom, the full witness set is therefore precisely $\{p\}$.

This witness set is dense below p: the only condition below p is p itself. It is not dense below 1: q is below 1 and its only refinement is q, which is not p. Thus $p⊩\check{p}\in \dot{G}$ and $1⊮\check{p}\in \dot{G}$, despite $p\le 1$. The proposed persistence to weaker conditions is false.

F2 gives exactly the valid direction: if a condition forces a formula, every stronger condition does. The calculation uses neither the existence of a generic nor AC, and it distinguishes failure to force at 1 from forcing the negation at 1. In fact 1 cannot force that negation, since its extension p forces the formula.

The conditions a and a' have the same extension set A, hence are mutually ${\le }^{\ast }$-equivalent. Neither is equivalent to b, which is incompatible with both. Also 1 is not ${\le }^{\ast }$-below either atom: the other atom witnesses failure. Thus the quotient classes are exactly $\{1\},A,B$, with the two atom classes below the top.

Downward open subsets of P are exactly $\mathrm{\varnothing },A,B,A\cup B,P$. The closure of A is $A\cup \{1\}$, since a condition is in its closure exactly when its extension cone meets A; its interior is A because the cone below 1 also includes b. Likewise B regularizes to B. The set $A\cup B$ meets every cone, so its closure and regularization are P. Therefore the regular opens are exactly the four sets displayed. Their meets are intersections, their complements exchange A and B and exchange empty and P, and $A\vee B=P$. The nonzero order is the same three-point order as the quotient; Boolean zero is omitted.

Every P-generic meets the ground dense set $A\cup B$. If it meets A, upward closure and the mutual inequalities force it to be $G_A=\{1,a,a^{\mathrm{\prime }}\}$; if it meets B it is $G_B=\{1,b\}$. It cannot meet both by directedness. Conversely these two filters meet every dense set: such a set must contain some member of A and must contain b, by testing a and b themselves. Hence these are exactly the generics. The quotient generics are $\{1,A\},\{1,B\}$ and the Boolean generics are $\{P,A\},\{P,B\}$, by the identical atom argument. They exist through every condition. All six filters are finite sets in M.

Let $e:P\to \mathrm{RO}(P{)}^{+}$ send 1 to P, a and a' to A, and b to B. Recursively replace each coefficient s of a name by e(s), translating its subnames at the same time. For the listed corresponding generic pair $(G_A,H_A)$ or $(G_B,H_B)$, s belongs to the first filter exactly when e(s) belongs to the second. Induction on name rank in F4 therefore proves equality of valuations. For the quotient use the identical construction with coefficients replaced by their classes. Conversely replace coefficients A,B and the top by the fixed representatives a,b and 1 respectively, recursively on names; the same coefficient test proves agreement in the reverse direction. These are three explicitly fixed representatives, not a choice from an arbitrary family of classes.

For each of these finite ground filters, valuation of a name in M can be performed internally in M and agrees with the external recursion by induction on subnames. Thus all name values lie in M. F5 gives the reverse inclusion, so each generic extension is M itself.

By step 2.1 generics exist through every condition, so F3 applies. The generic lists correspond bijectively and, by step 3.1, translated parameters have equal values in the identical models of step 3.2. Therefore the truth test in all corresponding generics gives equal forced formulas at corresponding conditions. For instance the top has two generic tests, whereas either atom has just its one test; duplicate a and a' give the same test. This completes the quotient, Boolean and name computations without AC.

Under Con(S), apply F3 to obtain a set model K of $S+\mathrm{\neg }\mathrm{TM}(\mathrm{Z}\mathrm{F}\mathrm{C})$. Inside K, Con(ZFC) holds and there is no transitive model of ZFC, hence no countable transitive one either. This is an actual model witness against derivability of the asserted consistency-to-CTM implication in ZFC. It is not asserted that K is externally well-founded or that Con(S) follows from Con(ZFC).

Independently, under external Con(ZFC), F5 verifies the arithmetic and standard derivability conditions for ZFC. F4 therefore gives $\mathrm{Z}\mathrm{F}\mathrm{C}⊬\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C})$. Thus the claimed internal proof of its own consistency cannot be furnished by forcing or by any other ZFC argument under this premise.

F1 begins with a full CTM as a hypothesis; applying it preserves that hypothesis and supplies no missing model-existence proof. F2 instead transforms verified finite-fragment constructions into a conditional Con implication. Accordingly neither theorem licenses the false inference, and the two precise failures in steps 1.1 and 1.2 refute its two assertions without confusing full CTMs with finite reflected fragments.

Let $P=2^{<\omega }$, ordered by extension, with stronger strings below weaker ones. Appending $0$ and appending $1$ gives two incompatible stronger conditions below every $p$, so $P$ is nonempty and atomless. If $M$ is a transitive ground model containing $P$ and $G$ is $M$-generic, F3 gives $G\mathrm{\notin }M$, while the generic-extension construction gives $G\in M[G]$.

If the ground and extension satisfy $K_L$, F4 gives them the same ordinals and F2 gives $L^{M[G]}=L^M\subseteq M$. Step 1.1 then gives $G\in M[G]\setminus L^{M[G]}$, and therefore $M[G]\models V\mathrm{\ne }L$.

Put $U=\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{\neg }(V=L)$ and fix an external finite $\mathrm{\Delta }\subseteq U$. Let ${\mathrm{\Delta }}_0$ be its ZFC-labelled members. Enlarge ${\mathrm{\Delta }}_0$ by $K_L$ and by the finitely many target-side ZF instances used in the fixed proofs of generic-extension transitivity, membership of $G$ in the extension and ordinal preservation. For each sentence in this finite enlarged list, expand the corresponding forcing-theorem and extension-axiom proof for $P=2^{<\omega }$. Also retain on the source side $K_L$ and the finitely many instances used to construct $P$, enumerate the ground dense sets, prove the direct atomlessness argument of step 1.1 and carry out the rank proof behind F4. This is one finite formal forcing verification, obtained separately for this fixed $\mathrm{\Delta }$; it makes no uniform assertion over coded fragments.

Apply F5 to the verification in step 3.1. It gives a finite $\mathrm{\Gamma }\subseteq \mathrm{Z}\mathrm{F}\mathrm{C}$ and ZFC proofs of a countable transitive $\mathrm{\Gamma }$-model $M$ and of the corresponding extension $N=M[G]$ satisfying the enlarged target list. The retained source requirements make $M$ a $K_L$-model; the enlarged target list makes $N$ a $K_L$-model. The retained fixed proof blocks give $G\in N\setminus M$ and equality of their ordinals, so F2 gives $N\models \mathrm{\neg }(V=L)$. Consequently the same ZFC conversion proof ends with a set model of the original $\mathrm{\Delta }$, including its extra axiom when that axiom occurs.

Since step 4.1 supplies the two stipulated ZFC proofs for every external finite $\mathrm{\Delta }\subseteq U$, F6 yields externally $\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C})\to \mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{\neg }(V=L))$. Together with F1, the stated $\mathrm{Con}(\mathrm{Z}\mathrm{F})$ hypothesis therefore gives $\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{\neg }(V=L))$.

Suppose instead that ZF proved $V=L$. The same finite derivation is a ZFC derivation. Appending it to the distinguished axiom $\mathrm{\neg }(V=L)$ and then the fixed propositional contradiction block would be a $\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{\neg }(V=L)$ refutation, contrary to step 5.1. Hence, assuming $\mathrm{Con}(\mathrm{Z}\mathrm{F})$, ZF does not prove $V=L$. The inner-model theorem proves a relativized assertion about the subclass $L$; it does not identify every ambient set with a constructible set.