wf of terms

MetaPRL Tutorial: Well-formedness

The first step in creating the logic is to declare a term to define well-formedness of expressions. We use the term type to provide a well-formedness type judgment. Proofs of well-formedness are computationally meaningless, and we also declare a trivial proof term trivial.

To form this judgment we create a module Fol_type. First, create an interface:

Create the file fol_type.mli, containing the line:

declare "type"{'A}
declare trivial

The intent of this term is that if the expression type{'t} is provable, then the term 't is a well-formed formula.

Next, we create the implementation. The rules for well-formedness will be stated in the module for the logical operators, so the only implementation we need to include is the syntax declaration and a display form to produce pretty output.

Create the file fol_type.ml containing the following lines:

include Base_theory
declare "type"{'A}
declare trivial
dform type_df : "type"{'A} = slot{'A} `" type"
dform trivial_df : trivial = cdot

The Base_theory is included for basic logic and display form definitions. The display form prints the term type{'t} as the term 't type. The trivial term is printed as the single character \cdot, which is defined in the Nuprl_font module in the Base_theory theory.

Next we are going to compile this theory.

Edit MetaprlInfo file:

THEORYNAME = fol
THEORYDESCR = First-Order Logic

THEORY_DEPS[] +=
    itt/core

# Library files
MPFILES[] =
    fol_type

then execute % omake in shell.

Now the module is compiled and linked with the editor, and we can view this theory in the editor.