first-order 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 **first-order theory** is a theory which allows for quantification over variables, but not over sets of variables. It is a theory (= language + axioms) in a language consisting of the language of first-order logic, plus additional relation, function and constant symbols.

The characterization of models over first-order theories is the topic of traditional model theory.

Formulation of set theory is a first-order theory, such as

Revised on March 26, 2014 04:40:25
by Urs Schreiber
(185.37.147.12)