Differences

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.