recursively axiomatizable theory

Let T be a first order theory. A subset ΔT is a set of axioms for T if and only if T is the set of all consequences of the formulasMathworldPlanetmathPlanetmath in Δ. In other words, φT if and only if φ is provable using only assumptionsPlanetmathPlanetmath from Δ.

Definition. A theory T is said to be finitely axiomatizablePlanetmathPlanetmath if and only if there is a finite setMathworldPlanetmath of axioms for T; it is said to be recursively axiomatizable if and only if it has a recursive setMathworldPlanetmath of axioms.

For example, group theory is finitely axiomatizable (it has only three axioms), and Peano arithmeticMathworldPlanetmathPlanetmath is recursivaly axiomatizable : there is clearly an algorithm that can decide if a formula of the languagePlanetmathPlanetmath of the natural numbersMathworldPlanetmath 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 characteristicPlanetmathPlanetmath p for any number p prime or 0. It is completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, 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