Beta Phase: Square45 is currently in beta testing. Expect some features or content to be incomplete or missing.
45

Finite axiomatization

A theory is finitely axiomatizable if it can be defined by a finite set of axioms.
📜

The statement of the theorem

Let L\text{L} be a first-order language, and let TT be a formal theory in L\text{L}. We denote Ax\text{Ax} as the set of axioms defining TT, such that T=Cn(Ax)T = \text{Cn}(\text{Ax}), where Cn(⋅)\text{Cn}(\cdot) is the closure under logical consequence. The theory TT is said to be finitely axiomatizable if there exists a finite set of formulas Ax0={A1,A2,…,Ak}k∈N\text{Ax}_0 = \{A_1, A_2, \dots, A_k\}_{k \in \mathbb{N}} such that T=Cn(Ax0)T = \text{Cn}(\text{Ax}_0). Equivalently, TT is finitely axiomatizable if there exists a finite set of axioms Ax0\text{Ax}_0 such that for every formula ϕ∈T\phi \in T, Ax0⊢ϕ\text{Ax}_0 \vdash \phi. This condition is often formalized by stating that the set of axioms Ax\text{Ax} is recursively enumerable and that TT is generated by a finite basis.