Timeline for What logic can express this sentence?
Current License: CC BY-SA 3.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 18, 2015 at 3:02 | comment | added | cody | 2nd order logic is undecidable, no quantifier elimination procedure exists for it. | |
| Dec 17, 2015 at 23:45 | comment | added | user84230 | Is there any result on QE for such 2nd order logic of real closed field, or 2nd order logic of arithmetic? What is the richest class for which QE result exists? Thanks. | |
| Dec 17, 2015 at 23:41 | comment | added | user84230 | So the sentence is \forall x,y,i: x(i) > y(i), which is a sentence of 2nd order logic, for qunatification over function. While seq of reals can itself be coded in 2nd order theory of arithmetic, or 1st order theory of real closed field. Thanks. | |
| Dec 17, 2015 at 22:52 | history | edited | cody | CC BY-SA 3.0 |
Answered follow up question
|
| Dec 17, 2015 at 22:48 | comment | added | cody | First order logic allows for fixed functions, so if your sequences $x_i$ and $y_i$ are fixed (you don't want to quantify over them) then you can do it in multi-sorted first order logic with 2 additional function symbols. But if you want to quantify over the sequences, you need something extra. Of course set theory can be specified in first order logic with enough symbols, so it really depends on what you allow. I was taking as basis the 1st order theory of Real Closed Fields vs the 2nd order theory of Arithmetic also called analysis precisely because you can encode sequences of reals. | |
| Dec 17, 2015 at 22:46 | comment | added | user84230 | Also about quantifer elimination, is there any result for L_{\omega_1,\omega}? | |
| Dec 17, 2015 at 22:39 | comment | added | user84230 | Thanks for your answer. Even 1st order logic allows functions, and so sequences. On the other hand, the quantification over index i is just over a variable, rather a set/predicate/function. So in what way 2nd order logic helping express the sentence? | |
| Dec 17, 2015 at 21:53 | history | edited | cody | CC BY-SA 3.0 |
Wording
|
| Dec 17, 2015 at 18:45 | history | answered | cody | CC BY-SA 3.0 |