Next: 8. Theories Up: 2. User's Guide Previous: 2. User's Guide

Subsections

# 7.1 Introduction

The logic of IMPS is called LUTINS7.1, a Logic of Undefined Terms for Inference in a Natural Style. LUTINS is a kind of predicate logic that is intended to support standard mathematical reasoning. It is classical in the sense that it allows nonconstructive reasoning, but it is nonclassical in the sense that terms may be nondenoting. The logic, however, is bivalent; formulas are always defined.

Unlike first-order predicate logic, LUTINS provides strong support for specifying and reasoning about partial functions (i.e., functions which are not necessarily defined on all arguments), including the following mechanisms:

• -notation for specifying functions;
• an infinite hierarchy of function types for organizing higher-order functions, i.e., functions which take other functions as arguments;
• full quantification (universal and existential) over all function types.
In addition to these mechanisms, LUTINS possesses a definite description operator and a system of subtypes, both of which are extremely useful for reasoning about functions as well as other objects.

The treatment of partial functions in LUTINS is studied in [4], while the treatment of subtypes is the subject of [5]. In this chapter we give a brief overview of LUTINS. For a detailed presentation of LUTINS, see [16]7.2.

# 7.2 Languages

A LUTINS language contains two kinds of objects: sorts and expressions. Sorts denote nonempty domains of elements (mathematical objects), while expressions denote members of these domains. Expressions are used for both referring to elements and making statements about them.

In this section we give a brief description of a hypothetical language . This language will be presented using the mathematical syntax'' which will be used throughout the rest of the manual. There are other syntaxes for LUTINS, including the string syntax'' introduced in Chapter 3 and the s-expression syntax'' presented in [16].

Expressions are formed by applying constructors to variables, constants, and compound expressions. The constructors are given in Table 7.1; they serve as logical constants'' that are available in every language. Variables and constants belong to specific languages.

Table 7.1: Table of Constructors
 Constructor String syntax Mathematical syntax the-true truth the-false falsehood not not(p) and p1 and ... and pn or p1 or ... or pn implies p1 implies p2 iff p1 iff p2 if-form if_form(p1,p2,p3) forall forall(v1:s1,...,vn:sn,p) forsome forsome(v1:s1,...,vn:sn,p) equals t1=t2 t1 = t2 apply f(t1,...,tn) lambda lambda(v1:s1,...,vn:sn,t) iota iota(v1:s1,p) iota-p iota_p(v1:s1,p) if if(p,t1,t2) is-defined #(t) defined-in #(t,s) undefined ?s

In the mathematical syntax, the symbols for the constructors, the common punctuation symbols, and the symbol with are reserved. By a name, we mean any unreserved symbol.

## 7.2.1 Sorts

The sorts of are generated from a finite set of names called atomic sorts. More precisely, a sort of is a sequence of symbols defined inductively by:

1.
Each is a sort of .
2.
If are sorts of with , then is a sort of .
Sorts of the form are called compound sorts. In the next section we shall show that a compound sort denotes a domain of functions. Let denote the set of sorts of .

assigns each a member of called the enclosing sort of . The atomic/enclosing sort relation determines a partial order on with the following properties:

1.
If and is the enclosing sort of , then .
2.
iff
.
3.
If with and is compound, then is compound and has the same length as .
4.
For every there is a unique such that and is maximal with respect to .
is intended to denote set inclusion.

The members of which are maximal with respect to are called types. A base type is a type which is atomic. Every language has the base type which denotes the set of standard truth values. The type of a sort , written , is the unique type such that . The least upper bound of and , written , is the least upper bound of and in the partial order . (The least upper bound of two sorts with the same type is always defined).

A function sort is a sort such that has the form . The range sort of a function sort , written , is defined as follows: if , then ; otherwise, where is the enclosing sort of .

Sorts are divided into two kinds as follows: A sort is of kind if either it is or it is a compound sort where is of kind ; otherwise it is of kind . We shall see later the purpose behind this division. All atomic sorts except are of kind .

