# Differences

This shows you the differences between two versions of the page.

first-order_theory [2011/07/14 02:52] jipsen |
first-order_theory [2011/07/14 03:05] (current) jipsen |
||
---|---|---|---|

Line 10: | Line 10: | ||

of length $n$ (as a string) and output: "true" if the formula holds in all members of the class, and "false" otherwise. | of length $n$ (as a string) and output: "true" if the formula holds in all members of the class, and "false" otherwise. | ||

- | The first-order theory is \emph{decidable} if there is an algorithm that solves the decision problem, otherwise it is \emph{undecidable}. | + | A first-order theory is \emph{decidable} if there is an algorithm that solves the decision problem, otherwise it is \emph{undecidable}. |

+ | | ||

+ | A first-order theory is \emph{hereditarily undecidable} if every consistent subtheory is undecidable. | ||

The complexity of the decision problem (if known) is one of PTIME, NPTIME, PSPACE, EXPTIME, ... | The complexity of the decision problem (if known) is one of PTIME, NPTIME, PSPACE, EXPTIME, ... | ||

The completeness theorem for first-order logic, due to Kurt Gödel, provides a complete deductive system for first-order logic, | The completeness theorem for first-order logic, due to Kurt Gödel, provides a complete deductive system for first-order logic, | ||

- | and shows that a set of formulas is a first-order theory of a class of structures (of the appropriate language) iff it is | + | and shows that a set of formulas is a first-order theory of a class of structures (of the appropriate language) if and only if it is |

closed under the 'usual' rules of logical deduction. | closed under the 'usual' rules of logical deduction. | ||

Trace: