Horn theory

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** = **propositions as types** +**programs as proofs** +**relation type theory/category theory**

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

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

$\phi_1 \wedge \ldots \wedge \phi_n \vdash \phi$

where each $\phi_i$ and $\phi$ is atomic. A (universal) **Horn theory** is a theory in which every axiom is a Horn clause.

Revised on August 25, 2012 21:44:45
by Urs Schreiber
(82.113.106.150)