term models for ZFC and related theories
David Libert
The usual construction of free groups is a method to construct a model for the theory of groups.
We make a formal language for the theory, creating closed terms in the language, of some starting
constant symbols, and iterated operator application expressions.
The basic operations of the theory are interpreted as formal application of the operator symbols.
We define an equivalence relation induced by what terms the theory proves are =.
So the final model has individuals being equivalence classes of terms by this equivalence relation,
and the operators are the quotienting of formal application.
What about making a term model for impredicative theories, like ZF or analysis?
In their original formultation they include existential axioms with no corresponding function
symbols, but that is easy to fix with a modification. Create new function symbols corresponding
to these existential axioms. In cases wherre the existential conclusion is contigent on a premise,
we can axiomatize that the corresponding fucntion result is some special trivial case, to allow
those functions to be total even when the original axiom wasn't. So the existential axioms
can be witnessed by formal application of the fucntoon symbol.
In the group theorty case we also had to interpret =, which was dome by te defined equivalence
relation.
For ZF or analysis, we must interpret = and also epsilon : membership. As with group theory
this will be an extra step an requires its own definition.
For ZF or analysis and other set like theories, there can be a simple interpretation of =
based on the epsilon interpretation: coextensiveness over epsilon. So for these cases it
all reduces to interpreting epsilon.
This is not easy to do for impredicative theories. To interpret epsilon of some set
term s into an abstrraction term a, you are led to check whether s satisfies the
definiting condition for a, and so led back to epsilon questions about s, including
the very s epsilon a question you are trying ot answer, since quantifiers appearing
in a range over a itself.
Or suppose you tried to somehow break such a construction into stages, only deciding
epsilon for some terms to start, and using that to extend to others. Once you create
new terms, or consider more terms with epsilon defined the meaning of quantification
has changed, so you no longer know your previous steps still witness the existenaials
they were suppsed to.
Anyway, the simple free group construction can be formalized in ZFC. But if we found
similar straightforward constructions of a ZF term model, they too as simple constuctions
should be formalizable in ZFC, so ZFC would prove the existence of a term model for
ZF, and hence Con(ZF), contrary to Godel's theorem incompleteness theorem and
L construction for AC.
So its not easy to see how to make term models for impredicative theories, and these
general considerations say we should expect it to be difficult.
I have just realized what I think are some interesting solutions, subject to caveats
to get around difficulties over incompleteness.
I will discuss getting term models for various theories, sometimes under an assumption.
I will start by discussing in more detail the exact term langauges for variups cases.
So ZFC to start. Make a constant symbol for emptyset, and for omega. Mkae a unary
function symbol for the powerset operation. Make a unary union symbol as from the
union aciom in ZFC: for the union of all the members of a set.
Make set abstraction terms corresponding to the separation axiom. These bind
one free variable which define memebrship. Since we are only doing separation
and not unbouned Frege style compregension these terms also have a term for
a larger set from which we are separating: {x epsilon S | phi(x)}.
Make terms corresonding to replacement. These will bind 2 free variables, since
the inner formula is to define a function.
Don't put any function symbols in specifically for AC, even when we target a theory
including it.
For Zermelo set theory, leave off the replacement terms.
For analysis, have a two sorted language with number variables and set variables, for
set of numbers. Have numbere constants 0 amd 1. Have function symbols +, * . And
set abstraction terms binding a single free number variable to define sets of numbers.
For simple type theory, omega types over numbers, do the obvious generalization
of analysis to higer types.
Ig you want to do term models for theories of ZFC and large cardinals, put in
individual constant symbols for the large cardinals. Or if you want one for
a theory of infiintely mnay large cardinals, say for example omaga many
inaccessibles, put in a function symbol for a function enunrating these.
So in all these cases, obtain language were all the existential axioms other
tham AC, are assrting the existence of a term named usnig the new function symbol.
By my comments about = above, all these set style theories have the problem
of giving a term model amount to giving E the interpretatiion of epsilon.
A successful term model should have E well defined over the coextentsive equivalence
relation, and should have all the abstraction terms and replacement terms if any
correctly evaluating E relations on elements according to the defining formula
with its epsilon iterpreted by that E, and with quantrifiers in those formuklas
just ranging over terms.
For the object theories above below ZF (analysis, type theory, Zermelo theory)
I think I have proven that ZF does prove term models exist (ie there are sutabable
E inrtepretting epsilon as noted above), and in fact definable term models exist
as I say in more detail below.
For making a term model for ZF, we can't prove that from just ZF unless ZF is
inconsistent. For that case though I can conclude somethng in meta-theories
ZF + Con(ZF) as one case, and also meta-theory ZF + ZF has well-founded
models to get more info.
For large cardinals above ZF, I would work in meta-theories
ZF + Con(the large cardinal theory) or in
ZF + the large cardinal theory has well-founded models.
So here is what I think I have. For analysis and simple type theory,
there is a delta-0-2 E making a model. (regarding E as a binary relation
on Godel numbers of terms).
These models have a notion of binary relations (via pairing functions), coded
as a set, and given such a binary realtion, the model can express whether they
asre weel founded. For example for analysis this would be binary relastions on
numbers, and whether those are well-founded.
Then there are also delta-1-2 E's making models of analysis and simple
type theory which are correct for well foundedness: any retation the model
says is well founded really is well founded.
For Zermelo theory, the following is also claimed to be provable in ZF.
There is a delta-1-2 E making a well-founded ZC model
(Zermelo theory inclding choice) .
(For Zermelo theory, I don't know whether we can get delta-0-2 models).
For ZF, in meta-theory ZF + Con(ZF), there is a delta-0-2 E making
a ZFC term model.
In meta-theory ZF + ZF has well-founded models, there is a delta-1-2
E making a well-founded ZFC model.
For large cardinals. The easy ones are inaccessibles, hyperinaccessibles etc, and
meassurable cardinals. Also higher order measurables as in Mitchell's theories.
We can cionsider theories expressing easy propostions about how many of these there
are such as 5 inaccessibles, or a proper class of inaccessibles. Simple expressions
of numbers of these.
So these go like the ZFC case. The basic version and the wellfounded version.
Each assumes Con() or well founded models, and gets delta-0-2 or delta-1-2.
I will comment more on the ZFC case. Similar comments apply to the other cases.
The 2 versions in questiion, basic Con() version or well-founded version, in each
case there are actually many different E at the respective delta-0-2 or
delta-1-2. You can do similar for any forcing extension of ZFC by a defniable
forcing. So you could have one E making CH true, and another makign it false.
Also, about the well founded case. In the assumption there are well-founded
models of ZF, there is a smallest well-founded ZFC model. Every well-founded
model of ZF end extends this model.
One of the delta-1-2 definitions of a ZFC term model is isomorphic to this
model. The definittion of this model, uniquely chatracterzing it up to
isomorphism, namely being the smallest well-founded model is itself be
incorporated as side clauses in the delta--1-2 definition, and it
keeps the overall defintion as no more than delta-1-2.