Timeline for why Skolemization?
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 23, 2012 at 14:06 | comment | added | Jason Rute | Ryan, the main point is that the innermost existential and universal quantifiers are bounded. In theories powerful enough to encode arithmetic, bounded number quantifiers can be removed by encoding finite sets as numbers. This makes the statement an $\exists \forall$ statement. As for your second question, yes one can just get rid of the inner existential by taking $M(\varepsilon,F)$ to be the minimal $m$ that satisfies the property. But the value of just using a bound is that a bound can be much more uniform. Notice my example. This version is more useful in applications. | |
| Nov 23, 2012 at 6:20 | comment | added | Ryan Reich | I don't understand; you haven't gotten rid of all the inner existential quantifiers. Do you mean to just set $m = M(\varepsilon, F)$, rather than supposing that it is bounded by it? | |
| Nov 22, 2012 at 17:18 | comment | added | Jason Rute | Andreas, yes this is basically Gödel's Dialectica interpretation. (In my mind I think of it as Skolemization which made me think to put it here). Thanks for the clarification! | |
| Nov 22, 2012 at 3:43 | comment | added | Andreas Blass | I like this answer, but I'd point out that, by going to an object $M$ two types higher than the base domains, it's rather different from the usual Skolemizations (and Herbrandizations) that one uses in first-order logic (where one goes up one type but then quickly removes the quantifiers over that higher type). In fact, this notion of metastability looks to me more like a Dialectica-style interpretation (though I confess that no exact correspondence to Dialectica is clear to me at the moment). | |
| Nov 22, 2012 at 1:50 | history | answered | Jason Rute | CC BY-SA 3.0 |