Timeline for first-order definability transitive closure operator
Current License: CC BY-SA 2.5
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 20, 2010 at 8:04 | comment | added | Gerhard Paseman | OK. Am I misremembering what Kunen has? I won't attempt the exact syntax, but is there not a first order predicate something like the unique w such that w is transitive and x subset of w and for any y which is transitive and for which x subset y, we have w subset y? Or am I still missing something? | |
| Jan 20, 2010 at 4:50 | comment | added | François G. Dorais | Your statement $x = TC(x)$ (and the pseudoformula accompanying it) only says "$x$ is transitive." Adam wants to prove the existence of the transitive closure of set $x$, not a criterion for when $x$ is transitive. | |
| Jan 20, 2010 at 3:36 | comment | added | Gerhard Paseman | Then what do you need? Something like existsunique w forallz,y (y in x) implies (y in w) and (y in w) and (z in y) implies (z in w) ? I could expand out exists unique if you like, and continue adding clauses, but I thought you would do that. Or am I misremembering, and Kunen does not have a first order expression? | |
| Jan 20, 2010 at 3:28 | comment | added | Adam | Thanks, but if I write a big expression involving "TC(x)", I cannot simply replace the "TC(x)" with what you have provided (which is otherwise perfectly accurate!) -- the result will not be a legitimate formula. In fact, what you write is the "$\phi$" mentioned in my question above -- it is the predicate which expresses the fact that its argument is the transitive closure of $x$. | |
| Jan 20, 2010 at 3:11 | history | answered | Gerhard Paseman | CC BY-SA 2.5 |