Timeline for Is there a syntactic proof that first-order positive inductive definitions are conservative?
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 5 at 8:04 | comment | added | Emil Jeřábek | Anyway, I can't make any sense of the claim at the end. First, so far you didn't mention anything that would force the fixed point to be the least one (which is actually impossible with FO axioms), or even that it shares some FO properties of the least fixed point. So, the fixed point you end up with might just be the whole model, not anything resembling the standard integers. Second, even if you did, at best you'd end up with "Con(PA) relativized to the new fixed point predicate", not Con(PA) as such. Indeed, the latter would contradict conservativity of the extension. | |
| Sep 5 at 7:57 | comment | added | Emil Jeřábek | What exactly are the axioms about the fixed point that you are adding? Just that it is a fixed point? | |
| Sep 5 at 3:03 | comment | added | François G. Dorais | I have no firm expertise nor guidance here, but Moschovakis likely gave some thought to this. That might be worth looking into if you haven't already. | |
| S Sep 5 at 0:37 | review | First questions | |||
| Sep 5 at 3:58 | |||||
| S Sep 5 at 0:37 | history | asked | Vann McGee | CC BY-SA 4.0 |