extending ZFC
From: David Libert (ah170_at_FreeNet.Carleton.CA)
Date: 10/11/04
- Next message: Tim Smith: "Re: Trisecting an Angle"
- Previous message: Denis Feldmann: "Re: DWB: Trisecting an Angle"
- Next in thread: Ross A. Finlayson: "Re: extending ZFC"
- Reply: Ross A. Finlayson: "Re: extending ZFC"
- Messages sorted by: [ date ] [ thread ]
Date: 11 Oct 2004 06:16:02 GMT
I present here a proposal for a family of set theories. I believe these
can be a good framework for working with set theory, providing an overall
organization to various alternative approaches.
In general I like ZFC, but I think the usual formulation leaves some
subtle philosophical loose ends. I am trying to have a basis for handling
these better.
My approach below departs somewhat from the mainstream set theoretic
opinion. The usual view of what should be reasonable canonical extensions
of ZFC would be agnostic about V=L or else to believe V ~= L.
I have been led to eventually come around to accept V=L in as a part of
the basis. I am aware that this is unusual, and of the usual reasons for
accepting V ~= L, (in fact I used to believe these myself), but I have my
own reasons for coming back to V=L. I am aware that Godel, he first
defined L, did not even believe V=L.
In fact my settling on V=L does not have the full ramifications it may
first seem, because I can recover some of the non-L alternatives in an
interpreted way.
There are several distinct philosphical difficulties I had with simple
ZFC, and there are accordingly distinct aspects of my systems to handle
these. So it is something of a hodge-podge, throwing in everything but the
kitchen sink. So there are several parallel motivating ideas co-existing.
Just as I recognize including V=L as controversial as noted above, I
also even recognize AC as controversial. I do think about such aspects,
but have so far come back to the AC side.
Another big issue in looking for alternative set theories is to consider
weakening ZFC. I have considered that too, but I think in the end it does
not solve the philosphical problems it was intended to solve. In fact I
strengthen ZFC.
Strengthening to beyond ZFC is the usual approach among set theoriests.
So against the background of sci.math my strengthening may seem
controversial. Compared to usual set theorists though my version will look
different by its relative weakness. By including V=L I am holding back
from the higher levels. I have philosphical reasons for that. But along
the lines of my comments about non-L above, I do manage to recover
something of these levels less directly.
For this first post I am just going to give a bare bones description of
the systems along with the opening comments above. For now I won't go into
detail about the motivations leading me to such systems.
So on to the systems. There will be a base system. Other systems from
the same family can be produced by adding more axioms and possibly
extending the language.
The base system will have language first order with = and primitive
binary relation epsilon, two individual constants u and U, and two
binary function symbols, which I will write in forms u^beta_alpha and
U^beta_alpha, ie u's or U's with superscripts and subscripts. So
basically I have an indexed family of u's with superscripts and
subscripts, and an indexed family of U's with superscripts and
subscripts, but also I have two very important special cases that are
written without superscripts or subscripts, they will act like the
correponding letters adorned to terms, but being the most important I make
them easy to write as u and U.
The axioms will included the corresponding ZFC axioms for the expanded
language, ie we allow separation and replacement axioms for formulas with
the extra terms.
Now to get to the "V=L" aspect of the systems. This is one of the
features of the system which makes the banishment of non-L and high
consistency strength beyond L incomplete, that those aspects are still
around in the background. This was the outcome of my struggles with the
difficulties Godel's incompleteness theorem makes for producing a
foundational system that could be judged as ultimate.
So in the end I am interest in V=L universes. We want a system to
generate theorems about that. Going to high universes gives us more proof
power to know about L, but that extra power also puts more complexity into
the universe and geenrates new difficult questions.
So I break the cycle. The "real" universe is L, but as a guide to what
is true in L, I can look out and see what higher universes tell me about L.
I think of them as a formal tool for generating an r.e. list of theorems
about L.
By Craig's theorem, any r.e. axiomatized theory can be equivalently
recursively axiomized (different axioms but same theorems). So I cna
consider that I have given a system telling about L even when I step
outside and then cut the answers back to L.
So though the language is first order language, I am giving an unusual
proof system for it. I am not literally adding to the extended ZFC
axiomatization above the axiom V=L. Instead I will define the final
theorems of my system to be those with L-relativization provable in an
underlying ZFC theory. In this way "V=L" gets into the the final system.
But it allows me to sneak power beyond L in the background, the
underlying theory generating those L theorems might use large cardinals
incomatible with L.
This is some more detail about what I wrote above, about not completely
abandoning non-L, or large cardinal strength beyond L.
This is a non-standard notion of proof system. It is my final resolution
of the struggles trying to reconcile Godel's theorem with system building.
So so far we have ZFC in the expanded language, and this indirect working
of "V=L" into the system.
So more axioms now, for te base system, about those new constants. We
axiomatize that U is an inaccessible L-rank, ie L_kappa for some
strongly inaccessible cardinal. This is inaccessiblity in the background
full universe, not just its L.
We axiomatize that for all alpha countle^L ordinals and beta
countable^L ordinals, with alpha < beta, that U^beta_alpha is an L
rank for an ordinal inaccessible in L. This is weaker than the
corresponding U axiom, because we axiomatized that U's rank was real
inaccessible, ie in the full background universe, but for this axiom we are
only claiming inaccessible in L.
(Note that in discussing the axioms we are using the language literally.
It is only the final reinterpretation step that automatically realtizes
back to L. The axioms and proofs stay in the base set theory language for
a while and only as a last step do we check which are the theorems produced
that realtized to L.)
We axiomatize that the u and U functions behind the terms have domain
as just mentioned: L-countable ordinals superscript beta subscript alpha
with alpha < beta.
We axiomatize with universal quantifiers that for suitable alpha1 <
alpha2 and beta U^beta_alpha1 member U^beta_alpha2 and
for suutable alpha1, alpha2, beta1, beta2 with beta1 < beta2
U^beta1_alpha1 member U^beta2_alpha2. Ie each beta makes an incrreasing
sequence as alpha increases, and the next beta sequence starts strictly
above the entire previous beta sequence. "Suitable" above means all
displayed terms are well-defined with the "alpha-beta" pair being in the U domain.
We axiomatize that every U^beta_alpha term as above (ie proper beta,
alpha to be in the dimain) is an elementary substructure of the full L of
the universe, elementary in the language of =, epsilon. This is a
schematum over every formula in the laguage. (We leave off the
U^beta_alpha's from the language since those may not be in the small
model).
This schematum is a schematum over choice of formula in expanding the
definition of elementary substructure. But the beta's and alpha's abpve
are expressed with full universal quantifiers, ie for each formula we have
an axiom saying for all suitable beta,alpha, actual universal quantifier
in the axiom.
Next axioms. We axiomatize as a schematum over formulas, with beta and
alpha universally quantified in the axiom, that for each L-countable
ordinal beta, the sequence <U> ^ <U^beta)alpha | alpha < beta>,
ie the seuquence with U followed by all the U^beta_alpha with fixed
beta and varying alpha, is a sequence of strong order indiscerables in
the full universe's L. Ie, this means for any formula with parameters in
L of rank < both starting members of two increading n-tuples from the
sequence, we have the indescernabilty axiom: the 2 formulas in those
respective tuples are equivalent.
We axiomatize that L satisfies separation and replacement for formulas
with the new symbols: u and U, both the constants and the function
symbols.
Now a suble point, for the next axioms. Above we axiomatized
L-inaccessiblilty and L-indiscernability for the U's, with full
universal quantifiers.
I want corresponding axioms for the full background universe. But I must
do these in a weaker form. Otherwise some of the intended strengthenings
of the base system would be inconsistent. For inaccessiblity, I axiomatize
a schematum, over all terms t1 and t2 in the language, terms with
parameters, and the full language with all the new symbols, saying that if
t1 denoted an L-countable ordinal and t2 denotes an L-countable ordinal,
and t1 < t2, then U^t2_t1 has rank strongly inaccessible in the
background universe.
Similarly, I axiomatize the indiscernability axiom, but not for
L-formulas, but for the full background universe, but instead of
quantifying over all suitable beta, alpha as in the L version above, I
just do each axiom in the schematum for a specific tuple of terms making
the "beta"'s and "alpha"'s for sequences of indiscernables.
I also axiomatize, in similar schematum fashion, that the U^beta_alpha's
have correponding full ranks (ie take the V rank in the background universe
with same height as U^beta_alpha's height) which are elementary
substructures in =,epsilon to the full background universe.
The previous axiom making the L levels elementary substuctures of L may
seem reundant after the last. But the L version quantified over all the
U^beta_alpha's and the full version is only a schematum so we retain the L
version too.
That covers U and U^beta_alpha.
Now u and u^beta_alpha, which I have not previously discussed. We
axiomatize using universal quantifiers that the u function has same
domain as the U function, ie L-countable ordinals both with alpha < beta.
We axiomatize that u and all suitable u^beta_alpha (using universal
quantifiers on alpha,beta) are countable L ranks.
And we axiomatize that for any formula in =,epsilon with parameters
exactly U^beta_alpha1 U^beta_alpha2 ... U^beta_alphan with these
all suitable (ie superscripts and subscripts in the domain of the U
function) such a formula holding in <U^beta_alphan+1> is equivalent
to having <u^beta_alpha_n+1> satisfying the same formula with each
U^beta_alphai replaced by the corresponding u^beta_alphai.
Ie: we have U and the various U^beta_alpha's sitting as inccessible
ranks in L and the universe. u and u^beta_alpha are a miniature
corresponding version, of small L-countable ranks that look like the
uncountable hierarchy sitting above regarding internal formulas.
This last axiomatization is done as a single axiom. We quantify over all
tuples of ordinals, of all arities (ie "n") in the quantification, and we
quantify over all formulas, since we are only talking about their truth in
set sized structures we can define that truth and so formalize all that in
one axiom instead of a schematum.
That's it, for the axiomatization.
The base system is the axiomatization just given, with the understanding
that the final list of the theorems generated will be those with L
relativization provable in the base axiomatization given above.
I started off writing that I was giving a family of related systems. So
we branch out into the family by adding more axioms to the above, axioms
about the underlying universe, and possibly get new theorems about its L,
hence new theorems about the final system.
We can also extend the language. For example, if we anted to add new
constant symbols we would typically axiomatize them to denote a member of
U. And we would probably make the real version of them in upper case in U,
and a lower case version in u, and extend the axiom reflecting the U's to
u's in the obvious way.
So even though L is in the foreground, we can add large cardinal strength
beyond L in the background, to the base axioms which don't assume outright
that V=L.
We can also get some strength from non-AC. If you have a strong ~AC
prinicple you would like to get into the background, in the framework above
you could axiomatize that there is an uncountable standard model of the
other principle. This will often be good enough to import things into L.
You can work in that model to get things about its L. Having things hold in
an uncounble L rank is as good for many purposes as having it in all of L.
This is actually a theorem if you are already beyond 0#.
Sometimes we want to treat the universe of set theory as the enveloping
context. Formalize this in the theiry above by just forgetting all the
extra machinery and working in the ZFC or ZFC + V=L part.
Sometimes we want to talk as if the set theoretic universe could itself
be a bounded object, having global properties to discuss. For this use U.
Sometimes we want to consider the universe as one of a population of many
possible universes. For this use u, and consider all the standard
countable ZF models to be the entire population.
If you just want to be working in ZFC or even ZFC + V=L, just use those
and interpret them straightforwardly in the axiomatization above. (Any
consequence of V=L is autimatically generated by the final theorems list).
If you want to be in GB or Morse-Kelley, interpret sets as members of U
and classes as subsets (in the original sense) of U.
If you want to be in ZFC + V ~= L or ZF + ~AC, interpret your
universe as one of the countable structures along with the u 's.
-- David Libert ah170@FreeNet.Carleton.CA
- Next message: Tim Smith: "Re: Trisecting an Angle"
- Previous message: Denis Feldmann: "Re: DWB: Trisecting an Angle"
- Next in thread: Ross A. Finlayson: "Re: extending ZFC"
- Reply: Ross A. Finlayson: "Re: extending ZFC"
- Messages sorted by: [ date ] [ thread ]
Relevant Pages
|