notation for assumptions is a comma-separate list of "term : type" that precede the turnstile symbol ''. Thus, the example statement is formally written: x:bool, y:nat (if x y y) : nat If there are no assumptions, there will be nothing to the left of the turnstile: S : nat nat The list of assumptions is called the "context". It is very common to see the symbol '' used to represent some or all of the assumptions. Thus, the formal notation for the 4 different judgements is usually: (NOTE: The judgement of equality of terms is where the phrase "judgemental equality" comes from. ) The judgements enforce that every term has a type. The type will restrict which rules can be applied to a term. Rules A type theory's rules say what judgements can be made, based on the existence of other judgements. The rules are expressed using a horizontal line, with the required input judgements above the line and the resulting judgement below the line. The rule for creating a lambda term is: The judgements required to create the lambda term go above the line. In this case, only one judgement is required. It is that there is some term "b" of some type "B", assuming there is some term "a" of some type "A" and some other assumptions "". (Note: "" "a", "A", "b", and "B" are all metavariables in the rule.) The resulting judgement goes below the line. This rule's resulting judgement states that the new lambda term has type "A B" under the other assumptions . The rules are syntactic and work by rewriting. Thus, the metavariables like "", "a", "A", etc. may actually consist of complex terms that contain many function applications, not just single symbols. To generate a particular judgement in type theory, there must be a rule to generate it. Then, there must be rules to generate all of that rule's required inputs. And then rules for all the inputs for those rules. The applied rules form a proof tree. This is usually drawn Gentzen-style, where the target judgement (root) is at the bottom and rules that do not require any inputs (leaves) at the top (see Natural deduction#Proofs_and_type_theory). An example of a rule that does not require any inputs is one that states there is a term "0" of type "nat": A type theory usually has a number of rules, including ones