## 7.2.2 Expressions

contains a set of names called constants. Each constant is assigned a sort in . An expression of of sort is a sequence of symbols defined inductively by:

1.
If x is a name and then is an expression of sort .
2.
If is of sort , then A is an expression of sort .
3.
If are expressions of sort with , then

## 7.2.3 Alternate Notation

Expressions will usually be written in an abbreviated form as follows. Suppose A is an expression whose free variables are . Then A is abbreviated as

where A' is the result of replacing each (free or bound) occurrence of a variable in A with xi. This mode of abbreviation preserves meaning as long as there are not two variables and with which are either both free in A or both in the scope of the same binder in A.

Parentheses in expressions may be suppressed when meaning is not lost. In addition, the following alternate notation may be used in the IMPS mathematical syntax:

1.
prop and ind in place of the base sorts and , respectively.

2.
in place of a compound sort , and in place of a compound sort with of kind .

3.
The symbol .'' in place of ,'' at the end of variable-sort sequence; e.g., instead of .

4.
in place of the biconditional .

5.
in place of

6.
in place of .

# 7.3 Semantics

The semantics for a LUTINS language is defined in terms of models that are similar to models of many-sorted first-order logic. Let be a LUTINS language, and let denote the set of sorts of .

A frame for is a set of nonempty domains (sets) such that:

1.
( ).
2.
If , then .
3.
If is of kind , then is the set of all partial functions .
4.
If is of kind , then is the set of all total functions such that, for all , whenever for at least one i with .
For a type of kind , is defined inductively by:
1.
.
2.
If , then is the function which maps every n-tuple to .

A model for is a pair where is a frame for and I is a function which maps each constant of of sort to an element of .

Let be a model for . A variable assignment into is a function which maps each variable of to an element of . Given a variable assignment into ; distinct variables ; and , , let

be the variable assignment such that

is the partial binary function on variable assignments into and expressions of defined by the following statements:

1.
2.
If A is a constant, .
3.
.
4.
.
5.
6.
7.
8.
If is or ,
9.
10.
11.
12.
13.
14.
Assume F is of kind . Then

if are each defined; otherwise
is undefined.
15.
Assume F is of sort of kind . Then

if are each defined; otherwise
.
16.
Assume A is of sort of kind . Then is the partial function such that

if is defined; otherwise is undefined.
17.
Assume A is of sort of kind . Then is the total function such that

if ; otherwise .
18.
is the unique element such that ; otherwise is undefined.
19.
is the unique element such that ; otherwise .
20.
21.
22.
is undefined.

Clearly, for each variable assignment into and each expression A of ,

1.
if is defined, and
2.
is defined if A is of kind .
is called the value or denotation of A in with respect to , provided it is defined. When is not defined, A is said to be nondenoting in with respect to .

# 7.4 Extensions of the Logic

The logic can be effectively extended by introducing quasi-constructors.'' They are the subject of Chapter 10.

# 7.5 Hints and Cautions

1.
In most cases, the novice IMPS user is better off relying on his intuition instead of trying to fully comprehend the formal semantics of LUTINS.

2.
Although IMPS can handle expressions containing two variables with the same name (such as, and with ), they tend to be confusing and should be avoided if possible.

3.
LUTINS is a logic of two worlds: the world and the world. Expressions of kind are part of the world, and expressions of kind are part of the world. Although both worlds can be used for encoding mathematics, the world is much preferred for this purpose. As a general rule, expressions of kind should not be used to denote mathematical objects. Normally, formulas or predicates (i.e., expressions having a sort of the form ) are the only useful expressions of kind . Consequently, there is little support in IMPS for the constructor , the definite description operator for the world.

4.
The character % is often used in the names of variables and constants in the string syntax to denote a space (the character _ is used to denote the start of a subscript). This character is printed in the mathematics syntax as either % or _.

Next: 8. Theories Up: 2. User's Guide Previous: 2. User's Guide