New APPS

Art, Politics, Philosophy, Science. Mostly Philosophy.

about

(Possibly Boneheaded) Question about Axiom of Choice, Soundness/Completeness, and Pi 2 Formulas

January 23, 2014

I'm not a logician. Nor do I play one on T.V. So please be patient if I'm messing up something basic in what follows. An explanation of what I'm messing up and/or some relevant citations would be pretty helpful too.

Gregory Moore's masterful Zermelo's Axiom of Choice: Its Origins, Development, and Influence contains the following passage:

Vestiges of the first state – choosing an unspecified element from a single set – can be found in Euclid's Elements, if not earlier. Such choices formed the basis of the ancient method of proving a generalization by considering an arbitrary but definite object, and then executing the argument for that object. This first stage also included the arbitrary choice of an element form each of finitely many sets. It is important to understand that the Axiom was not needed for an arbitrary choice from a single set, even if the set contained infinitely many elements. For in a formal system a single arbitrary choice can be eliminated through the use of universal generalization or similar rule of inference. By induction on the natural numbers, such a procedure can be extended to any finite family of sets.

I don't get this at all.

It seems to me that there are two relevant questions about choice vis a vis systems of formal logic: (1) is choice required to be used in constructing countermodels (which via soundness show that there will not be a proof in the system), and (2) is choice required in showing all models will have a certain property (for expressively limited frameworks like first-order logic some such properties, via completeness, will show that there is a proof in the system). This kind of reasoning leads to all sorts of question of whether there are any interesting deductive systems which are (or fail to be) sound or complete with respect to some semantics only on the assumption of choice, as well as questions about logics such as intuitionism that are supposed to be more constructive than classical logic. I'm sure there must be lots of work on this, unless Moore's brief discussion settles the issue in some clear way that's eluding me.

As far as soundness*- I do recall strengthened versions of the downward Löwenheim–Skolem theorem, where not only is the cardinality of the model denumerable, but that the domain is the natural numbers and all of the predicates defined at a certain cutoff in the arithmetic hierarchy. Might results in this neighborhood show that using ZF without choice is strong (i.e. so the proof theory is still sound) enough to be used in countermodel construction in normal first-order semantics? Or, in terms of Moore's discussion, might this also show in some sense that the use of eigenvariables in standard classical logic is free from implicit use of the axiom of choice?

This latter issue is more closely related to the completeness worry. Consider a meta-theoretic demonstration that some existentially quantified sentence is logically true. If we don't avail ourselves of completeness results, this requires basically showing that every single model is such that at least one object in that model renders the formula (you get when a name for that object replaces the bound variable) true.

Clearly, if the axiom of choice is true, this is a licit procedure. The choice function will take each of an infinite number of models to the object assigned in each model to the variable made free when the existential quantifier stripped off. But it raises the question of whether some logics are such that the converse holds, that this is only in general a licit procedure if the axiom of choice is true. This is much closer to Moore's issue, as the treatment of the free variable in the meta language mirrors the use of eigenvariables in natural deduction proofs of the sentence.

If there's anything to this, then one would expect expressibility issues to loom large. For example ZF being fine for the semantics of expressively weaker logics, but ZFC needed for expressively stronger logics.

Likewise, there are interesting issues of constructivity and choice. Intuitionist logic has the existential property and classical logic does not. That is, if an existentially quantified statement is provable in intuitionist logic, then the formula with the quantifier removed and the resulting free variable replaced by a name is also provable. (Along with the similar disjunction property), this a concrete way in which intuitionist logic is more constructable than classical logic. Intuitively, this connects to the choicyness (even for first order logic) of meta-linguistically determining that an existentially quantified statement is logically true.

Moore's book is fantastic, so I suspect I'm missing something. But as I try to make sense of Moore with my limited set theory abilities, it would be cool if anyone wants to set me straight and/or direct me to some literature on these very issues.

[Notes*

I don't like this way of talking. Why not say that the issue is whether the semantics are complete with respect to the proof theory? Seriously, why doesn't Goedel entail that second order semantics are unsound rather than second order proof theory incomplete? Full second order entailment contains so much mathematics (e.g. if the continuum hypothesis is true, then its second order formulation is true in every second order model) why not take a natural deduction formulation of the proof theory to get at its logical core and relegate the extra stuff to mathematics? I should probably ask for an explanation of this in a stand alone post.

Kreisel worried about related issues so much that he had a hard time seeing what completeness proofs are for in the first place. He thought there only justification was that they entailed that truth via the semantics was recursively (/effectively, at least via Church's Thesis, but maybe also without; I don't know) enumerable.

It would have been great to talk with Kreisel about modal logic, because it seems clear that completeness proofs there do much more, so much so that it's bizarre that we typically teach meta-theory of first-order logic before teaching modal logic. Often at the end of a well taught normal meta-theory class, over half the class still has no idea why we've proved all this stuff. At the end of a well taught modal logic class, this simply doesn't happen. And those very same students will get why one studies meta-theory of regular first order logic.]

Posted in Jon Cogburn, Logic

11 responses to “(Possibly Boneheaded) Question about Axiom of Choice, Soundness/Completeness, and Pi 2 Formulas”

Alex Clark

January 23, 2014

Here is a proposition “If S is a set with two elements each of which is a non empty set, then there is a set T with two elements one from each of the two elements of S”. That is a sort of trivial version of the axiom of choice for finite sets.
Now we don’t need AC to prove that: it follows from the other axioms of ZF.
If S is a countable set of non empty sets, then we need something more: the Axiom of countable choice, and if S is an arbitrary set, then we need AC itself.
That is I think all that quote means. It isn’t anything to do with choosing from among models, but given a set in a model, choosing from within that set.
Maybe you are asking whether we can prove the completeness of first order logic from ZF or whether we need ZFC to prove it?

LikeLike

Reply
Karim Zahidi

January 23, 2014

As far as I can see the quote is about formalizations of bits of ordinary mathematics and whether these formalizations require the axiom of choice. So, say you want to formalize Euclid’s Elements (or parts thereof). Apart from the properly geometric axioms, you will need some axioms about sets. The question is how much of set theory does one need to substantiate some of the moves Euclid makes in deriving geometric theorems. One of those moves consists in picking an arbitrary element, proving whatever one needs to prove and then use universal generalization. So no axiom of choice is required, provided you have something like universal generalization among the rules of inference in the deductive apparatus underlying the formalization.
The issues touched upon in the quote seem to be independent from the meta-theoretical questions you are asking, which seem to be centered around the question how much set theory is needed to construct models or to derive metamathematical theorems. I’m not quite sure whether there are very general answers to this type of question, because I would guess that even for very basic procedures in model theory, choice is needed. For example, you mention strong versions of Lowenheim-Skolem about the existence of denumerable models whose domains are the natural number and wonder whether these might show that in the construction of models ZF might suffice. I doubt whether this is the case, for, as far as I know, all proofs of the LS-theorem depend on the axiom of choice. So the existence of these models is already dependent on the axiom of choice.
I hope this helps (although I have a nagging feeling that I didn’t quite catch your point).

LikeLike

Reply
Jon Cogburn

January 23, 2014

Yeah, I get that he’s saying that at the beginning of the quote.
I thought he was saying something stronger at the end though, that because we know that universal introduction (and existential elimination) are kosher, that choice isn’t an issue with standard first order logic.
I wasn’t asking about having to use choice in completeness proofs, though that is almost certainly equivalent to one of the two issues (and maybe with respect to soundness for the other). Again, I was asking about whether choice has to be used in (1) constructing countermodels, and (2) meta-linguistic establishing that a claim is true over all models.
For the second issue, choice clearly entails that certain meta-linguistic proof strategies are kosher. Again proving that an existentially quantified claim E(x)Phi(x) is logically true just is proving that for each of an infinite set of models at least one object is in the extension of Phi. Just note that from a semantic perspective, the claim that an existential is logically true is itself a Pi 2 (for all, there exists) claim. Maybe it’s easier to look at the converse (whether some claims can only be established as logically true via choice) if we use unique existence (E! or just use existential and fill in the rest to establish uniqueness), then you really do have what looks to be a choice function when you ask about whether the claim is true in the full infinite set of models.
But maybe this doesn’t really require choice in first-order logic because of the ways the downward Lowenheim-Skolem theorem can be strengthened. And maybe this has some connection to use of choice in proving soundness and/or completeness. I don’t know.

LikeLike

Reply
Jon Cogburn

January 23, 2014

Ooh thanks. That’s very helpful.
The reason I wondered about Choice and first versus higher order logic is that you get really, really weird stuff with the continuum hypothesis and expressibility. In second order logic it is true at all models if it is true.
The only point I think you missed is the question with respect to the existential property in intuitionist logic. An existentially quantified claim is only provable in intuitionist logic if one can find a witness and prove the claim of that witness (likewise, a disjunction is only provable when one of the disjuncts is). In addition to conservative extension issues, this is the main claim to constructivity for intuitionistic logic.
This kind of constructivity for intuitionist logic contrasts sharply with the way the axiom of choice is presented as non-constructive.
Classical logic, on the other hand, has all sorts of existentially quantified theorems where the claim with the quantifier removed and a name replacing the variable is not provable. But showing existentially quantified claims to be classically valid semanticly requires meta-linguistic proof of a Pi 2 formula (for all models there is at least one object that satisfies the formula in question). If we use a uniqueness existential then it looks even more like a choice function rendering the claim true (for all models there is exactly one object in question).
Moore is going to go on to discuss intuitionism so I probably should have waited until I got to that part in the book before broaching the question of the intuitionist existence property.

LikeLike

Reply
Alex Clark

January 23, 2014

“Again proving that an existentially quantified claim E(x)Phi(x) is logically true just is proving that for each of an infinite set of models at least one object is in the extension of Phi.”
Yes, but this doesn’t need the Axiom of Choice, surely? The axiom of choice would allow you to make a further claim that there is a set which consists of one object from each model, which you don’t need to establish the claim.

LikeLike

Reply
Jon Cogburn

January 23, 2014

O.K. that seems clear now with respect to the second issue.
Your “surely” is a little bit misplaced though, and not just because of my set theoretic incompetence. Again, for constructivists an existential is never assertible unless the claim is provable with respect to an individual. So for them the proof that a Pi 2 sentence is valid does seem to require choice.*
But of course (hopefully not misplaced) I was talking about classical logic, so you are absolutely right.
For the classical logic a Pi 2 claim where the existential is the uniqueness existential E! choice does seem to be required. Since E! can be expressed in regular logic, e.g. Ex(Phi(x) & ~E(y)(P(y) & ~(y = x),** there’s probably something here.
Does the existential property hold in classical logic for E!? If it does then a certain kind of constructivist critique of classical logic might be undermined, for the uses of choice in utilizing semantics for first order classical logic*** will be unproblematic then from a constructivist perspective.
[Notes:
*Ironically, choice is for this very reason no problem for someone whose constructivism dictates adoption of Heyting semantics for the logical operators. For this person, choice is trivially true.
** In Latexese “\exists x\,( P(x) \, \wedge \neg \exists y\,(P(y) \wedge y \ne x))”
***I just mean providing countermodels and determining validity, not the use of choice in proving things like Lowenheim-Skolem.]

LikeLike

Reply
Richard

January 23, 2014

Often at the end of a well taught normal meta-theory class, over half the class still has no idea why we’ve proved all this stuff. At the end of a well taught modal logic class, this simply doesn’t happen.
Actually, could you shed a little light on the significance of completeness proofs in modal logic (or point in me the direction of where I can find some light)?

LikeLike

Reply
Benedict Eastaugh

January 24, 2014

As far as I know, all proofs of the LS-theorem depend on the axiom of choice.

This is essentially correct, although the situation is slightly more subtle. There are different versions of the Löwenheim–Skolem theorem, but all of them require some form of choice. We assume ZF; then the following equivalences hold.
1) The axiom of Dependent Choice, DC, is equivalent to “Every model M of a first-order theory T with a countable signature has an elementary submodel N of at most countable cardinality”.
2) The Axiom of Choice, AC, is equivalent to “Every model M of a first-order theory T with a signature of cardinality k has an elementary submodel N with cardinality at most k”.
The upwards Löwenheim–Skolem theorem just needs compactness, so it’s equivalent over ZF to the ultrafilter lemma.
This area has been very well studied; lots of forms of LS and AC are known, and we have a lot of equivalences.

LikeLike

Reply
Richard Heck

January 24, 2014

Benedict and Karim: Can’t the simplest version of L-S be proven without choice? This is just: If a theory T with countable signature is consistent, then it has a countable model. That just falls out of the usual proof of the completeness theorem, which does not require choice. (It has a natural proof in I\Sigma_1.)
Any form involving submodels will require choice, and of course those are the most interesting and useful forms.

LikeLike

Reply
Benedict Eastaugh

January 24, 2014

Richard: I don’t personally know very much about the arithmetised completeness theorem provable in I\Sigma_1 besides what I gleaned from skimming through the Hájek and Pudlák book a while ago, but as far as I understand the notion of model involved is pretty weak. Once we move to say, second order arithmetic, we get stronger definitions of a model and correspondingly, the principles required to prove LS-style theorems increase in strength also. So for example RCA0 has a notion of a weak model, and the completeness theorem (and thus presumably any form of LS) for this definition of a model requires WKL0. Once we move to ZF, choice principles are required to prove completeness and LS theorems.
For the I\Sigma_1 version that you stated, once you stop quantifying over cardinals it stops feeling like LS and is just the model existence lemma from the completeness theorem. And as you say, the most interesting and useful forms are those involving submodels (I can’t remember ever using LS without that part). So I’m not really sure it deserves the appellation. But I don’t think this is a substantive disagreement.

LikeLike

Reply
Ansten Klev

January 26, 2014

I believe that what Moore has in mind are such assumptions as are made at the opening of the proof of a general proposition: let a be such and such; or, let a, b, and c be such and such. Such phrases are ubiquitous in the Elements.
Already Bishop (1967) noted that AC is true on the constructive understanding of the quantifiers. For a proof in Constructive Type Theory see page 50 of Martin-Löf’s book. See also Martin-Löf’s paper on AC, “100 years of Zermelo’s Axiom of Choice: What was wrong with it?” There is, finally, John Bell’s quite recent book, available online.

LikeLike

Reply