Also see Sequents, for supplementary material.


next up previous contents index
Next: The Type System Up: Semantics Previous: The Type System

Judgements

The significance of the so--called judgements  lies in the fact that they constitute the claims of a proof. They are the units of assertion ; they are the objects of inference. The judgements of have the form

where are distinct variables and are terms (n may be 0), every free variable of is one of , and every free variable of S or of s is one of . The list is called the hypothesis  list or assumption  list, each : is called a declaration  (of ), each is called a hypothesis  or assumption , S is called the consequent  or conclusion , s the extract  term (the reason will be seen later), and the whole thing is called a sequent .

Before explaining the conditions which make a sequent true   we shall define a relation , where H is a hypothesis list and l is a list of terms, and we shall define what it is for a sequent to be true  at a list of terms.

:,,: if and only if
*
* &
* if

We can also express this relation by saying that every is a member of

and every is type --functional in , where means the set  type

The sequent


is true at if and only if
* (
* &
* )
* if :,,:
* &

Equivalently, we can say that s is S--functional in if
:,,: . The sequent

is true if and only if
* is true at

The connection between functionality and the truth of sequents lies in the fact that S is type--functional (or s is S--functional) in if and only if T is a type and for each member t of T, S is type--functional (s is S--functional) in {x:T| x=t in T}. Therefore, s is S--functional in if and only if T is a type and the sequent x:T >> S [ext s] is true.gif

It is not always necessary to declare a variable with every hypothesis in a hypothesis list. If a declared variable does not occur free in the conclusion, extract term or any hypothesis, then the variable (and the colon following it) may be omitted.

In it is not possible for the user to enter a complete sequent directly; the extract  term must be omitted. In fact, a sequent is never displayed with its extract term. The system has been designed so that upon completion of a proof, the system automatically provides, or extracts, the extract term. This is because in what is anticipated to be the standard mode of use, the user tries to prove that a certain type is inhabited without regard to the identity of any member. One expects that in this mode the user thinks of the type (that is to be shown inhabited) as a proposition, and that it is merely the truth of this proposition that the user wants to show. When one does wish to show explicitly that or that , one instead shows the type (a = b in A) or the type  (a in A) to be inhabited.gif

Also, the system can often extract a term from an incomplete  proof when the extraction is independent of the extract terms of any unproven claims within the proof body. Of course, such unproven claims may still contribute to the truth of the proof's main claim. For example, it is possible to provide an incomplete proof of the untrue sequent >> 1<1 [ext axiom], the extract term axiom being provided automatically.

Although the term extracted from a proof of a sequent is not displayed in the sequent, the term is accessible by other means through the name assigned to the proof in the user's library. It should be noted that in the current system proofs named in the user's library cannot be proofs of sequents with hypotheses.



next up previous contents index
Next: The Type System Up: Semantics Previous: The Type System


Also see Sequents, for supplementary material.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995