Timeline for When does Skolemization require the axiom of choice?
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| 21 hours ago | comment | added | Juan Atacama | @EmilJeřábek Where can I find a purely syntactic proof that Skolemization of a theory T (we can assume that the language of T is countable) is a conservative extension of T? By purely syntactic, I mean one in which only finite strings are worked with, without using both model theory and ZF set theory. | |
| Dec 19, 2014 at 16:43 | comment | added | Emil Jeřábek | ... requires a weak (actually, not so weak) form of choice, namely the Boolean prime ideal theorem. But having said that, the choice schema $(*)$ may be true in a Henkin-style model even if the axiom of choice fails for sequences of subsets of the model, because the validity of the schema only concerns sequences of sets uniformly definable in the model by a formula. | |
| Dec 19, 2014 at 16:38 | comment | added | Emil Jeřábek | I’m not sure this is the right way to think about it. First, usual skolemization in one-sorted first-order theories still has a different meaning than the kind of skolemization you consider in the higher-order (multi-sorted first-order) theories: the former is a metamathematical closure property of the logic (a form of an admissible rule), whereas the latter is an actual formula (or schema) in the logic. It’s also problematic to involve semantics in the issue, since just like for plain first-order logic, the completeness and compactness of Henkin semantics (for uncountable languages) ... | |
| Dec 18, 2014 at 21:18 | comment | added | dezakin | Does this mean using Henkin semantics doesn't require choice then, because first order theories don't require choice for Skolemization and Henkin semantics essentially makes higher order theories multi-sorted first order theories? | |
| Dec 18, 2014 at 19:20 | vote | accept | dezakin | ||
| Dec 18, 2014 at 15:48 | history | edited | Emil Jeřábek | CC BY-SA 3.0 |
added 980 characters in body
|
| Dec 18, 2014 at 14:31 | comment | added | Asaf Karagila♦ | Everyone knows that second-order logic is set theory in sheep clothing. "Bahhh... baahhhh..." | |
| Dec 18, 2014 at 14:27 | history | answered | Emil Jeřábek | CC BY-SA 3.0 |