recursively axiomatizable theory

Let $T$ be a first order theory. A subset $\mathrm{\Delta }\subseteq T$ is a set of axioms for $T$ if and only if $T$ is the set of all consequences of the formulas in $\mathrm{\Delta }$. In other words, $\phi \in T$ if and only if $\phi$ is provable using only assumptions from $\mathrm{\Delta }$.

Definition. A theory $T$ is said to be finitely axiomatizable if and only if there is a finite set of axioms for $T$; 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 $p$ for any number $p$ prime or 0. It is complete, and the set of axioms is obviously recursive, and so it is decidable.

Title	recursively axiomatizable theory
Canonical name	RecursivelyAxiomatizableTheory
Date of creation	2013-03-22 12:43:13
Last modified on	2013-03-22 12:43:13
Owner	mathcam (2727)
Last modified by	mathcam (2727)
Numerical id	7
Author	mathcam (2727)
Entry type	Definition
Classification	msc 03C07
Defines	finitely axiomatizable