A.2 The second presentation

In this sectionPlanetmathPlanetmath, there are three kinds of judgments {mathpar} Γ 𝖼𝗍𝗑Γ ⊒a : A Ξ“ ⊒a ≑a’ : A which we specify by providing inference rules for deriving them. A typical inference rule has the form


It says that we may derive the conclusionMathworldPlanetmath π’₯, provided that we have already derived the hypotheses π’₯1,…,π’₯k. (Note that, being judgments rather than types, these are not hypotheses internal to the type theoryPlanetmathPlanetmath in the sense of Β§1.1 (http://planetmath.org/11typetheoryversussettheory); they are instead hypotheses in the deductive system, i.e.Β the metatheoryMathworldPlanetmath.) On the right we write the Name of the rule, and there may be extra side conditions that need to be checked before the rule is applicable.

A derivation of a judgment is a tree constructed from such inference rules, with the judgment at the root of the tree. For example, with the rules given below, the following is a derivation of β‹…βŠ’Ξ»x.x:πŸβ†’πŸ. {mathpar} \inferrule*[right=Ξ -intro] \inferrule*[right=𝖡𝖻𝗅𝖾] \inferrule*[right=𝖼𝗍𝗑-ext] \inferrule*[right=𝟏-form] \inferrule*[right=𝖼𝗍𝗑-emp] Β  ⋅ 𝖼𝗍𝗑 ⊒𝟏 : 𝒰 _0 x : πŸΒ π–Όπ—π—‘ x : 𝟏 ⊒x : 𝟏 β‹… ⊒λx. x : 𝟏 β†’πŸ

Title A.2 The second presentationMathworldPlanetmathPlanetmath