Timeline for Reference request: eliminating function symbols in predicate logic
Current License: CC BY-SA 3.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 27, 2016 at 15:13 | comment | added | Colin McLarty | The technique is there, yes, but this result understates the result in OP's question, since co-validity is not the same thing as being a conservative extension. And on its face this theorem finds for each formula $\alpha$ two different formulas: one co-satisfiable with $\alpha$ and one co-valid, while OP cites a uniform translation from sentences using the function to sentences not, with an axiom making the two provably equivalent. Probably Bell and Machover somewhere state OP's result as OP states it but this theorem is not it. | |
| Jan 27, 2016 at 13:47 | vote | accept | Peter LeFanu Lumsdaine | ||
| Jan 27, 2016 at 13:12 | history | edited | Håkon R. Gylterud | CC BY-SA 3.0 |
Shortened google books link.
|
| Jan 27, 2016 at 12:19 | history | answered | Håkon R. Gylterud | CC BY-SA 3.0 |