recursively axiomatizable theory
Let be a first order theory. A subset is a set of axioms for if and only if is the set of all consequences of the formulas in . In other words, if and only if is provable using only assumptions
from .
Definition. A theory is said to be finitely axiomatizable if and only if there is a finite set
of axioms for ; it is said to be recursively axiomatizable if and only if it has a recursive set
of axioms.
For example, group theory is finitely axiomatizable (it has only three axioms), and Peano arithmetic is recursivaly axiomatizable : there is clearly an algorithm that can decide if a formula of the language
of the natural numbers
is an axiom.
Theorem. recursively axiomatizable theories are decidable.
As an example of the use of this theorem, consider the theory of algebraically closed fields of characteristic for any number prime or 0. It is complete
, and the set of axioms is obviously recursive, and so it is decidable.