Timeline for Restricting First Order Logic to make it decidable [closed]
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 25, 2019 at 13:14 | history | closed |
Andrej Bauer Pace Nielsen YCor Piotr Hajlasz Joseph Van Name |
Not suitable for this site | |
| Feb 21, 2019 at 11:12 | comment | added | Hauke Reddmann | Ha. I knew there was something fishy with the "standard" answer...(And feel free to close, I have my answer.) | |
| Feb 21, 2019 at 11:07 | vote | accept | Hauke Reddmann | ||
| Feb 20, 2019 at 19:51 | comment | added | Alex Kruckman | As the answer and Emil's link show, the fact that there are infinitely many ground terms has nothing to do with undecidability. Indeed, first-order logic is undecidable in a signature with a single binary relation and no function symbols (so there are no terms other than the variables). While on the other hand, first-order logic is decidable in a signature with a single unary function symbol and a single constant symbol (where there are infinitely many ground terms: $c$, $f(c)$, $f(f(c))$, $\dots$). | |
| Feb 20, 2019 at 16:19 | comment | added | Pace Nielsen | I'm voting to close this question as it was previously answered. | |
| Feb 20, 2019 at 15:53 | answer | added | tomkot | timeline score: 4 | |
| Feb 20, 2019 at 14:45 | review | Close votes | |||
| Feb 25, 2019 at 13:14 | |||||
| Feb 20, 2019 at 11:59 | comment | added | Emil Jeřábek | Various restrictions on the signature and/or on the quantifier prefix that guarantee decidability are mentioned in the question mathoverflow.net/questions/83399/… and in my answer there. | |
| Feb 20, 2019 at 10:15 | history | asked | Hauke Reddmann | CC BY-SA 4.0 |