Skolemization
tc...@lsa.umich.edu
them in Cohen's book, though maybe that's just because Cohen's book doesn't
have an index and I missed it while flipping through (it probably didn't
help that I didn't really know what I was looking for other than the words
"Skolem function" and that I was hoping they would be underlined). They
might be in Chang and Keisler's book, but in the library I came across
_Model_Theory_ by Wilfrid Hodges first, and found his account very readable.
I think I now understand David Libert's recent article on using Skolem
functions to construct a nonstandard model of PA. The way I see it, he
is basically following Cohen's remark that we can get a nonstandard model
by running through the proof of the Loewenheim-Skolem theorem, since after
all that's how we figured out that there exist countable nonstandard models
in the first place. By carefully examining just where the proof "goes non-
recursive" and using the minimum amount of non-recursivity possible,
we get a nonstandard model that is as close to recursive as possible.
After this I went back to an old article by Herb Enderton that I didn't
understand at the time, again because I didn't know what Skolem functions
were.
http://www.google.com/groups?selm=7majf2%24ols%241%40carroll.library.ucla.edu
He makes one remark that I still don't quite understand, which is that one
of the proofs of the Loewenheim-Skolem theorem doesn't require the axiom of
choice. Part of my problem is that I'm not sure which proof he means (it
looks to me that he says one thing in the first part of the article and
then reverses it in the second part). In any case, is it true that if we
formalize logic inside ZF, then we can prove in ZF that (for example)
first-order logic is complete? If so, I am surprised, because I was always
under the impression that AC, or at least some weak form of it, was needed.
--
Tim Chow tchow-at-alum-dot-mit-dot-edu
The range of our projectiles---even ... the artillery---however great, will
never exceed four of those miles of which as many thousand separate us from
the center of the earth. ---Galileo, Dialogues Concerning Two New Sciences
Chris Menzel
<tc...@lsa.umich.edu> said:
> ...
> After this I went back to an old article by Herb Enderton that I didn't
> understand at the time, again because I didn't know what Skolem functions
> were.
>
> http://www.google.com/groups?selm=7majf2%24ols%241%40carroll.library.ucla.edu
>
> He makes one remark that I still don't quite understand, which is that
> one of the proofs of the Loewenheim-Skolem theorem doesn't require the
> axiom of choice.
I think what he is referring to is the fact that there are weaker and
stronger version of the LS theorem. The weaker version just guarantees
models of every cardinality for a given theory T with infinite models.
The stronger guarantees (very roughly) that from a *given* model M of T
one can construct substructures and superstructures of M of all infinite
cardinalities that are models of T. Enderton only says that choice
*may* be required for the stronger theorem -- I suspect (I'm sitting at
a coffee shop with no text handy) that choice is needed to guarantee
that the substructures and superstructures in the stronger form of the
theorem are *elementary* with respect to the original structure M.
> In any case, is it true that if we formalize logic inside ZF, then we
> can prove in ZF that (for example) first-order logic is complete? If
> so, I am surprised, because I was always under the impression that AC,
> or at least some weak form of it, was needed. -- Tim Chow
Not exactly sure myself, but perhaps it's to prove completeness
generally for languages of arbitrary infinite cardinality, in particular
to well-order the formulas for the Lindenbaum construction. ??
Chris Menzel
H. Enderton
> In any case, is it true that if we formalize logic inside ZF, then we
>can prove in ZF that (for example) first-order logic is complete? If
>so, I am surprised, because I was always under the impression that AC,
>or at least some weak form of it, was needed.
If the set of symbols can be well ordered, then I think the Henkin
completeness proof goes through without requiring choice. But for a
completely arbitrary set of symbols, probably one needs at least the
prime ideal theorem.
In fact in this case, is completeness equivalent to the prime ideal
theorem? Perhaps someone has a reference to someplace where this is
nailed down.
--Herb Enderton
tc...@lsa.umich.edu
H. Enderton <h...@sonia.math.ucla.edu> wrote:
>If the set of symbols can be well ordered, then I think the Henkin
>completeness proof goes through without requiring choice. But for a
>completely arbitrary set of symbols, probably one needs at least the
>prime ideal theorem.
Just to be sure what you're saying here: In particular, for a countable
set of symbols, one doesn't need even countable choice?
David Libert
> In article <ath806$5ms$1...@galois.mit.edu>, <tc...@lsa.umich.edu> wrote:
> > In any case, is it true that if we formalize logic inside ZF, then we
> >can prove in ZF that (for example) first-order logic is complete? If
> >so, I am surprised, because I was always under the impression that AC,
> >or at least some weak form of it, was needed.
>
> If the set of symbols can be well ordered, then I think the Henkin
> completeness proof goes through without requiring choice. But for a
> completely arbitrary set of symbols, probably one needs at least the
> prime ideal theorem.
Cohen mentions this about the completeness theorem for
well-orderable symbols in ST&tCH. Namely, starting the proof of the
completeness theorem, he writes the proof uses AC, unless the set of
statements is well-ordered (p 13).
Anyway, do a usual Henkin constants proof, as in Cohen. My 0'
construction recently is like this too, phrased though with Skolem
functions.
> In fact in this case, is completeness equivalent to the prime ideal
> theorem? Perhaps someone has a reference to someplace where this is
> nailed down.
>
> --Herb Enderton
Yes, I think that's right, completeness equivalent to prime ideal
theorem.
Closely related to this, in terms of existing references, in the
Jech's Axiom of Choice paper in the Handbook of Mathematical
Logic, Jech writes that the compactness theorem is equivalent to the
Boolean Prime Ideal Theorem.
I will write my own comments related to various points about this,
some as found in Jech's paper just mentioned.
Tim asked in followup to Herb's just quoted article whether Herb's
comments give the completeness theorem for theories in a countable
language, as a ZF theorem (no amount of choice or anything beyond ZF
needed). I think that is true, by Herb's comments, ZF alone gives
this fragment of completeness.
Someone in one of the recent threads noted that reverse math
classified completeness over ACA_0 as being weak Konig's Lemma. So
that level would also be outright in ZF, part of what was above.
Jech's paper has an earlier section about the Boolean Prime Ideal
theorem, BPI. An ideal is a non-empty subset of a Boolen algebra,
closed downward by the induced Boolean partial ordering, and closed
under join. Equivalently, it is the preimage of {0} in some Boolean
homomorphism.
A filter in a Boolean algebra is the dual, closed upward and under
meets, the preimage of {1}. Ideals and filters pair off: the
elementwise compliments from an ideal are the associated filter and
similarly the other direction.
A prime ideal is an ideal including at least one of each element or
its compliment. The corresponding notion for filters is
ultrafilters. You can pass back and forth by the association just
mentioned between these, and I will tend below to use whichever comes
up at the moment.
BPI says that any Boolean algebra has a prime ideal. This implies
its own self stengthening: any ideal I in any Boolean alebra B can
be extended to a prime ideal P. Namely take B/I the quotient
Boolean alebra collapsing I to 0, with the associated collapsing map
: B -> B/I, then in B/I get a prime ideal from BPI, and take the
preimage of that in B via that collapsing map, to get the desired P
prime ideal in B extending I.
So Jech wrote that the semantic compactness theorem for arbitrary
first order languages is equivalent over ZF to BPI.
I claim each of these is ZF provably equivalent to the completeness
theorem for arbitrary first order languages.
I will prove that equivalence and the one from Jech in a triangle of
3 steps, BPI -> completeness -> compactness -> BPI.
Toward proving BPI -> completeness, given T a syntactically
consistent first order theory in language L, first consider Henkinizing
T, namely making an extended version of T in an expanded language,
adding new Henkin constants and associated axioms.
Namely the Henkin constants are added in omega many stages, each
Henkin constant is to name a witness for a existential sentence if it
exists, otherwise there is no requirement on the constant. So this can
be expressed by an axiom: if c is the Henkin constant for phi(x)
the corresponding Henkin axiom is (exist x) [phi(x)] -> phi(c).
We have to add Henkin constants in omega many stages, because new
Henkin constants create new phi's that can mention the constants as
side parameters and hence give rise to a next generation of Henkin
constants.
Each formula is finite and only mentions finitely many Henkin constant
parameters, so this stabilizes at stage omega.
So the Henkinized version of starting theory T is the expanded
language with those new Henkin constants and extended axioms over
those of T, adding the new Henkin axioms as above.
The claim is that T syntactically consistent -> the Henkinized
version syntacitally consistent, this just in ZF. In ZF we already
have the syntactic version of compactness, since every proof is
finite. So this amounts to showing finitely many new Henkin axioms
can't introduce a new proof of contradiction. And this is like
Shoenfield's theorem on constants, that new constants asserting what
is provable about something from existentials can't make a new
contradiction. A syntactic proof. And the Henkin axioms in that
sense only assert what is trivial in logic.
So the Henkin theory is syntactically consistent. A complete Henkin
theory provides a canonical Henkin constants model, since the Henkin
axioms provide Henkin constant witnesses to all existentials.
So it amounts to finding a complete extension of the Henkinized
version of T. Take the Lindenbaum algebra of this theory, ie the
sentences of it language, modded out by provable equivalence, provable
in the Henkinized T, this is a Boolean algebra. Finding a complete
theory extending the Henkinzed T amounts to finding an ultrafilter in
this Boolean algebra. BPI!! What more need be said? I think just:
QED.
Next, completeness to semantic compactness. The soundness theorem
is ZF provable, and is one direction of the equivalence of syntactic
to semantic consistency. Completeness being presently assumed is the
other direction. So with both directions available semantic
compactness is equivalent to syntactic compactness. But syntactic
compactness is ZF provable, as was used above, ie proofs are finite.
Next, compactness (ie semantic compactness) to BPI. So suppose B is
a Boolean algebra. I will phrase BPI in terms of ultrafilters where I
know more related terminology. So we seek to find U an ultrafilter in
B.
Form a first order theory, in the language of Boolean algebra, with
unary predicate symbol F, and with individual constant symbols one
corresponding to each element of B. (In fact we could take the B
element to be the constant symbols). Make axioms saying this is a
Boolean algebra, express that F is a filter in axioms ie closure
properties etc. Also put in a schematum of axioms expressing all true
Boolean equalities from B as corresponding equations in the
corresponding constant symbols. Also, make a schematum of axioms over
the constant symbols which together say that filter F is actually ultra:
for each constant symbol b put in axiom F(b) or F(-b).
This theory is finitely satisfiable. Namely, given finitely many
"ultra" axioms, you can satisfy that fragment over all the rest by
taking F to be a principal filter generated by some non-0 finite meets
of b or -b 's from the axioms. All those meets can't be 0, else by
finite distributivity 1 would be a finite join of 0's.
So that theory is finitely satisfiable. So by the assumed
compactness it is satisfiable.
A model of this full theory is a Boolean algbra, into which B embeds
by taking each B element to the denotation of its constant symbol. We
don't know that F in the model is really ultra, but at least it is
ultra w.r.t. the image of that embedding, by the schematum of ultra
axioms included.
So pull back the model's F to B from the embedding, obtaining the
desired U on B.
That completes BPI <-> completeness <-> semantic compactness.
Now some more related results. I am making up my own terminology,
so if there is some literature about this I don't know it may disagree
with my terminilogy.
Let LI+ be the statement that any partial order on any set can be
extended to a linear order on that same set. Let LI be the statement
that any set can be linearly ordered.
For the next section I will be discussing implications. When I
assert implications, it means I am asserting these are ZF provable.
LI+ -> LI, by extending the empty partial ordering.
BPI -> LI+. Use the compactness equivalent of BPI. Namely given a
partial order on index set I, make a theory with individual constants
for I elements, the axioms of linear ordering, and a schematum of
individual axioms asserting true < 's from the partial order.
This is finitely satisfiable, because given finitely many such
axioms the fragment theory is asserting its universe is a linear order
with finitely many constants in consistent positive relations to each
other, and such fragments are consistent, ie any finite partial order
can be extended to a linear order, as a ZF theorem, (induction on
number of element in the partial order).
So by compactness the whole theory has a model. Like last proof
with the Boolean algebras, this model may have bigger underlying set
than our starting I, but we can still embed the original partial order
order preservingly into the model, and then pull back to induce a
linear order on I.
We can also get to BPI, ie getting ultrafilters basically, from AC,
a Zorn's lemma argument.
So over ZF we have the chain of implications AC -> BPI -> LI+ -> 0=0.
None of these reverses as a ZF theorem. I included the 0=0 just as
a way with the last observation to express that ZF doesn't prove LI+,
or indeed even LI.
Jech cites Halpern and Levy as showing BPI -/-> AC. For
Li+ -/-> BPI I was once told of a Fraenkel Mostowski model with
atoms corresponding to the rationals, the group being order preserving
bijections, and finite supports. Seems to me now that does that last.
Regarding ~LI+ in ZF. Even better, I can get ~LI in ZF.
This is along the lines of some of my earlier posts about things
from Cohen's book. This is various constructions he gave of ~AC ZF
models.
Regarding the underlying technique in general:
[1] David Libert sci.logic July 6 '00
"Cohen symmetric choiceless ZF models"
Message-ID: <8k1pfm$3a7$1...@freenet9.carleton.ca>
Cohen's first ~AC model constructed an amorphous set A. A is
defined to be amorphous if A is infinite (ie does not have cardinality
being a member of omega) and every subset C of A is either finite or
cofinite in A, that last property meaning A-C is finite.
I had some related discussion of that, proving that an amorphous set
can't be linearly ordered among other things:
[2] David Libert sci.logic June 27 '00
"Re: cardinality of the power set of the integers"
Message-ID: <8jadvc$me4$1...@freenet9.carleton.ca>
Cohen also had a ZF model with a countable set of two element sets,
having no choice function, ie there is no choice function making
countably many choices of one member from those respective doubletons.
If the union of the doubletons could be linearly ordered, that would
give a choice function, ie pick the smallest from each doubleton.
Any infinite subset of an amorphous set is amorphous. So the first
example has no linear ordering on any infinite subset of itself.
The second example has this stronger property too. Namely, similar
proofs to Cohen's show any choice function on a subset of the
doubletons is on only finitely many doubletons, ie choice
sub-functions are all finite. A linear ordering on an infinite subset
of the last example would induce a choice function on infinitely many
doubletons.
So that wraps up the comments on AC -> BPI -> LI+ -> 0=0 not
reversing.
The question originally was completeness in just ZF, so I am going
to continue with some strange examples against usual theorems, examples
in ZF.
There is a gap though in what I have so far, which I will be writing
about below. Namely, the discussion above showed regarding
completeness and compactness anyway, the familar results are available
with BPI. I am going to be giving strange examples with ~LI. A
sharper result would be to give examples in ZF + LI+ + ~BPI.
But so far what I see are these ~LI related examples.
So suppose I is a set which cannot be linearly ordered. (For this
first example that's all I need to assume, a later example will use
the stronger property that no infinite subset can be linearly
ordered.)
Form a theory: the axioms of linear ordering, and a constant symbol
for each element of I, and for distinct I elements an axiom saying the
corresponding two constant are ~=.
If there were a model of this theory, we could map I into it by
carrying each I element to the denotation of its constant, and then
pull back the model's linear ordering onto I, obtaining a linear
ordering on I, contra choice of I.
So this theory has no models.
But any finite fragment of this theory is just saying it is a linear
order with finitely many distinct constants. Each of these is
consistent. And ZF proves syntactic compactness.
So this theory is syntactically consistent.
So we just found a consistent first order theory with no models!
More fun. Let <J, < > be a linear order < on some index set J.
Let I be that same set above, with no linear orders.
Consider J union I. This has cardinality (assuming we have made a
reasonable choiceless version of cardinals) > #J, since J is a
subset of J union I.
If <J, < > were elementarily equivalent to any structure on
J union I, a set of cardinality > #J, then that structure would have
a linear ordering on J union I, and so by restriction induce a linear
ordering on I, contra choice of I.
We just found a counterexample to the weak upward Lowenhiem Skolem
theorem! (Ie weak: in terms of elementary equivalence rather than
elementary extension.)
Now I need to jazz up I for the next example. Take the stronger
property as above, no infinite subset of I can be linearly ordered.
Let < be a linearly ordering on J, assuming now also that < is
without endpoints. Consider the structure < J union I, < > .
Ie this structure has < a binary relation with field a part (namely
J) of the universe J union I.
The theory of this structure says that < on its field (field of <
being definable in the theory) is a linear ordering without
endpoints.
This structure has universe J union I, which has cardinality > #I.
Suppose there was an elementarily equivalent substructure of this
< J union I, < > of cardinality #I, a cardinal < the cardinality
of the starting structure.
Such a substructure, while not having universe I itself as it sits
in J union I, would still have universe of cardinality #I, so
bijective with I, and so by this bijection we could pull back to make
a new structure on I.
The theory of the original < J union I, < > structure said that <
is a linear ordering without endpoints on its field, so by elementary
equivalence the assumed substructure would also say that, so the
isomorphic structure we induced on I would also say that.
So the new relation on I would be a linear order without endpoints
on its field (nonempty by elementarity etc since J was), so we have
induced a infinite (no end points) linear ordering on a subset of I,
contra the stronger property of I.
So <J union I, < > has no elementarily equivalent substructures
of cardinality #I < #(J union I).
We have a counterexample to the weak downward Lowenhiem Skolem
theorem!
Anyway, above I got the explicit counterexample to completeness, but
what is the big deal, because earlier I proved completeness is
equivalent to BPI, and these ~LI models are certainly not BPI models
by the previous implication.
Anyway, weak upward and downward Lowenhiem Skolem only need
completeness, and that is equivalent to BPI.
For strong upward and downward Lowenhiem Skolem, with elementary
equivalence, the usual method is Skolem functions.
How to get Skolem functions? The obvious way is AC, to pick from
witnesses. So strong LS seems more or less AC, above the BPI level of
completeness and weak LS, as from recent posts.
In models below BPI above, I was contradicting those lower BPI
theorems.
Here are some more examples, related to the strong LS levels, and
Skolemization.
Above in proving BPI -> completeness, I argued that ZF proves
Henkinization preserves syntactic consistency.
What about Skolemization? First off, in ZFC, any structure can be
Skolemized, by getting Skolem functions on the original structure with
AC. So in meta-theory ZFC, Skolemization applied to a theory
preserves consistency, since it works that way on each model one at a
time.
Now consider what can happen in ZF + ~AC. Take Cohen's countably
many choiceless doubletons. Form a structure, consisting of all those
doubletons and also all their members, and the binary membership
relation holding between doubletons and their members.
Make a language, with a constant symbol for each doubleton, and a
constant symbol for each member of any doubleton. Also include a
binary membership relation in the language.
Make a theory in that language: for each doubleton put in an axiom
about that constant symbol, saying that the constants for its actual
members lie in the language's membership relation to it, and a
quantified formula saying anything in the universe in the membership
of the doubleton constant is one of those constant.
Ie: basically saying in the theory that the constant for a doubleton
has membership corresponding to the original doubleton.
So that is the base theory.
Now consider the Skolemization of that theory: ie add Skolem
function symbols and Skolem axioms.
Consider the formula in free variable x: (exists y) y member x .
Consider the associated Skolem function for that existential.
Suppose the Skolemized theory had a model.
Then we can map Cohen's original countable set of doubletons into
that model, by carrying each doubleton to the denotation of itself as
constant symbol.
Since this is a model of the theory, the membership relations in the
model of those denotations of doubletons are exactly the denotations
of the members of the original doubletons, by the axioms we put in.
The model's denotation of the Skolem function symbol for the
existential formula would therefore give the denotation of a member of
the original doubleton.
Taking the constant symbol corresponding in the model to such output
of the Skolem function, we get back a member of the original
doubleton.
So this would define a choice function on Cohen's original
doubletons, contrary to Cohen's construction.
So the Skolemization of the theory above has no model.
But the original base theory had a model: just Cohen's original
doubletons and their members, ie letting everything denote iteself.
So we have a base theory which has a model, with its Skolemization
having no model.
My previous discussion of Henkinizing had Henkinization preserves
syntactic consistency.
I have just above gotten Skolemization to lose semantic
consistency. But in these choiceless models, syntactic and semantic
consistency can diverge, as we saw in an earlier example.
What about syntactic consistency? We are in metatheory ZF, we
assume a base theory T is syntactically consistent. We want to know
if T's Skolemization must be syntacitically consistent.
Well, suppose the Skolemization were not syntactically consistent.
Then some finite fragment of the base theory and the Skolem axioms
over it would be syntactically inconsistent, ie syntactic compactness
is available even in ZF.
Possibly T was over a language which included symbols that were not
even in Godel's L, ie potentially any set can be used as a symbol.
But all the finitely many symbols, original base symbol or Skolem
function symbol, from that finite fragment just found, can be replaced
by members of Godel's L.
Then the the original fragment of T, ie the finite axioms, can be
copied over onto those L symbols. The resulting axioms are just
finite, built from L elements, so they are in L.
Since the original base theory was syntactically consistent, the
part of the L copy corresponding to the base theory (as opposed to the
Skolemization) is recognized by our working universe as being
syntactically consistent (ie any inconsistency proof could be copied
back to an inconsistency proof on the original).
But syntactic consistency is an absolute property, the syntactic
consistency of formulas in L is the same as viewed from L as from V,
ie L and V agree on the same finite constructions, syntactic
constructions, on the base.
So Godel's L thinks that its copy of the finite fragment of the base
theory is syntactically consistent.
But Godel's L satisfies AC, so we are back to the familar world,
with the completeness theorem, and syntacitic consistency and
semantic consistency coincide.
So the L copy of the base part of the finite fragment is
semantically consistent in L, so there is a model.
But L satisfies AC, so it can Skolemize models. So L thinks that
the Skolemized extension, ie its copy of the entire finite fragment,
is semantically consistent.
Our outer working universe V (our ZF universe), can see that model
of the fragment in L, and can see that L copy is syntactically
isomorphic to the finite fragment of the language.
So our V sees that fragment is semantically consistent. And hence
certainly syntaically consistent.
Contrary to the supposed syntactic inconsistency of the fragment.
This contradiction from assuming in ZF that the Skolemization of T
was syntactically inconsistent.
So earlier I argued that Henkinization preserves syntactic
consistency.
I have just argued that Skolemization preserves syntatic
consistency, even working in meta-theory ZF.
But we have seen that Skolemization can newly lose semantic
consistency.
The whole point of Skolemization was to be a tool to build models,
and we have seen that Skolemization can itself make models impossible,
in a choiceless context.
Anyway, the corresponding was true for Henkinization. Having
Henkinization, as syntactically consistent, we still need some power
to get to a model, ie we still needed BPI as a later step to get to a
model.
All this is really saying is that the usual arguments that seem to
be using something beyond ZF really are: this is showing there is no
reworking of them to get by with less.
I will close with some further comments of Jech, general interest
points about BPI, and ultrafilters.
As I understand it, (this from general background, Jech doesn't
mention this), over ZF AC is equivalent to the Tychonoff product
theorem for general topological spaces.
Jech mentions that BPI is equivalent to the Tychonoff product
theorem for compact Hausdorff spaces.
Also, Jech mentions that Hahn Banach and Stone-Cech compactification
are consequences of BPI.
Finally, Jech mentions that Feferman got a ZF model in which there
is no non-principal ultrafilter on omega. Blass extended this to a
related model, with no non-principal ultrafilters at all, ie on any
set.
--
David Libert ah...@FreeNet.Carleton.CA
tc...@lsa.umich.edu
In article <m3el8h1...@localhost.localdomain>,
David Libert <ah...@freenet.carleton.ca> wrote:
> Tim asked in followup to Herb's just quoted article whether Herb's
>comments give the completeness theorem for theories in a countable
>language, as a ZF theorem (no amount of choice or anything beyond ZF
>needed). I think that is true, by Herb's comments, ZF alone gives
>this fragment of completeness.
Elsewhere, George Greene asked how one can possibly obtain countable
nonstandard models M of PA if + and * in M are necessarily non-recursive.
I suggested that perhaps the problem was the use of the axiom of choice
in the proof of the compactness theorem. In light of what David Libert
and Herb Enderton have just said, this does not seem to be the correct
diagnosis. Perhaps a more accurate diagnosis is that in ZF we can say
things like "Let S be the set of all n such that Turing machine T_n halts,"
even though the halting problem is undecidable?
Andrew Boucher
tc...@lsa.umich.edu wrote:
> In any case, is it true that if we
>formalize logic inside ZF, then we can prove in ZF that (for example)
>first-order logic is complete? If so, I am surprised, because I was always
>under the impression that AC, or at least some weak form of it, was needed.
>
>
You might want to consult Simpson's "Subsystems of Second-Order
Arithmetic." RCA0 - a very weak theory indeed - proves a weak version
of the completeness theorem (Theorem II.8.4, p. 92). Weak Konig's Lemma
suffices to prove the full version (Theorem IV.3.3, p. 140).
Robert E. Beaudoin
I believe Jech (in his text _Set Theory_) states that (1) completeness
(of some suitable deductive system, of course), (2) compactness, and
(3) the prime ideal theorem are equivalent (without AC). But he
doesn't give details; some of the proofs are just not discussed and
some are left as exercises.
The equivalence of (1), (2), and (3) in ZF is not hard to establish for
propositional logic. That completeness (of, say, a standard Hilbert-
style deductive system) implies compactness is trivial as any proof
involves only finitely many formulae. To show compactness implies
the PIT, or dually that every proper filter on a Boolean algebra
extends to an ultrafilter, begin by observing that on a finite (or
even a countable) algebra B the standard proof of existence of
ultrafilters goes through without AC, since it involves an
induction of length |B|. So if B is any Boolean algebra and F any
proper filter on B, let L be a propositional language with one
propositional variable P_a for each element a of B, and let T be
the following set of axioms in L: -P_{}, P_a -> P_b for all a <= b
in B, (P_a & P_b) -> P_(ab) for a, b in B, P_a v P_(-a) for a in B,
and P_a for every a in F. If T' is a finite subset of T, then the
subalgebra A of B generated by all a such that P_a occurs in some
proposition in T' is finite. Hence F intersect A extends to an
ultrafilter W on A. Now the truth assignment making P_a true if
a is in W and false if not satisfies T'. By compactness there is
an assignment f satisfying T, and one can define an ultrafilter U
on B extending F by putting a in U if and only if f(P_a) = true.
Now suppose T is a propositional theory consistent with respect to
some fixed deductive system S. From the PIT and a few assumed
properties of S one can produce an assignment satisfying T:
Let B be the Lindenbaum algebra of T w.r.t. S. (I'm sure Herb
Enderton knows what that is, but for anyone who doesn't, B is
formed by modding out the set of sentences of the language of T
by the equivalence relation ~ defined by: A ~ B if and only if
the sentence A <-> B is provable [in S] from T. One can define
complementation and disjunction on B by -[A] = [-A] and
[A] v [B] = [A v B] and this makes B a Boolean algebra. Well, it
does as long as S is strong enough to prove a selection of
tautologies, e.g. DeMorgan's laws, which correspond to the axioms
defining Boolean algebras.) Fix any ultrafilter U on B. Define a
truth assignment f by setting f(P) = true if [P] belongs to U, and
f(P) = false if [P] does not belong to U. For any proposition A
in the language of T (by induction on the structure of A) it
then follows that f(A) = true if and only if [A] belongs to U.
But for each A in T, [A] is the maximum element of B and so
belongs to U.
For first-order logic the details are hairier. One can give
an argument like that of the last paragraph (but the construction
from an ultrafilter on the Lindenbaum algebra of a model is more
complex in any language with function and constant symbols), but
first one must show that any consistent T can be extended to a
consistent T' containing Henkin formulae (Ex)A(x) -> A(c) for any
A in the language of T' (where c is a sufficiently "new" constant
symbol). With AC one can interleave the addition of Henkin
formulae one at a time with addition of formulae to make T'
complete, and avoid the need to choose an ultrafilter on the
Lindenbaum algebra. Without it one can (with sufficient care)
construct T' by an induction of length omega, in which one adds
many Henkin formulae at each step. I know that's sketchy, but
this post is already more than long enough, no?
Hope this was of some interest.
Bob Beaudoin
Andrew Boucher
Robert E. Beaudoin wrote:
> H. Enderton wrote:
>
>> In article <ath806$5ms$1...@galois.mit.edu>, <tc...@lsa.umich.edu> wrote:
>>
>>> In any case, is it true that if we formalize logic inside ZF, then we
>>> can prove in ZF that (for example) first-order logic is complete? If
>>> so, I am surprised, because I was always under the impression that AC,
>>> or at least some weak form of it, was needed.
>>>
>>
>> If the set of symbols can be well ordered, then I think the Henkin
>> completeness proof goes through without requiring choice. But for a
>> completely arbitrary set of symbols, probably one needs at least the
>> prime ideal theorem.
>>
>> In fact in this case, is completeness equivalent to the prime ideal
>> theorem? Perhaps someone has a reference to someplace where this is
>> nailed down.
>>
>> --Herb Enderton
>>
>>
Also Simpson's "Subsystems of Second Order Arithmetic", p. 139-147,
which shows in the countable case equivalence to Weak Koenig's Lemma.
H. Enderton
>>If the set of symbols can be well ordered, then I think the Henkin
>>completeness proof goes through without requiring choice. But for a
>>completely arbitrary set of symbols, probably one needs at least the
>>prime ideal theorem.
And then Tim Chow <tc...@lsa.umich.edu> wrote:
>Just to be sure what you're saying here: In particular, for a countable
>set of symbols, one doesn't need even countable choice?
Right. For a countable language, the Henkin completeness proof does
not use any choice.
In connection with the earlier thread on Tennenbaum's theorem: The
fact that no choice is used does not at all say that the construction
is effective, or that you will get a countable non-standard model
with decidable properties. The construction is recursive in 0',
but that's about as far as it can be pushed down.
--Herb Enderton
George Greene
: Elsewhere, George Greene asked how one can possibly obtain countable
: nonstandard models M of PA if + and * in M are necessarily non-recursive.
"obtain" is the critical verb here. That is not a technical term,
nor is it the verb I used. The needed verbs really do have technical
definitions, but nobody has coined any verbs to abbreviate the
concepts. The difference here is between referring to something
as opposed to "specifying" it, as opposed to writing out all its parts.
: I suggested that perhaps the problem was the use of the axiom of choice
: in the proof of the compactness theorem. In light of what David Libert
: and Herb Enderton have just said, this does not seem to be the correct
: diagnosis. Perhaps a more accurate diagnosis is that in ZF we can say
: things like "Let S be the set of all n such that Turing machine T_n halts,"
: even though the halting problem is undecidable?
More to the point, in PA, you can say "~Con(PA)".
Even if the "proof" of the contradiction from PA (in that
model of PA) is not computable/recursive/finitary whatever.
--
---
"It's difficult ... you need to be united to have any
strength, but internal issues have to be addressed."
--- E. Ray Lewis, on liberalism in America
tc...@lsa.umich.edu
Andrew Boucher <Helene....@wanadoo.fr> wrote:
>Also Simpson's "Subsystems of Second Order Arithmetic", p. 139-147,
>which shows in the countable case equivalence to Weak Koenig's Lemma.
Good reference! I'm wondering if this can resurrect my idea of blaming
the non-recursiveness of countable non-standard models of PA on the axiom
of choice. Namely, RCA_0 seems to be designed so that things provable
in it are "recursive" in some sense. The completeness theorem can't be
proved in RCA_0; one has to add the weak Koenig lemma, which is a sort
of axiom-of-choice-ish assumption.