consequent

**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 *consequent* or *conclusion* judgement on the right of the “$\vdash$”-symbol of a sequent/hypothetical judgement: a judgement that is a consequence of the antecedent judgements on the left of the symbol.

If there is more than one disjunctively connected consequent, these are called the *succedents*.

antecedents$\vdash$ succedents

antecedents$\vdash$ **consequent**

Last revised on September 27, 2012 at 23:22:46. See the history of this page for a list of all contributions to it.