nLab
Horn theory

Idea

A Horn theory is a theory in which every axiom has a certain special form.

Definition

Let $\Sigma$ be a signature. A term of $\Sigma$ is an expression built out of variables and function symbols. (For example, $x{y}^{-1}z$ is a term in the language of groups.) An atomic formula relative to $\Sigma$ is a formula that consists of a relation symbol of $\Sigma$ (including equality) applied to terms.

A Horn clause is a logical expression of the form

$${\varphi }_1\wedge \dots \wedge {\varphi }_n⊢\varphi$$\phi_1 \wedge \ldots \wedge \phi_n \vdash \phi

where each ${\varphi }_i$ and $\varphi$ is atomic. A (universal) Horn theory is a theory in which every axiom is a Horn clause.

Related concepts

• modular lattice