Timeline for decidable fragments of first-order logic without the finite countermodel property
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 20, 2011 at 19:39 | history | edited | symplectomorphic | CC BY-SA 3.0 |
added 29 characters in body
|
| Dec 20, 2011 at 18:34 | history | edited | symplectomorphic | CC BY-SA 3.0 |
clarified the question
|
| Dec 20, 2011 at 18:26 | comment | added | symplectomorphic | Revised the question question in light of your first comment. | |
| Dec 14, 2011 at 15:21 | vote | accept | symplectomorphic | ||
| Dec 14, 2011 at 12:53 | comment | added | Emil Jeřábek | Also, it’s important that the Bernays–Schönfinkel class does not allow any function symbols. | |
| Dec 14, 2011 at 12:51 | comment | added | Emil Jeřábek | The Bernays–Schönfinkel class $\exists^\*\forall^\*$ has FMP for satisfiability. Validity of $\exists^\*\forall^\*$-sentences is in fact undecidable. If you want FMP for validity (or falsifiability), you need to define the class dually: $\forall^\*\exists^\*$. | |
| Dec 14, 2011 at 11:39 | answer | added | Emil Jeřábek | timeline score: 7 | |
| Dec 14, 2011 at 6:15 | history | asked | symplectomorphic | CC BY-SA 3.0 |