Let's now look into the Vernacular. When we start the system the Vernacular is in normal mode. In normal mode we may issue a command to the system. For instance, we may ask to type check a term and obtain in this way the type of a given term. Most Vernacular commands alter the state. They are the commands required to save theorems, to extend the environment in which proofs are performed by adding declarations. For instance, in the slide we have added an axiom LEM for the law of excluded middle, which is the given formula. And in the same way we may add parameters, variables, hypotheses. Then we have definitions, where we may associate a name to a term. Let me remark the difference between an axiom and a definition: An axiom introduces a hypotheses - we are assuming the validity of a formula. The formula may be used during a proof by referring to its name. On the other hand, a definition is just a mere abbreviation: id is simply a shorthand for the longer term given in the slide.

---