The Language Pt. 3

A proof consists of four types of sentences.

1. Deductions
2. Variable declarations
3. Constant declarations
4. Namespace declarations

DEDUCTIONS

Proof sentences consist of a name atom, a colon, a list of comma-separated antecedant propositions, a deduction symbol, and a consequent proposition, followed by a justification or a subproof. Subproofs are proofs encased in either curly or square brackets. The last line of a subproof must have no step name, no antecedants and a consequent matching that of the step the subproof justifies. Some examples are:

1. T4: u+w=v+w ⊨ u=v Rep(T3)

2. T4: ⊨ u=v {
      : u=v MP(T1,T2);     
   }

VARIABLE DECLARATIONS

A variable declaration consists of the keyword Var, a semantic type, and an atom, optionally followed by an argument list, consisting of atoms that are also variables. If there is no argument list, the variable's semantic type will be exactly the one given. If there are arguments, the type of the variable will be the compound type which has the types of arguments as the domain list, and the given type as the range type. The variables used as arguments must be defined in the same scope as the declaration. Some examples of variable declarations are:

1. Var 0 x;
2. Var 0 y;
3. Var 0 z(x,y)

CONSTANT DECLARATIONS

A constant declaration consists of the keyword Const, a semantic type, an atom optionally followed by an argument list. This can in turn be optionally followed by the "≜" symbol and then a definition. If there is no argument list, the variable's semantic type will be exactly the one given. If there are arguments, the type of the variable will be the compound type which has the types of arguments as the domain list, and the given type as the range type. The variables used as arguments must be defined in the same scope as the declaration. Free variables occuring in the definition must either be the arguments in the argument list or variables declared outside of the present scope. The definition must have the same semantic type as the one given in the prototype.

1. Const 0 C;
2. Const 0 g(x,y)≜f(x)+y;
3. Const 0 a+b≜sum(a,b);

In a constant declaration number patterns may be used. For example the declaration

Const 0 .real.#=nat2real(.#);

The above example will have the effect of defining .real.0,.real.1,... as nat2real(.0),nat2real(.1). By using a namespace declaration such as

Use namespace .real with {digit}+;

numbers without explicit namespaces will be implicitly assumed to have namespace .real.

NAMESPACE DECLARATIONS

A namespace declaration has the form:

Use namespace <namespace sequence> with <regular expression>.

Some examples are

• Use namespace . with {equals};
• Use namespace .real.sub1 with T{alpha}*;
• Use namespace .real.sub2.a with {alnum}+⋃{plus};

Following a namespace declaration, whenever an atom matches the regular expression in the namespace declaration, if the atom has no explicit namespace prefix, the one refered to in the namespace declaration will be assumed. A namespace declaration that follows a previous one will partly override the previous one in that if an atom doesn't match its regular expression, an attempt will then be made to match it against using the previous one, then the one previous to that, etc. In a subproof the namespace declarations in all the underlying scopes will also be matched against unless the subproof is encapsulated in square brackets. Whenever a subproof is encapsulated in square brackets the namespace stack is entirely reset within the scope of the subproof. Once again, this feature is not very useful at the moment, but it will be in the future.