**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.

- Michael Barr,
*Models of Horn theories*, in:*Categories in Computer Science and Logic*, Contemporary Math.**92**, Amer. Math. Soc. (1989) 1–7 [pdf, pdf]

Last revised on February 23, 2024 at 19:53:19. See the history of this page for a list of all contributions to it.