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: