Timeline for When does Skolemization require the axiom of choice?
Current License: CC BY-SA 3.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 20, 2022 at 14:10 | comment | added | saolof | It can be worth adding that even without having the equality, you can often include the function in the definitions that would have made you use the first form. See Bishop defining a continuous function as one which is uniformly continuous on every compact subset for example. You can just put functions everywhere and avoid introducing existentials in the first place. | |
| Dec 18, 2014 at 19:20 | vote | accept | dezakin | ||
| Dec 18, 2014 at 17:24 | comment | added | Andreas Blass | By referring to the statement $(\forall x\exists y\,\phi(x,y))\iff(\exists f\forall x\,\phi(x,f(x))$ as an identity, the OP probably meant that this statement should be valid, i.e., true in all structures. If that was the intention, then, as Joel said, the full axiom of choice is required. | |
| Dec 18, 2014 at 14:32 | comment | added | Emil Jeřábek | @Joel: Well, it’s not entirely clear to me what is the original question (as I commented on in my answer), but I’m almost certain that properties of skolemization of plain first-order theories is not what it asks for. I merely mentioned it in the comment above to put things into context. | |
| Dec 18, 2014 at 14:27 | answer | added | Emil Jeřábek | timeline score: 8 | |
| Dec 18, 2014 at 14:10 | comment | added | Joel David Hamkins | @EmilJeřábek, why not post an answer explaining the situation? To Skolemize the theory and have a conservative extension does not require any AC; to get some model of that Skolemized theory generally requires some choice, even when you start with a satisfiable theory; to expand a given model to satisfy the Skolem theory is fully equivalent to AC. | |
| Dec 18, 2014 at 13:50 | comment | added | Emil Jeřábek | Right. This is a nice example showing how the completeness theorem fails in absence of the BPIT. | |
| Dec 18, 2014 at 13:01 | comment | added | Joel David Hamkins | Yes, as I indicated I was referring only to the model-expansion version of conservativity (and this also is often called conservativity--is there another term?), and this is equivalent to AC. But even if you are just looking at the theory version, if we have a collection of finite sets $A_i$, and we write down the corresponding theory $T$ asserting that $f(i)\in A_i$, using constant symbols for the elements of each $A_i$, then it will require choice for finite sets to get a model of this theory. The proofs-are-finite observation shows that the theory is conservative, but it has no models! | |
| Dec 18, 2014 at 12:47 | comment | added | Emil Jeřábek | You obviously can't talk about uncountable languages directly in arithmetic, but even so, conservativity of Skolem extensions in arbitrary languages is provable without choice (for one thing, a given proof only involves a finite sublanguage). Conservativity does not imply that you can expand an arbitrary model to a model with Skolem functions, this is a stronger property. | |
| Dec 18, 2014 at 12:29 | comment | added | Joel David Hamkins | But is the version of the Skolem theorem that one would formalize in a weak fragment of arithmetic really the same theorem as the one we might want to consider in a set theoretic context, with uncountable languages and whatnot? The conservativity result on Skolem functions (asserting that one can expand any model to a model with a Skolem function) is obviously equivalent to AC, for the reasons that have been mentioned. | |
| Dec 18, 2014 at 12:13 | comment | added | Emil Jeřábek | It might be worth stressing that the usual Skolem theorem for first-order logic (i.e., that the skolemization of a theory is its conservative extension) does not require any choice, or even set theory for that matter (it can be formalized in a weak fragment of arithmetic). | |
| Dec 18, 2014 at 6:57 | history | edited | Asaf Karagila♦ |
edited tags
|
|
| Dec 18, 2014 at 6:56 | answer | added | Asaf Karagila♦ | timeline score: 8 | |
| Dec 18, 2014 at 4:02 | comment | added | dezakin | I don't know that it's obviously full choice and not something weaker like countable choice, since first order theories have countable models. As someone who is a not a mathematician, choice always being required for any Skolemization is acceptable as an answer, but I find it a bit surprising given how readily I use Skolemization for my proof calculus. | |
| Dec 18, 2014 at 3:40 | comment | added | Joel David Hamkins | Isn't this obviously a choice principle? The function $f$ is making choices for you, choosing for each $x$ a particular witness $y$, namely $y=f(x)$, among all the possible witnesses $y$ that could work. It seems like the very essence of choice, and any instance of choice could be converted into such a case. | |
| Dec 18, 2014 at 3:30 | history | asked | dezakin | CC BY-SA 3.0 |