[Home]First-order theory

HomePage | RecentChanges | Preferences

A first-order formula is an expression constructed from atomic formulas combined with logical connectives not,  and  ,  or  ,   ⇒  ,   ⇔   and quantifiers , followed by variables.

The first-order theory of a class of structures is the set of first-order formulas that hold in all members of the class.

The decision problem for the first-order theory of a class of structures is the problem with input: a first-order formula 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 decidable if there is an algorithm that solves the decision problem, otherwise it is undecidable.

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, and shows that a set of formulas is a first-order theory of a class of structures (of the appropriate language) iff it is closed under the 'usual' rules of logical deduction.


HomePage | RecentChanges | Preferences
This page is read-only | View other revisions
Last edited March 15, 2003 7:52 pm (diff)
Search: