7. Logic Overview

7.1 Introduction

The logic of IMPS is called LUTINS^7.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:

• $\lambda$-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 $\mathcal L$ . 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	$\mbox{${\sf T}$ }$
the-false	falsehood	$\mbox{${\sf F}$ }$
not	not(p)	$\neg\varphi$
and	p1 and ... and pn	$\varphi_1 \wedge \ldots \wedge \varphi_n$
or	p1 or ... or pn	$\varphi_1 \vee \ldots \vee \varphi_n$
implies	p1 implies p2	$\varphi\supset \psi$
iff	p1 iff p2	$\varphi\equiv \psi$
if-form	if_form(p1,p2,p3)	$\mbox{if-form}(\varphi_1,\varphi_2,\varphi_3)$
forall	forall(v1:s1,...,vn:sn,p)	$\forall{v_1\mbox{:}\alpha_1,\ldots,v_n\mbox{:}\alpha_n},\varphi$
forsome	forsome(v1:s1,...,vn:sn,p)	$\exists{v_1\mbox{:}\alpha_1,\ldots,v_n\mbox{:}\alpha_n},\varphi$
equals	t1=t2	t1 = t2
apply	f(t1,...,tn)	$f(t_1,\ldots,t_n)$
lambda	lambda(v1:s1,...,vn:sn,t)	$\lambda{v_1\mbox{:}\alpha_1,\ldots,v_n\mbox{:}\alpha_n},t$
iota	iota(v1:s1,p)	$\iota{v\mbox{:}\alpha},\varphi$
iota-p	iota_p(v1:s1,p)	$\iota_{\rm p}{v\mbox{:}\alpha},\varphi$
if	if(p,t1,t2)	$\mbox{if}(\varphi,t_1,t_2)$
is-defined	#(t)	$t\!\!\downarrow$
defined-in	#(t,s)	$t\downarrow\alpha$
undefined	?s	$\bot_\alpha$

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 $\mathcal L$ are generated from a finite set $\mathcal A$ of names called atomic sorts. More precisely, a sort of $\mathcal L$ is a sequence of symbols defined inductively by:

1.

Each $\alpha \in \mbox {$\mathcal A$ }$ is a sort of $\mathcal L$ .

2.

If $\alpha_1,\ldots,\alpha_{n+1}$ are sorts of $\mathcal L$ with $n \geq 1$, then $[\alpha_1,\ldots,\alpha_{n+1}]$ is a sort of $\mathcal L$ .

Sorts of the form $[\alpha_1,\ldots,\alpha_{n+1}]$ are called compound sorts. In the next section we shall show that a compound sort denotes a domain of functions. Let $\mathcal S$ denote the set of sorts of $\mathcal L$ .

$\mathcal L$ assigns each $\mathcal A$ a member of $\mathcal S$ called the enclosing sort of $\alpha$. The atomic/enclosing sort relation determines a partial order $\preceq$ on $\mathcal S$ with the following properties:

1.

If $\alpha \in \mbox {$\mathcal A$ }$ and $\beta$ is the enclosing sort of $\alpha$, then $\alpha \preceq \beta$.

2.

$\alpha_1 \preceq \beta_1,\ \ldots,\ \alpha_n \preceq \beta_n,\ \alpha_{n+1} \preceq \beta_{n+1}$ iff
$[\alpha_1,\ldots,\alpha_n,\alpha_{n+1}] \preceq [\beta_1,\ldots,\beta_n,\beta_{n+1}]$.

3.

If $\alpha, \beta\in \mbox {$\mathcal S$ }$ with $\alpha \preceq \beta$ and $\alpha$ is compound, then $\beta$ is compound and has the same length as $\alpha$.

4.

For every $\alpha \in \mbox {$\mathcal S$ }$ there is a unique $\beta\in \mbox {$\mathcal S$ }$ such that $\alpha \preceq \beta$ and $\beta$ is maximal with respect to $\preceq$.

$\preceq$ is intended to denote set inclusion.

The members of $\mathcal S$ which are maximal with respect to $\preceq$ are called types. A base type is a type which is atomic. Every language has the base type $\ast$ which denotes the set $\{\mbox{\sc t},\mbox{$\mbox{\sc f}_{}$ }\}$ of standard truth values. The type of a sort $\alpha$, written $\tau(\alpha)$, is the unique type $\beta$ such that $\alpha \preceq \beta$. The least upper bound of $\alpha$ and $\beta$, written $\alpha \sqcup \beta$, is the least upper bound of $\alpha$ and $\beta$ in the partial order $\preceq$. (The least upper bound of two sorts with the same type is always defined).

A function sort is a sort $\alpha$ such that $\tau(\alpha)$ has the form $[\alpha_1,\ldots,\alpha_n,\alpha_{n+1}]$. The range sort of a function sort $\alpha$, written $\textrm{ran}(\alpha)$, is defined as follows: if $\alpha = [\alpha_1,\ldots,\alpha_n,\alpha_{n+1}]$, then $\textrm{ran}(\alpha)=\alpha_{n+1}$; otherwise, $\textrm{ran}(\alpha)=\textrm{ran}(\beta))$ where $\beta$ is the enclosing sort of $\alpha$.

Sorts are divided into two kinds as follows: A sort is of kind $\ast$ if either it is $\ast$ or it is a compound sort $[\alpha_1,\ldots,\alpha_{n+1}]$ where $\alpha_{n+1}$ is of kind $\ast$; otherwise it is of kind $\iota$. We shall see later the purpose behind this division. All atomic sorts except $\ast$ are of kind $\iota$.

7.2.2 Expressions

$\mathcal L$ contains a set $\mathcal C$ of names called constants. Each constant is assigned a sort in $\mathcal S$ . An expression of $\mathcal L$ of sort $\alpha$ is a sequence of symbols defined inductively by:

1.

If x is a name and $\alpha \in \mbox {$\mathcal S$ }$ then $x\mbox{:}\alpha$ is an expression of sort $\alpha$.

2.

If $A \in \mbox {$\mathcal C$ }$ is of sort $\alpha$, then A is an expression of sort $\alpha$.

3.

If $A,B,C,A_1,\ldots,A_n$ are expressions of sort $\ast$with $n \geq 0$, then ${\sf T}$

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 $x_1\mbox{:}\alpha_1,\ \ldots,\ x_n\mbox{:}\alpha_n$. Then A is abbreviated as

$$(\mbox{with}\ x_1\mbox{:}\alpha_1,\ldots,x_n\mbox{:}\alpha_n,\ A'),$$

where A' is the result of replacing each (free or bound) occurrence of a variable $x_i\mbox{:}\alpha_i$ in A with x_i. This mode of abbreviation preserves meaning as long as there are not two variables $x\mbox{:}\alpha$ and $x\mbox{:}\beta$ with $\alpha\not=\beta$ 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 $\ast$ and $\iota$, respectively.

2.

$\alpha_1\times\cdots\times\alpha_n \rightarrow \beta$ in place of a compound sort $[\alpha_1,\ldots,\alpha_n,\beta]$, and $\alpha_1\times\cdots\times\alpha_n \rightharpoonup \beta$ in place of a compound sort $[\alpha_1,\ldots,\alpha_n,\beta]$ with $\beta$ of kind $\iota$.

3.

The symbol ``.'' in place of ``,'' at the end of variable-sort sequence; e.g., $\exists x\mbox{:}\alpha.x=x$ instead of $\exists x\mbox{:}\alpha,x=x$.

4.

$\Leftrightarrow$ in place of the biconditional $\equiv$.

5.

$\exists!{x\mbox{:}\alpha},\varphi(x)$ in place of $\exists{x\mbox{:}\alpha},(\varphi(x) \wedge \forall{y\mbox{:}\alpha}, (\varphi(y) \supset x=y)).$

6.

$A \not= B$ in place of $\neg(A = B)$.

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 $\mathcal L$ be a LUTINS language, and let $\mathcal S$ denote the set of sorts of $\mathcal L$ .

A frame for $\mathcal S$ is a set $\{\mbox {$\mathcal D$ }_\alpha : \alpha \in \mbox {$\mathcal S$ }\}$ of nonempty domains (sets) such that:

1.

$\mbox {$\mathcal D$ }_\ast = \{\mbox{\sc t},\mbox{$\mbox{\sc f}_{}$ }\}$ ( $\mbox{\sc t}\not=\mbox{$\mbox{\sc f}_{}$ }$).

2.

If $\alpha \preceq \beta$, then $\mbox {$\mathcal D$ }_\alpha \subseteq \mbox {$\mathcal D$ }_{\beta}$.

3.

If $\alpha = [\alpha_1,\ldots,\alpha_n,\alpha_{n+1}]$ is of kind $\iota$, then $\mbox {$\mathcal D$ }_\alpha$ is the set of all partial functions $f: \mbox {$\mathcal D$ }_{\alpha_1}\times\cdots\times\mbox {$\mathcal D$ }_{\alpha_n}\rightarrow\mbox {$\mathcal D$ }_{\alpha_{n+1}}$ .

4.

If $\alpha = [\alpha_1,\ldots,\alpha_n,\alpha_{n+1}]$ is of kind $\ast$, then $\mbox {$\mathcal D$ }_\alpha$ is the set of all total functions $f: \mbox {$\mathcal D$ }_{\tau(\alpha_1)}\times\cdots\times\mbox {$\mathcal D$ }_{\tau(\alpha_n)}\rightarrow\mbox {$\mathcal D$ }_{\alpha_{n+1}}$ such that, for all ${\langle b_1,\ldots,b_n\rangle} \in \mbox {$\mathcal D$ }_{\tau(\alpha_1)}\times\cdots\times\mbox {$\mathcal D$ }_{\tau(\alpha_n)}$ , $f(b_1,\ldots,b_n)= \mbox{$\mbox{\sc f}_{\tau(\alpha_{n+1})}$ }$ whenever $b_i \not\in \mbox {$\mathcal D$ }_{\alpha_i}$ for at least one i with $1 \leq i \leq n$.

For a type $\alpha \in \mbox {$\mathcal S$ }$ of kind $\ast$, $\mbox{$\mbox{\sc f}_{\alpha}$ }$ is defined inductively by:

1.

$\mbox{$\mbox{\sc f}_{\ast}$ } = \mbox{$\mbox{\sc f}_{}$ }$.

2.

If $\alpha = [\alpha_1,\ldots,\alpha_{n+1}]$, then $\mbox{$\mbox{\sc f}_{\alpha}$ }$ is the function which maps every n-tuple ${\langle a_1,\ldots,a_n\rangle} \in \mbox {$\mathcal D$ }_{\alpha_1} \times \cdots \times \mbox {$\mathcal D$ }_{\alpha_n}$ to $\mbox{$\mbox{\sc f}_{\alpha_{n+1}}$ }$.

A model for $\mathcal L$ is a pair $(\{\mbox {$\mathcal D$ }_\alpha : \alpha \in \mbox {$\mathcal S$ }\},I)$ where $\{\mbox {$\mathcal D$ }_\alpha : \alpha \in \mbox {$\mathcal S$ }\}$ is a frame for $\mathcal S$ and I is a function which maps each constant of $\mathcal L$ of sort $\alpha$ to an element of $\mbox {$\mathcal D$ }_\alpha$ .

Let $\mbox {$\mathcal M$ }= (\{\mbox {$\mathcal D$ }_\alpha : \alpha \in \mbox {$\mathcal S$ }\},I)$ be a model for $\mathcal L$ . A variable assignment into $\mathcal M$ is a function which maps each variable $x\mbox{:}\alpha$ of $\mathcal L$ to an element of $\mbox {$\mathcal D$ }_\alpha$ . Given a variable assignment $\varphi$ into $\mathcal M$ ; distinct variables $x_1\mbox{:}\alpha_1,\ldots,x_n\mbox{:}\alpha_n\ (n\geq 1)$; and $a_1 \in \mbox {$\mathcal D$ }_{\alpha_1}, \ldots a_n \in \mbox {$\mathcal D$ }_{\alpha_n}$, , let

$$\varphi[x_1\mbox{:}\alpha_1\mapsto{a_1}, \ldots,x_n\mbox{:}\alpha_n\mapsto{a_n}]$$

be the variable assignment $\psi$ such that

$$\psi(A) = \left\{\begin{array}{ll} a_i & \mbox{if $A=x_i\mbo... ... \leq n$}\\ \varphi(A) & \mbox{otherwise} \end{array}\right.$$

$V = V^{\cal M}$ is the partial binary function on variable assignments into $\mathcal M$ and expressions of $\mathcal L$ defined by the following statements:

1.

$V_\varphi(x\mbox{:}\alpha) = \varphi(x\mbox{:}\alpha)$

2.

If A is a constant, $V_\varphi(A) = I(A)$.

3.

$V_\varphi(\mbox{${\sf T}$ })=\mbox{\sc t}$.

4.

$V_\varphi(\mbox{${\sf F}$ })=\mbox{$\mbox{\sc f}_{}$ }$.

5.

$V_\varphi(\neg(A))= \left\{\begin{array}{ll} \mbox{\sc t}& \mbox{if $V_\varphi... ...}_{}$ }$ }\\ \mbox{$\mbox{\sc f}_{}$ } & \mbox{otherwise} \end{array}\right.$

6.

$V_\varphi(A \supset B)= \left\{\begin{array}{ll} \mbox{\sc t}& \mbox{if $V_\va... ...{\sc t}$ }\\ \mbox{$\mbox{\sc f}_{}$ } & \mbox{otherwise} \end{array}\right.$

7.

$V_\varphi(A \equiv B) = \left\{\begin{array}{ll} \mbox{\sc t}& \mbox{if $V_\v... ...rphi(B)$ }\\ \mbox{$\mbox{\sc f}_{}$ } & \mbox{otherwise} \end{array}\right.$

8.

If $\Box$ is $\mbox{if-form}$ or $\mbox{if}$, $V_\varphi(\Box(A,B,C))= \left\{\begin{array}{ll} V_\varphi(B) & \mbox{if $V_\varphi(A)=\mbox{\sc t}$ }\\ V_\varphi(C) & \mbox{otherwise} \end{array}\right.$

9.

$V_\varphi(A_1 \wedge \cdots \wedge A_n)= \left\{\begin{array}{ll} \mbox{\sc t}... ...{\sc t}$ }\\ \mbox{$\mbox{\sc f}_{}$ } & \mbox{otherwise} \end{array}\right.$

10.

$V_\varphi(A_1 \vee \cdots \vee A_n)= \left\{\begin{array}{ll} \mbox{\sc t}& \m... ... \leq n$ }\\ \mbox{$\mbox{\sc f}_{}$ } & \mbox{otherwise} \end{array}\right.$

11.

$V_\varphi(\forall\ x_1\mbox{:}\alpha_1,\ldots,x_n\mbox{:}\alpha_n,\ A) = \left\... ...alpha_n}$ }\\ \mbox{$\mbox{\sc f}_{}$ } & \mbox{otherwise} \end{array}\right.$

12.

$V_\varphi(\forall\ x_1\mbox{:}\alpha_1,\ldots,x_n\mbox{:}\alpha_n,\ A) = \left\... ...alpha_n}$ }\\ \mbox{$\mbox{\sc f}_{}$ } & \mbox{otherwise} \end{array}\right.$

13.

$V_\varphi(A=B) = \left\{\begin{array}{ll} \mbox{\sc t}& \mbox{if $V_\varphi(A... ...varphi(B)$ }\\ \mbox{$\mbox{\sc f}_{}$ } & \mbox{otherwise} \end{array}\right.$

14.

Assume F is of kind $\iota$. Then

$$V_\varphi(F(A_1,\ldots,A_n)) = V_\varphi(F)(V_\varphi(A_1),\ldots,V_\varphi(A_n))$$

if $V_\varphi(F),V_\varphi(A_1),\ldots,V_\varphi(A_n)$ are each defined; otherwise
$V_\varphi(F(A_1,\ldots,A_n))$ is undefined.

15.

Assume F is of sort $[\alpha_1,\ldots,\alpha_{n+1}]$ of kind $\ast$. Then

$$V_\varphi(F(A_1,\ldots,A_n)) = V_\varphi(F)(V_\varphi(A_1),\ldots,V_\varphi(A_n))$$

if $V_\varphi(A_1),\ldots,V_\varphi(A_n)$ are each defined; otherwise
$V_\varphi(F(A_1,\ldots,A_n))=\mbox{$\mbox{\sc f}_{\tau(\alpha_{n+1})}$ }$.

16.

Assume A is of sort $\alpha_{n+1}$ of kind $\iota$. Then $V_\varphi(\lambda\ x_1\mbox{:}\alpha_1,\ldots,x_n\mbox{:}\alpha_n,\ A)$ is the partial function $f: \mbox {$\mathcal D$ }_{\alpha_1}\times\cdots\times\mbox {$\mathcal D$ }_{\alpha_n}\rightarrow\mbox {$\mathcal D$ }_{\alpha_{n+1}}$ such that

$$f(a_1,\ldots,a_n) =V_{\varphi[x_1\mbox{:}\alpha_1\mapsto{a_1}, \ldots,x_n\mbox{:}\alpha_n\mapsto{a_n}]}(A)$$

if $V_{\varphi[x_1\mbox{:}\alpha_1\mapsto{a_1}, \ldots,x_n\mbox{:}\alpha_n\mapsto{a_n}]}(A)$ is defined; otherwise $f(a_1,\ldots,a_n)$ is undefined.

17.

Assume A is of sort $\alpha_{n+1}$ of kind $\ast$. Then $V_\varphi(\lambda\ x_1\mbox{:}\alpha_1,\ldots,x_n\mbox{:}\alpha_n,\ A)$ is the total function $f: \mbox {$\mathcal D$ }_{\tau(\alpha_1)}\times\cdots\times\mbox {$\mathcal D$ }_{\tau(\alpha_n)}\rightarrow\mbox {$\mathcal D$ }_{\alpha_{n+1}}$ such that

$$f(a_1,\ldots,a_n) =V_{\varphi[x_1\mbox{:}\alpha_1\mapsto{a_1}, \ldots,x_n\mbox{:}\alpha_n\mapsto{a_n}]}(A)$$

if ${\langle a_1,\ldots,a_n\rangle} \in \mbox {$\mathcal D$ }_{\alpha_1} \times \cdots \times \mbox {$\mathcal D$ }_{\alpha_n}$ ; otherwise $f(a_1,\ldots,a_n)= \mbox{$\mbox{\sc f}_{\tau(\alpha_{n+1})}$ }$.

18.

$V_\varphi(\iota x\mbox{:}\alpha,A)$ is the unique element $a \in \mbox {$\mathcal D$ }_\alpha$ such that $V_{\varphi[x\mbox{:}\alpha \mapsto a]}(A) = \mbox{\sc t}$; otherwise $V_\varphi(\iota x\mbox{:}\alpha,A)$ is undefined.

19.

$V_\varphi(\iota_{\rm p}x\mbox{:}\alpha,A)$ is the unique element $a \in \mbox {$\mathcal D$ }_\alpha$ such that $V_{\varphi[x\mbox{:}\alpha \mapsto a]}(A) = \mbox{\sc t}$; otherwise $V_\varphi(\iota_{\rm p}x\mbox{:}\alpha,A) = \mbox{$\mbox{\sc f}_{\tau(\alpha)}$ }$.

20.

$V_\varphi(A\!\!\downarrow)= \left\{\begin{array}{ll} \mbox{\sc t}& \mbox{if $V... ...s defined}\\ \mbox{$\mbox{\sc f}_{}$ } & \mbox{otherwise} \end{array}\right.$

21.

$V_\varphi(A\downarrow\alpha)= \left\{\begin{array}{ll} \mbox{\sc t}& \mbox{if ... ..._\alpha$ }\\ \mbox{$\mbox{\sc f}_{}$ } & \mbox{otherwise} \end{array}\right.$

22.

$V_\varphi(\bot_\alpha)$ is undefined.

Clearly, for each variable assignment $\varphi$ into $\mathcal M$ and each expression A of $\mathcal L$ ,

1.

$V_\varphi(A) \in \mbox {$\mathcal D$ }_\alpha$ if $V_\varphi(A)$ is defined, and

2.

$V_\varphi(A)$ is defined if A is of kind $\ast$.

$V_\varphi(A)$ is called the value or denotation of A in $\mathcal M$ with respect to $\varphi$, provided it is defined. When $V_\varphi(A)$ is not defined, A is said to be nondenoting in $\mathcal M$ with respect to $\varphi$.

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, $x\mbox{:}\alpha$ and $x\mbox{:}\beta$ with $\alpha\not=\beta$), they tend to be confusing and should be avoided if possible.

3.

LUTINS is a logic of two worlds: the $\iota$ world and the $\ast$ world. Expressions of kind $\iota$ are part of the $\iota$world, and expressions of kind $\ast$ are part of the $\ast$ world. Although both worlds can be used for encoding mathematics, the $\iota$world is much preferred for this purpose. As a general rule, expressions of kind $\ast$ should not be used to denote mathematical objects. Normally, formulas or predicates (i.e., expressions having a sort of the form $[\alpha_1,\ldots,\alpha_n,\ast]$) are the only useful expressions of kind $\ast$. Consequently, there is little support in IMPS for the constructor $\iota_{\rm p}$, the definite description operator for the $\ast$ 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 _.