The unification of three calculi
EWD1123 · 1991–1995 · PDF · Source language: English. · Local OCR-derived source needs manual review.
The unification of three calculi
The purpose of this note is to show how much the predicate calculus, the relational calculus, and the regularity calculus have in common, or, more precisely, how much commonality we can design into them. Because the predicate calculus will emerge as a subcalculus of the other two calculi, we discuss the predicate calculus first.
To begin with, I assume the reader to be familiar with
- the boolean domain ${ \text{true, false}}$
the unary (prefix) operator 7 (not, negation)
the binary (infix)operators
V (or, disjunctiOn), A (and, conjunctiOn)
$\Rightarrow$ (implies,implication), $\Leftarrow$ (follows from,consequence)
$\equiv$ (equivalences or equals,equivalence or equality).
Above, the order from top to bottom coincides for the operators with the order of decreasing syntactic binding power; notice that -in order not to destroy the symmetry between them - we have given the same binding power to v and A .
In the following, $s$ is variable ranging over a domain $S$ and (primarily) $x, y, z$ will be used to denote boolean functions whose domain is $S$ . Function application will be denoted by an infix dot, preceded by a denotation of the
function and followed by a denotation of the argu-. ment to which the function is applied. The applica- tion dot has the highest binding power and associates to the left - i.e. "p.p.q" is short for "(p.p).q"-"
To express that $x$ and $y$ are the same function,one writes traditionally
$$ \langle \forall s: s \in S: x. s \equiv y. s \rangle $$
Here, the functions applied to $s$ , $vi2$ . $x$ and $y$ , are denoted by single identifiers. With the rule that application to $s$ distributes over the logical connectives, we can write the above as
$$ \langle \forall s: s \in S: (x \equiv y). s \rangle $$
with the understanding that $x \equiv y$ is now an expression denoting the function that is true wherever $x$ and $y$ are equal and is false elsewhere. The distribution can be applied repeatedly, e.g.
$$ \langle \forall s: s \in S: x. s \vee y. s \equiv 2. s \rangle $$
can be written - remember that $\equiv$ has the lowest binding power- as
$$ \langle \forall s: s \in S: (x \vee y). s \equiv 2. s \rangle $$
or even as
$$ \langle \forall s: s \in S: (x \vee y \equiv z). s \rangle $$
For reasons that will become clear later, we now propose the following abbreviation:
instead of $\left\langle {\forall s : s \in S : \left( {{}^{\prime \prime }\text{we write}}\right) {}^{\prime \prime }}\right\rbrack$ instead of
Using the square brackets, our formula expresses that the disjunction of $x$ and $y$ equivales
$$ [ x \vee y \equiv z ] \quad ; $$
our former formula , expressing that x and
$$ [ x \equiv y ] \quad \quad \quad \quad . $$
We now take what is a standard step in mathematical theory building. The step is taken after the introduction of a notational novelty - such as a new abbreviation or a "mathematical macro" - for formulae that were interpreted in a familiar domain of discourse. The step consists of starting with a clean slate and axiomatizing afresh the manipulations of the new formulae. In doing so, one creates a new domain of discourse; the role of the old, familiar domain of discourse, that used to constitute the subject matter, is thereby reduced to that of providing a possible model for the newly postu
lated theory. It is essential that the axioms of the new theory - which can be interpreted as theorems in the old universe of discourse- are clearly postulated as such and that the new theory is derived from them without reference to the model of the old universe of discourse. This is the only way to assure that the axioms of the new theory provide an interface that is independent of the old universe of discourse and that, hence, the new theory is safely applicable to alternative models.
Remark The above paragraph sketches in a bird's- eye view the process of mathematical abstraction. The result of being more abstract is not being more vague, on the contrary: the purpose of abstraction is the creation of a new semant- tic level at which one can again be absolutely precise, but with less commitment. The virtue of the new theory is that one can work in it, unburdened by the irrelevant details of the model that inspired it. Experience has shown that people's first confrontation with mathema- tical abstraction is often emotionally disturbing; the rest of the educational process hardly teaches the potential intellectual advantages of ignoring available knowledge and the manifest freedom of creating one's own universe of dis- course could very well be frightening. (End of Remark.)
We begin our axiomatization by introducing (variables $x, y, z$ of) a new type that we call "boolean structures". It contains the traditional boolean domain ${\text{true}, \text{false}}$ as subtype, whose two values are sometimes referred to as "the boolean scalars".
We introduce a function from boolean structures to boolean scalars; it is called "the everywhere operator" and is denoted by surrounding the boolean structure it is applied to by a pair of square brackets.
Legenda The axioms and theorems that follow should be universally quantified over their global variables of type boolean structure. The marks $\underline{\mathbf{A}}\mathbf{x}$ and $\underline{\mathbf{I}}\mathbf{h}$ distinguish axioms from theorems; the choice is some- what arbitrary. (End of Legenda.)
In order to express that two boolean structures $x$ and $y$ are the same we write $\left\lbrack {x \equiv y}\right\rbrack$ instead of the more usual $x = y\;\left. {\;{So},\;Leibniz's}\right.$ Principle
$$ x = y \Rightarrow f _ {x} = f _ {y} $$
we render for arguments and function values of type boolean structure as
$$ \underline {{A x}} \quad [ x \equiv y ] \Rightarrow [ f. x \equiv f. y ] $$
Remark It is understood that an expression is a
function of any of its subexpressions. (End of Remark.)
For the general infix operator $\bullet$ we define the following terms:
" $\bullet$ is associative " means $\left\lbrack {\left( {x \cdot y}\right) \cdot z \equiv x \cdot \left( {y \cdot z}\right) }\right\rbrack$ " $\bullet$ is symmetric " means $\left\lbrack {x \cdot y \equiv y \cdot x}\right\rbrack$ " $\bullet$ is idempotent" means ${\left\lbrack x \cdot x \equiv x\right\rbrack }^{2}$ ,
(the three formula to be universally quantified as usual over $x, y, z$ .) In what follows, we shall exploit associativity by omitting semantically superfluous parentheses whenever convenient - i.e. we don't hesitate to write $x \cdot y \cdot z$ for any associative $\bullet$
$A \times .\; \equiv \;$ is associative
Remark For nonboolean types, equality is not associative - its associativity would lead to a type conflict. . The associativity of equality for boolean types is therefore very special, so special that it deserves a special symbol $(\equiv)$ with a special pronunciation ("equivales"). (End of Remark.)
[\text{Ax. = is symmetric}]
${Ax}.$ $\left\lbrack {x \equiv \text{true} \equiv x}\right\rbrack$ or $\left\lbrack {x \equiv x \equiv \text{true}}\right\rbrack$
In the first version, this axiom expresses that true
is the left and right identity of $\equiv$ - note that
it admits the parsings $\left\lbrack {x \equiv \left( {\text{true} \equiv x}\right) }\right\rbrack$ and
$\left\lbrack {\left( {x \equiv \text{true}}\right) \equiv {x}^{\prime }}\right\rbrack - \cdots$ In the second version
-parsed $\left\lbrack {\left( {x \equiv x}\right) \equiv \text{true}}\right\rbrack -$ it expresses that
$x \equiv x\;$ is also the identity element of
(The existence of an identity element $\Rightarrow$
follows from the previous two axioms.)
[\left\lbrack \text{true}\right\rbrack \equiv \text{true}]
for the disjunction
Ax. is associative
[\text{Ax.}\;V\text{ is symmetric.}]
$A$ x. V is idempotent
For equivalence and disjunction together we give
A. $\vee$ distributes over $= ,$ i.e.
$$ [ x \vee (y \equiv z) \equiv x \vee y \equiv x \vee z ] $$
[\left\lbrack {\texttt{x} \vee \text{true} \equiv \text{true}}\right\rbrack \quad \text{or}\quad \left\lbrack {\texttt{x} \vee \text{true}}\right\rbrack ]
Proof We observe for any boolean structures $x,y$
$$ \begin{array}{l} x \vee \mathrm {t r u e} \ = {A x. w i t h x = y y i e l d s [ (y \equiv y) \equiv \mathrm {t r u e} ] } \ x \vee (y \equiv y) \ = {\vee \mathrm {d i s t . o v e r} \equiv } \ x \vee y \equiv x \vee y \ = {A x. w i t h x := x \vee y } \ t r u e. \ \end{array} $$
(End of Proof.)
(Note that in view of the symmetry of $v$ ,we did not need to distinguish between left and right distribution over
The conjunction $\land$ is defined by
$\left{ {\begin{array}{l} x \in A \ y \in B \end{array}\;A \subseteq B}\right.$
an axiom that is also known as The Golden Rule .
[\text{Th.}\;{\;A}\text{is associative}] [\text{Th.}\;{\;\Lambda }\;{\text{ is symmetric }}] [\text{Th.}\;{\;A}\text{is idempotent}] [ \Leftrightarrow \left\lbrack {x \land \text{true} \equiv x}\right\rbrack .]
Proof. We observe for any boolean structure $x$
$$ \begin{array}{l} x \wedge \mathrm {t r u e} \ = {\mathrm {G o l d e n R u l e w i t h} y := \mathrm {t r u e} } \ x \equiv \mathrm {t r u e} \equiv x \vee \mathrm {t r u e} \ = {\left[ x v t r u e \right] } \ x \equiv \mathrm {t r u e} \equiv \mathrm {t r u e} \ = {\mathrm {i d e n t i l y e l e m e n t o f} \equiv } \ x \quad (\mathrm {E n d o f P r o o f}). \ \end{array} $$
$\left\lbrack {x \land \left( {y \equiv z}\right) \equiv x \land y \equiv x \land z \equiv x}\right\rbrack$
Proof We observe for any (boolean structures) $x,y,z$
$$ x \wedge y \equiv x \wedge z \equiv x $$
$$ = {\mathrm {G o l d e n R u l e} \quad \mathrm {t w i c e} } $$
$$ \begin{array}{l} x \equiv y \equiv x \vee y \equiv z \equiv x \vee z \ = {\equiv s y m m e t r i c; v d i s h. o v e r \equiv } \ \end{array} $$
$$ \begin{array}{l} x \equiv y \equiv z \equiv x \vee (y \equiv z) \ = {\mathrm {G o l d e n R u l e} } \ x \wedge (y \equiv z) \ \end{array} $$
(End of Proof.)
A corollary of the last theorem is
$\land \;distribu\;tes\;over\;{}^{\prime \prime } \equiv \equiv {}^{\prime \prime },i.e.$
$$ [ u \wedge (x \equiv y \equiv z) \equiv u \wedge x \equiv u \wedge y \equiv u \wedge z ] $$
[ \land \text{and} \vee \text{distributive over each other}]
Proof Because of the symmetry of $\land$ and $\lor$ , we need not distinguish between left and right distribution. We show that $\land$ distributes over $\lor$ by observing for any $x, y, z$
$$ \begin{array}{l} x \wedge (y \vee z) \ = {\mathrm {G o l d e n R u l e} } \ x \wedge (y \equiv z \equiv y \wedge z) \ = {\wedge^ {\sim} d i s h. o v e r \equiv \equiv } \ x \wedge y \equiv x \wedge z \equiv x \wedge y \wedge z \ = {\mathrm {p r o p e r t i e s} o f \wedge } \ x \wedge y \equiv x \wedge z, \equiv x \wedge y \wedge x \wedge z \ = {\tilde {G} o l d e n R u l e } \ (x \wedge y) \vee (x \wedge z) \ \end{array} $$
(End of Proof.)
The Laws of Absorption
$$ [ x \wedge (x \vee y) \equiv x ], [ x \vee (x \wedge y) \equiv x ]. $$
Proof To demonstrate the first law of absorption we observe for any $x,y$
$$ \begin{array}{l} x \wedge (x \vee y) \equiv x \ = {\mathrm {G o l d e n R u l e w i t h} y := x \vee y } \ x \vee y \equiv x \vee x \vee y \ = {\vee i d e m p o t e n t } \ x \vee y = x \vee y \ = {\mathrm {i d e n t i t y} o f \equiv } \ \mathbf {t r u e} \ \end{array} $$
$$ (E n d o f P r o o f.) $$
$$ \begin{array}{l} \text {I m p l i c a t i o n} \Rightarrow \text {a n d c o n s e q u e n c e} \Leftarrow \text {a r e} \ \text {d e f i n e d b y t h e f o l l o w i n g t w o a x i o m s} \end{array} $$
$$ \begin{array}{l} \underline {{A x}}. \qquad [ x \Rightarrow y \equiv y \Leftarrow x ] \ \underline {{A x .}} \qquad [ x \Rightarrow y \equiv x \vee y \equiv y ] \ \end{array} $$
$$ \begin{array}{l} f r o m w h i c h w e i m m e d i a t e l y d e d u c e w i t h t h e \ \mathrm {T h .} \quad [ x \Rightarrow y \equiv x \land y \equiv x ] \ \end{array} $$
$$ \begin{array}{l} \begin{array}{l} \mathrm {A s i m p l e r e w r i t i n g o f t h e L a w s o f A b s o r p t i o n} \ \mathrm {n o w y i e l d s} \end{array} \ \underline {{I h .}} \quad [ x \Rightarrow x \vee y ] \quad a n d \quad [ x \wedge y \Rightarrow x ], \ w h i c h a r e a l s o k n o w n a s L a w s o f A b s o r p h i o n \ \mathrm {I m}. \quad [ x \Rightarrow (y \Rightarrow z) \equiv x \wedge y \Rightarrow z ] \ \mathrm {P r o o f} \quad \mathrm {W e o b s e r v e f o r a n y} x, y, z \ x \Rightarrow (y \Rightarrow z) \ = {\mathrm {e l i m i n a t e o u t e r} \Rightarrow \mathrm {w i t h} \land \equiv } \ x \wedge (y \Rightarrow z) \equiv x \ \end{array} $$
$$ \begin{array}{l} = {\text {e l i m i n a t e i n n e r} \Rightarrow \text {w i t h} \land \equiv } \ x \wedge (y \wedge z \equiv y) \equiv x \ = {\wedge \mathrm {a l m o s t d i s t r i b u t e s} \mathrm {o v e r} = } \ x \wedge y \wedge z \equiv x \wedge y \ = {\mathrm {r e i n t r o d u c t i o n} o f \Rightarrow \mathrm {w i t h} \land \equiv } \ x \wedge y \Rightarrow z \ \end{array} $$
(End of Proof)
$\left{ {\begin{array}{l} x \land \left( {x \Rightarrow y}\right) \equiv x \land y}\end{array}\rbrack }\right.$
Proof We observe for any $x, y$
$$ \begin{array}{l} x \wedge (x \Rightarrow y) \ = {\mathrm {e l i m i n a t e} \Rightarrow \mathrm {w i t h} \land \equiv } \ x \wedge (x \wedge y \equiv x) \ = {\wedge a l m o s t d i s t r i b u t e s o v e r \equiv } \ x \wedge x \wedge y \equiv x \wedge x \equiv x \ = {\wedge i s i d e m p o t e n t } \ x \wedge y \equiv x \equiv x \ = {\mathrm {i d e n t i t y} o f \equiv } \ x \wedge y \ \end{array} $$
(End of Proof.)
Remark From the above and a law of Absorption we can derive $[x \wedge (x \Rightarrow y) \Rightarrow y]$ , a law that is at least since the Middle Ages known as the Modus Ponens. These days it no longer deserves a special name. (End of Remark.)
One of the most important properties of the implication is
${TH}.$ $\Rightarrow$ is transitive , i.e.
$$ [ (x \Rightarrow y) \land (y \Rightarrow z) \Rightarrow (x \Rightarrow z) ] $$
Proof We observe for any $x,y,z$
$$ (x \Rightarrow y) \land (y \Rightarrow z) \Rightarrow (x \Rightarrow z) $$
[\left{ \begin{array}{ll} \text{ Theorem } & \text{ before last } \ & \end{array}\right} ]
$$ x \wedge (x \Rightarrow y) \wedge (y \Rightarrow z) \Rightarrow z $$
[\left{ \begin{array}{ll} \text{last theorem} \end{array}\right} ]
$$ x \wedge y \wedge (y \Rightarrow z) \Rightarrow z $$
[\left{ \begin{array}{ll} \text{ Last theorem } \ \end{array}\right} ]
$$ x \wedge y \wedge z \Rightarrow z $$
$=$ {Law of Absorption}
true
(End of Proof.)
$\Rightarrow$ is reflexive , i.e. $\left\lbrack {x \Rightarrow x}\right\rbrack$ .
$\Rightarrow$ is antisymmetric , i.e.
$$ [ (x \Rightarrow y) \wedge (y \Rightarrow x) \Rightarrow (x \equiv y) ] $$
Proof We observe for any $x,y$
$$ (x \Rightarrow y) \land (y \Rightarrow x) $$
$= { \Rightarrow \text{ in }\Lambda$ and $\equiv ,}$ twice
$$ (x \wedge y \equiv x) \wedge (x \wedge y \equiv y) $$
Punchua!
$$ (x \wedge y \equiv x) \wedge (x \equiv y) $$
$\Rightarrow$ {Absorption}
$$ x \equiv y $$
(End of Proof.)
Our earlier proofs all consisted of sequences of equivalent expressions. Now we have es-
tablished that $\Rightarrow$ is transitive, we also accept, as in the last proof, proofs of implications in which some expressions in the sequence are connected by $\Rightarrow$ to their successor.
The implication is not a symmetric operator, its two operands have therefore different names: in $x \Rightarrow y$ and in $y \Leftarrow x$ , $x$ is called the "antecedent" and $y$ is called the "consequent". In our last proof we started with the antecedent of the demonstrandum and ended up with its consequent; hence the occurrence of $\Rightarrow$ in the left-most column. We sometimes arrange implication proofs the other way round; in that case we start with the consequent and end up with the antecedent; such proofs have occurrences of $\Leftarrow$ in the left-most column.
Our last 3 theorems state that implication is transitive, reflexive, and antisymmetric, i.e. that implication is a "partial order". The adjectives "weaker" and "stronger" are in common usage to describe the "direction" of this partial order: in [antecedent ⇒ consequent] the antecedent is said to be "stronger than the consequent" and the consequent is said to be "weaker than the antecedent". (The use of the comparatives is not entirely fortunate since antecedent and consequent could be equivalent.)
The unary operator $\neg$ (not, negation) is defined by the two axioms that connect it to the equivalence and the disjunction respectively
$\left\lbrack {7\left( {x \equiv y}\right) \equiv {7x} \equiv y}\right\rbrack$ $\left\lbrack {x + 7}\right\rbrack$ (i.e. Law of the Excluded Middle).
From the first axiom by itself one can deduce
$\left\lbrack {{7x} \equiv y \equiv x \equiv {7y}}\right\rbrack$ $\left\lbrack {x \equiv {77}x}\right\rbrack$ (i.e. $\neg$ is an involution).
Together they yield another way to write the implication:
[x \rightarrow y \equiv {7x} \sim y]
Proof We observe for any $x,y$
$$ \begin{array}{l} t r u e \ = {\text {E x c l u d e d M i d d l e} } \ [ (x \equiv y) \vee \neg (x \equiv y) ] \ = {\neg \equiv } \ [ (x \equiv y) \vee (\neg x \equiv y) ] \ = {\vee d i s t r i b u t e s o v e r \equiv } \ [ x \vee \neg x \equiv x \vee y \equiv y \vee \neg x \equiv y \vee y ] \ = {\text {E x c l u d e d M i d d l e}; \vee \text {i d e m p o f e n t} } \ [ x \vee y \equiv y \vee x \equiv y ] \ = {\equiv v s y m m e t r i c; \Rightarrow i n V a n d \equiv } \ [ x \Rightarrow y \equiv 7 x \vee y ] \ \end{array} $$
(End of Proof)
An immediate consequence is what is known
as the Law of the Contrapositive
$\left\lbrack {x \Rightarrow y \equiv {7x} \Leftarrow {7y}}\right\rbrack$
Furthermore, the "laws of de Morgan" are important
$\left\lbrack {{7x} + {7y} \equiv 1\left( {x \land y}\right) }\right\rbrack$ $\left\lbrack {{7x} \land {7y} \equiv 7\left( {x \vee y}\right) }\right\rbrack$
Proof. We prove the first one by observing for any $x, y$ :
$$ \begin{array}{l} \lnot x \lor \lnot y \ = {\Rightarrow \neg \vee } \ x \Rightarrow 7 y \ = {\Rightarrow v \equiv } \ x \vee \neg y \equiv \neg y \ = {\Rightarrow \neg \vee } \ y \Rightarrow x \equiv \neg y \ = \quad {\Rightarrow v \equiv } \ y \vee x \equiv x \equiv \neg y \ = {\neg \equiv } \ 7 (y \vee x \equiv x \equiv y) \ = {G o l d e n R u l e } \ \lnot (x \land y) \ \end{array} $$
(End of Proof).
A useful equivalence is
$\left{ {\begin{array}{l} x \wedge y \Rightarrow z \ z \end{array} \equiv x \Rightarrow {7y} \vee z}\right}$
an appeal to it is called "shunting".
Closely connected to the negation is the boolean
constant "false". It is connected to true by
${A}_{x}$ . [false $\equiv 7$ true]
and to the everywhere operator by
[\text{false}\rbrack \equiv \text{false}]
We leave to the reader the proofs of
[ \Leftrightarrow \;{f}^{\prime }\left( x\right) \leq 0]
[[\text{false} \vee x \equiv x]
[ \Leftrightarrow \;{\left\lbrack \text{false} \land x \equiv \text{false}\right\rbrack }^{ * }]
We write the quantified expressions as follows. For the universally quantified expression we write
$$ \langle \forall x: r. x: t. x \rangle ; $$
for the existentially quantified expression we write
$$ \langle \exists x: r. x: t. x \rangle $$
Instead of the angular brackets $\langle \rangle$ , one can also use the normal parentheses ( ) without introducing syntactic ambiguity. For many years I used, in fact, the normal parentheses; later I learned to appreciate the angular brackets as a welcome visual aid to parsing. In the above schemata:
x -called "the dummy" - is a local variable of the quantified expression; the angular brackets de
lineate the scope of the dummy, whose type we tend to define in the environment of the quantified expression; instead of a single dummy we admit a list of dummies, say "x,y,z" instead of just "x".
r.x stands for an expression of type "predicate" which, in general, depends on the dummy. (Using the infix dot - with the highest binding power- to denote functional application, we denoted the expression in functional form, all other syntactic forms of a predicate expression are allowed as well.) The expression represented in the schemata by r.x is called "the range".
t.x - called "the term" - is also an expression of type "predicate" which, like the range, in general, depends on the dummy.
Universal quantificat i ond existential quantificat i onr all r, t connected by
$A \times \left\lbrack {\langle \exists x : r.x : t.x\rangle \equiv \neg \langle \forall x : r.x : t.x\rangle }\right\rbrack$
The syntactic categories "range" and "term" are inspired by the analogy with the notation for summation that would denote the sum of the squares of the first $K$ natural numbers by $\langle \sum n: 0 \leq n \land n < K: n^2 \rangle$ ,
the only difference being that here the term is not of type predicate (but of type integer).
With the term of type predicate , we could restrict ourselves to ranges that are true ; the following two rewrite rules are known under the name "trading":
$$ \underline {{A x}} \quad [ \langle \forall x: r. x: t. x \rangle \equiv \langle \forall x: t r u e: r. x \Rightarrow t. x \rangle ] $$
$$ [ \langle \exists x: r. x: t. x \rangle \equiv \langle \exists x: t r u e: r. x \wedge t. x \rangle ] $$
Note It is customary to omit the range (and to write :: after the dummy) if the range is true or constant all through a calculation. (End of Note.)
The following rewrite rules, known under the names "nesting" and "unnesting", are in a way the analogue of the associativity of conjunction and disjunction:
$\left{ {\forall x,y : r \cdot x \land s \cdot x.y : t \cdot x.y}\right} \equiv$
$$ \langle \forall x: r. x: \langle \forall y: s. x. y: t. x. y \rangle \rangle ] $$
[1\left\lbrack {\langle \exists x,y : r \cdot x \land s \cdot x,y : t \cdot x \cdot y}\right\rangle \equiv ]
$$ \langle \exists x: r. x: \langle \exists y: s. x. y: f. x. y \rangle \rangle ] $$
As a consequence we have the following "interchanges" of quantification
$\left\lbrack {\langle \forall x : r.x : \langle \forall y : s.y : t.x.y\rangle }\right\rangle \equiv$
$$ \langle \forall y: s. y: \langle \forall x: r. x: +. x. y \rangle \rangle ] $$
and similarly for the existential quantificati on.
The analogue of the distribution of [] over
$$ \underline {{A}} x \quad [ \langle \forall x: [ r. x ]: t. x \rangle ] \equiv \langle \forall x: [ r. x ]: [ t. x ] \rangle $$
It is referred to by "interchange" or "[] over V"; the [ ] around $r \times$ indicate that the range has to be a boolean scalar. Note the absence of "[] over 3".
The following two are known as "splitting the term".
$A \times \left\lbrack {\langle \forall x : r.x : s.x \land t.x}\right\rbrack \equiv$
$$ \langle \forall x: r. x: s. x \rangle \land \langle \forall x: r. x: t. x \rangle ] $$
$\left\lbrack {\langle \exists x : r.x : s.x \sim t.x}\right\rangle \equiv$
$$ \langle \exists x: r. x: s. x \rangle \vee \langle \exists x: r. x: t. x \rangle ] $$
and with trading we derive the two known as "splitting the range" - note that in both cases the range being split is a disjunction
[ \Leftrightarrow \left\lbrack {\langle \forall x : r.x \vee s.x : t.x}\right\rangle \equiv ]
$$ \langle \forall x: r. x: t. x \rangle \land \langle \forall x: s. x: t. x \rangle ] $$
[\left\lbrack {\langle \exists x : r.x \vee s.x : t.x}\right\rangle \equiv ]
$$ \langle \exists x: r. x: t. x \rangle \vee \langle \exists x: s. x: t. x \rangle ] $$
Important are the distributions known as " $v$ over $\forall$ " :
$$ \underline {{A x}} \quad [ q \vee \langle \forall x: r. x: t. x \rangle \equiv \langle \forall x: r. x: q \vee t. x \rangle ] $$
and as "w over 3
$\left\lbrack {9 \land \langle \exists x : r.x : t.x}\right\rangle = \langle \exists x : r.x : q \land t.x\rangle \rbrack$
Of the following theorems we prove the first
[[\left\langle {\forall x : \text{ false } : t.x}\right\rangle \equiv \text{ true }}]
[[\left\langle {3x : \text{ false } : t.x}\right\rangle \equiv \text{ false }}]
Proof We observe for any $t$
$$ \begin{array}{l} \langle \forall x: f a l s e: t. x \rangle \ = {\mathrm {t r a d i n g} } \ \langle \forall x: t r u e: f a l s e \Rightarrow t. x \rangle \ = {\text {p r e d i c a t e c a l c u l u s} } \ \langle \forall x: t r u e: t r u e \vee t. x \rangle \ = {\vee \mathrm {o v e r} \forall } \ t r u e \vee \langle \forall x: t r u e: t. x \rangle \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ t r u e. \ \end{array} $$
(End of Proof.)
The above two theorems deal with "empty ranges". For nonempty ranges - symbolized by $r.x \lor [x = y]$ - we have
[{\left\lbrack q \land \left\langle \forall x : r.x \vee \left\lbrack {x = y}\right\rbrack : t.x\right\rbrack \Rightarrow \right. }]
$$ \langle \forall x: r. x \vee [ x = y ]: q \wedge t. x \rangle ] $$
[ \Leftrightarrow \left\lbrack {9 \vee { \exists x : r \cdot x \vee \left\lbrack {x = y}\right\rbrack : t \cdot x}\right\rbrack \equiv ]
$$ \langle \exists x: r. x \vee [ x = y ]: q \vee f. x \rangle ] $$
They follow from the "1-point rule":
$\left\lbrack {\langle \forall x : \left\lbrack {x = y}\right\rbrack : t.x}\right\rangle \equiv t.y\rbrack$ [[\left{ {\exists x : \left\lbrack {x = y}\right\rbrack : t.x}\right} \equiv t.y]]
We shall prove the first, after establishing
$$ [ (\forall x: r. x \vee [ x = y ]: q) \geq q ] $$
Proof We observe
$$ \begin{array}{l} [ \langle \forall x: r. x \vee [ x = y ]: q \rangle \equiv q ] \ = {\text {s p l i t i n g t h e r a n g e} } \ [ \langle \forall x: r. x: q \rangle \land \langle \forall x: [ x = y ]: q \rangle \equiv q ] \ = {\text {1 - p o i n t r u l e} } \ [ \langle \forall x: r. x: q \rangle \land q \equiv q ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ 7 9 ^ {\prime} \vee \langle \forall x: r. x: q \rangle ] \ = {\vee \mathrm {o v e r} \forall } \ [ \langle \forall x: r. x: 7 9 \vee q \rangle ] \ = {\text {E x c l u d e d M i d d l e} } \ [ \langle \forall x: r. x: t r u e \rangle ] \ = {\mathrm {t r a d i n g} } \ [ \langle \forall x: f a l s e: \neg r. x \rangle ] \ = {\mathrm {e m p h y r a n g e} } \ t r u e \ \end{array} $$
(End of Proof of Lemma)
The first unproved theorem now follows:
$$ \begin{array}{l} q \land \langle \forall x: r. x \lor [ x = y ]: t. x \rangle \ = {\mathrm {a b o v e L e m m a} } \ \end{array} $$
$$ \begin{array}{l} \langle \forall x: r. x \vee [ x = y ]: q \rangle \land \langle \forall x: r. x \vee [ x = y ]: t. x \rangle \ = {\text {s p l i t t i n g t h e t e r m} } \ \langle \forall x: r. x \lor [ x = y ]: q \land b. x \rangle \ \end{array} $$
We have introduced the everywhere operator [ ] as a function from boolean structures to boolean scalars, and have used it all the time, without being very specific about its properties. We recall
$$ [ t r u e ] \equiv t r u e \qquad a n d \quad [ f a l s e ] \equiv f a l s e , $$
from which follows that the everywhere operator is idempotent:
[\left\lbrack {\left\lbrack x\right\rbrack }\right\rbrack \equiv \left\lbrack x\right\rbrack ]
We also conclude from the above
[ \Leftrightarrow \;{[x} \vee \left\lbrack y\right\rbrack \equiv \left\lbrack x\right\rbrack \vee \left\lbrack y\right\rbrack ]
which is not a very useful theorem in this
$$ [ x ] \Rightarrow [ y ] \equiv [ [ x ] \Rightarrow y ] $$
A function that for any scalar range distributes over universal quantification, i.e. an $f$ for which for any scalar range
$$ [ f. \langle \forall x:: x \rangle \equiv \langle \forall x:: f. x \rangle ] $$
holds, is called "universally conjunctive". (If it distributes for any scalar range over existential
quantrification, i.e.
$$ [ f. \langle \exists x:: x \rangle \equiv \langle \exists x:: f. x \rangle ] \quad , $$
it is said to be "universally disjunctive".
Boolean structures are also called "predicates" and functions from predicates to predicates -like the above $f-$ are known as "predicate transformers - Monotonicity of predicate transformers is defined by
$$ \begin{array}{l} {(f \mathrm {i s m o n o t o n i c}) \equiv} \ {\langle \forall x, y: [ x \Rightarrow y ] \Rightarrow [ f. x \Rightarrow f. y ] \rangle} \end{array} $$
and the connection with the above is that a (con- or dis-)junctive function is monotonic. We shall show this for a function $f$ that distributes over conjunction. We observe for
any
$$ \begin{array}{r l} & {\left[ f. x \Rightarrow f. y \right]} \ {=} & {{\text {p r e d i c a t e c a l c u l u s} }} \ & {\left[ f. x \wedge f. y \equiv f. x \right]} \ {=} & {{\text {f d i s t r i b u t e s o v e r} \wedge} \ & {\left[ f. (x \wedge y) \equiv f. x \right]} \ {=} & {{\text {L e i b n i z} }} \ & {\left[ x \wedge y \equiv x \right]} \ {=} & {{\text {p r e d i c a t e c a l c u l u s} }} \ & {\left[ x \Rightarrow y \right].} \end{array} $$
Since a universally conjunctive function distributes over $\land$ , and $[ ]$ is universally
conjunctive, we conclude
[\left\lbrack {x \land y}\right\rbrack \equiv \left\lbrack x\right\rbrack \land \left\lbrack y\right\rbrack ]
from which the monotonicity now follows
[\left\lbrack {x \Rightarrow y}\right\rbrack \Rightarrow \left( {\left\lbrack x\right\rbrack \Rightarrow \left\lbrack y\right\rbrack }\right) \quad .]
Remark Of the two ways of rewriting an equivalence
$$ \begin{array}{l} [ x \equiv y \equiv (x \Rightarrow y) \land (x \Leftarrow y) ] \qquad a n d \ [ x \equiv y \equiv (x \wedge y) \vee (7 x \wedge 7 y) ] \quad , \ \end{array} $$
the former - known as "mutual implication". is much more popular than the latter. The explanation is to be found in the distributive properties of [], which yield
$$ [ x \equiv y ] \equiv [ x \Rightarrow y ] \wedge [ x \Leftarrow y ] \quad , $$
i.e. mutual implication translates a proof obligation of the form $[x = y]$ to two indep- pent proof obligations, while rewriting with
$$ [ x \equiv y ] \equiv [ (x \wedge y) \vee (1 x \wedge 1 y) ] $$
does not yield such disentanglement. (End of Remark.)
In view of the monotonicity of [ ] the rule of Leibniz
$$ [ x \equiv y ] \Rightarrow [ f. x = f. y ] $$
follows from
$$ [ (x \equiv y) \Rightarrow (\not {p} x \equiv \not {p} y) ] \quad ; $$
a function $f$ satisfying for any $x, y$ the latter stronger relation is called a "punctual function". Since
$$ [ (x \equiv y) \Rightarrow (\rho_ {x} \equiv \rho_ {y}) ] $$
$= \left{ {{pedi}{cate}\;{calculus}}\right}$
$$ [ (x \equiv y) \wedge (f x \equiv f \cdot y) \equiv (x \equiv y) ] $$
$= \left{ \begin{array}{l} \text{predicate calculus: } \land \text{ and } \equiv } \end{array}\right.$
$$ [ (x \equiv y) \land f. x \equiv (x \equiv y) \land f. y ] $$
an alternative definition of punctuality is
$$ \begin{array}{l} {(f \mathrm {i s p u n c t u a l}) \equiv} \ {\langle \forall x, y: [ (x \equiv y) \land f. x \equiv (x \equiv y) \land f. y ] \rangle .} \end{array} $$
We are now ready to demonstrate that expressions formed from variables with the logical operators and quantification are punctual functions of the variables. Since negation and existential quantification - which includes disjunction - suffice to write down the expressions, it suffices to show that
(i) the identity function is punctual (ii) the negation of a punctual function is punctual (iii) an existential quantification over punctual
functions is punctual
Proof For (i) we observe $\left\lbrack {\left( {x \equiv y}\right) \Rightarrow \left( {x \equiv y}\right) }\right\rbrack$ .
For (ii) we observe
$$ [ (x \equiv y) \Rightarrow (p _ {x} \equiv p _ {y}) ] \equiv [ (x \equiv y) \Rightarrow (p _ {x} \equiv p _ {y}) ] $$
For (iii) we observe - with $f$ ranging over some set of punctual functions
$$ \begin{array}{l} (x \equiv y) \land \langle \exists f: f _ {x} \rangle \ = {\wedge o v e r \exists } \ \langle \exists f: (x = y) \land f \cdot x \rangle \ = {f \text {i s p u n c t u a l} } \ \langle \exists p: (x = y) \land f. g \rangle \ = {\wedge o v e r ] } \ (x \equiv y) \land \langle \exists p: f. y \rangle \ \end{array} $$
(End of Proof.)
By way of illustration of the use of punctuality we now give another proof of the transitivity of the implication. We observe for any $x,y,z$
$$ \begin{array}{l} (x \Rightarrow y) \land (y \Rightarrow z) \land (x \Rightarrow z) \ = {\text {p r e d i c a t e c a l c u l u s} } \ (x \wedge y \equiv x) \wedge (y \wedge z \equiv y) \wedge (x \wedge z \equiv x) \ = {x \wedge z \equiv x i s a p u n c t u a l f u n c t i o n o f x } \ (x \wedge y \equiv x) \wedge (y \wedge z \equiv y) \wedge (x \wedge y \wedge z \equiv x \wedge y) \ = {x \wedge (y \wedge z) \equiv x \wedge y i s a p u n c t u a l f u n c h i o n \ o f (y \wedge z) } \ (x \wedge y \equiv x) \wedge (y \wedge z \equiv y) \wedge (x \wedge y \equiv x \wedge y) \ = {\text {p r e d i c a t e c a l c u l u s} } \ (x \Rightarrow y) \land (y \Rightarrow z), \ \end{array} $$
$$ h e n c e (x \Rightarrow y) \land (y \Rightarrow z) \Rightarrow (x \Rightarrow z) $$
*
The "galois connection" is a property than an ordered pair of predicate transformers may enjoy. For the ordered pair $\left( {p,g}\right)$ ,this state of affairs is denoted by gal.(p,g),which is defined by
$$ g a l. (f, g) \equiv \langle \forall x, y: [ f. x \Rightarrow y ] \equiv [ x \Rightarrow g. y ] \rangle . $$
The central theorem about the Galois connection states that the following 3 assertions are equivalent:
(i) $\operatorname{gal}\left( {\rho ,g}\right)$ (ii) $f$ is universally $\left{ \begin{array}{l} \text{disjunctive and} \ \end{array}\right.$ $\left\lbrack {g \cdot y \equiv \langle \exists x : \left\lbrack {f \cdot x \Rightarrow y}\right\rbrack : x\rbrack }\right\rbrack$ for all $y$ (iii) $g$ is universally conjunctive and $\left\lbrack {f \cdot x \equiv \langle \forall y : \left\lbrack x \Rightarrow g \cdot y\right\rbrack : y}\right\rbrack$ for all $x$ .
Proof The proof of (i) $\equiv$ (ii) is left to the reader; we prove (i) $\equiv$ (iii) by mutual implication.
$$ (i) \Rightarrow (i i i) $$
The universal conjunctivity of $g$ states that for any scalar range of $y$
$$ [ g. \langle \forall y: y \rangle \equiv \langle \forall y: g. y \rangle ] \quad ; $$
this will be demonstrated by showing that for any $x$ $\left\lbrack {x \Rightarrow g. < {\forall y} : y}\right\rbrack \equiv \left\lbrack {x \Rightarrow {\left\langle {\forall y} : y\right\rangle }}\right\rbrack$ .
To this end we observe, using gal. (p,g)
$$ \begin{array}{l} [ x \Rightarrow g. \langle \forall y: y \rangle ] \ = {g a l. (p, g) } \ [ f. x \Rightarrow \langle \forall y: y \rangle ] \ = {\mathrm {p r e d . c a l c .}: \vee \mathrm {o v e r} \forall } \ [ \langle \forall y: f. x \Rightarrow y \rangle ] \ = {\left[ \begin{array}{l l} \end{array} \right] o v e r \forall } \ \langle \forall y: [ p x \Rightarrow y ] \rangle \ = {g a l. (f, g) } \ \langle \forall y: [ x \Rightarrow g \cdot y ] \rangle \ = {\left[ \right] \mathrm {o v e r} \forall } \ [ \langle \forall y: x \Rightarrow g, y \rangle ] \ = {\vee o v e r \forall } \ [ x \Rightarrow \langle \forall y: g. y \rangle ] \ \end{array} $$
In order to prove the second conjunct of (iii), using $\operatorname{gal}\left( {f,g}\right)$ ,we observe for any $x$
$$ \begin{array}{l} \langle \forall y: [ x \Rightarrow g. y ]: y \rangle \ = {g a l. (f, g) } \ \langle \forall y: [ f. x \Rightarrow y ]: y \rangle \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ p. x \ \end{array} $$
$$ (i) \Leftarrow (i i i) $$
$$ U s i n g (i i i), w e s h o w $$
$$ [ f. x \Rightarrow y ] \equiv [ x \Rightarrow g. y ] \quad \mathrm {f o r a l l} x, y $$
by mutual implication.
LHS
$$ \begin{array}{l} \langle \forall x, y: [ f. x \Rightarrow y ] \Leftarrow [ x \Rightarrow g. y ] \rangle \ = {\mathrm {n e s t i n g}, \mathrm {t r a d i n g} } \ \langle \forall x: \cdot \cdot \cdot \langle \forall y: [ x \Rightarrow g \cdot y ]: [ f. x \Rightarrow y ] \rangle \rangle \ = {\text {p r e d . c a l c .} } \ \langle \forall x: [ f. x \Rightarrow \langle \forall y: [ x \Rightarrow g. y ]: y \rangle ] \rangle \ = {(i i i), 2 n d c o n j u n c t } \ \langle \forall x: [ f. x \Rightarrow p. x ] \rangle \ = \begin{array}{l} {{\mathrm {p r e d . c a l c} }} \ {\mathrm {t r u e}} \end{array} \ \end{array} $$
[\text{LHS} \Rightarrow \text{RHS}]
We observe for any $x,y$
$$ \begin{array}{l} [ f. x \Rightarrow y ] \ \Rightarrow \left{ \begin{array}{l l} {(i i i), 1 s t c o n j u n c t, h e n c e g i s m o n o t o n i c} \ {[ g. (f. x) \Rightarrow g. y ]} \end{array} \right} \ = {(i i i), 2 n d c o n j u n c t } \ [ g. \langle \forall y: [ x \Rightarrow g. y ]; \breve {y} \rangle , \Rightarrow g. \breve {y} ] \ = {(i i i), 1 s t c o n j u n c t } \ [ \langle \forall y: [ x \Rightarrow g, y ]: g, y \rangle \Rightarrow g, y ] \ \Rightarrow \quad {\mathrm {p r e d . c a l c} } \ [ x ^ {\prime} \Rightarrow g \cdot y ] \ \end{array} $$
(End Proof.)
Exercise Let $\operatorname{gal}\left( {p,g}\right)$ . Show
(i) fog and gof are monotonic - with $0$
$$ \begin{array}{l} w e d e n o t e f u n c h i o n a l c o m p o s i t i o n: [ (p _ {0} g). y \equiv f. (g. y) ] \ \mathrm {(i i)} \quad \mathrm {f o g i s s t r e n g t h e n i n g a n d g o f i s w e a k e n i n g} \ \end{array} $$
$$ \begin{array}{l} {- i. e. \left[ (\mathrm {f o g}) _ {.} y \Rightarrow y \right] a n d \left[ (\mathrm {g o f}) _ {.} x \Leftarrow x \right] -} \ {\mathrm {(i i i)} \quad \mathrm {f o g} \quad a n d \quad \mathrm {g o f} \quad a r e \quad i d e m p o t e n t - i. e.} \ {\left[ (\mathrm {f o g} _ {\cdot} \mathrm {f o g}) _ {.} y \equiv (\mathrm {f o g}) _ {.} y \right] a n d \left[ (\mathrm {g o f} _ {\cdot} \mathrm {g o f}) _ {.} x \equiv (\mathrm {g o f}) _ {.} x \right]} \ {\mathrm {(A c h u a l l y} \quad (\mathrm {f o g o f}) = \mathrm {f}, \mathrm {f r o m w h i c h}} \ {\mathrm {b o t h i d e m p o t e n c e s f o l l o w .) (E n d o f E x e r c i s e .)}} \end{array} $$
The relational calculus emerges from the predicate calculus by extending the latter with two operators and a constant. In the context of the relational calculus, the predicates are usually called "relations".
The first additional operator is the unary "transposition". It is denoted by the prefix "~" - pronounced: "tilde", which is given the same syntactic binding power as the negation.
The second additional operator is the binary "composition". It is denoted by the infix ";" - pronounced: "semi"-, which is given a binding power between the binary logical operators and the unary operators.
The constant is denoted by $J$ ; it will emerge as the identity element of the composition.
Though the axioms defining the new operators
are few, the relational calculus has a much richer structure than the predicate calculus, a major difference being that, in contrast to the logical operators, the two relational operators yield expressions that are not punctual functions of their arguments.
By postulate the transposition satisfies $\underline{Ax}\quad \left\lbrack {\sim x \Rightarrow y}\right\rbrack \equiv \left\lbrack {x \Rightarrow {\sim y}}\right\rbrack$ for all $x,y$ . A shorter formulation would have been: gal. $\left( {n,\sim }\right)$ . In any case we can conclude:
\~ is universally conjunctive and disjunctive, hence [true true] and [false false] and \~ is monotonic; \~ is an involution - i.e. $[\sim x \equiv x]$ for all $x$ - because (see Exercise) \~ is both weakening and strengthening.
Next we show that negation and transposition distribute over each other, i.e.
$$ \ln [ \sim 7 x \equiv \sim x ] $$
Proof The proof is by mutual implication. We ob
$$ \begin{array}{r l r} {[ \sim 7 x \Rightarrow 7 \sim x ]} & & {\mid [ \sim 7 x \Leftarrow 7 \sim x ]} \ {= {\mathrm {p r e d . c a l c .} }} & & {\mid = {\mathrm {p r e d . c a l c .} }} \end{array} $$
$$ \begin{array}{r l} {[ \sim \neg x \land \sim x \Rightarrow \mathrm {f a l s e} ].} & {[ \sim \neg x \lor \sim x \Leftarrow \mathrm {t r u e} ]} \ {=} & {{\sim \mathrm {o v e r} \land , \mathrm {f o r} \sim} \ & {\mathrm {i s c o n j u n c t i v e} }} \ {[ \sim (\neg x \land x) \Rightarrow \mathrm {f a l s e} ]} & {[ \sim (\neg x \lor x) \Leftarrow \mathrm {t r u e} ]} \ {=} & {{\mathrm {p r e d . c a l c .} }} \ {[ \sim f a l s e \Rightarrow f a l s e ]} & {[ \sim \mathrm {t r u e} \Leftarrow \mathrm {t r u e} ]} \ {=} & {{\mathrm {r e l . c a l c .} }} \ & {\mathrm {t r u e}} \end{array} $$
(End of Proof.)
As quantification and negation suffice for all other logical operators we conclude
Th. Transposition distributes over all logical operators.
$$ \mathrm {T h} [ x ] \equiv [ \sim x ] $$
$$ \begin{array}{l} \mathrm {P r o o f} \quad \mathrm {W e o b s e r v e} \quad \mathrm {f o r a n y} \quad x \ [ x ] \ = {\text {p r e d . c a l c .} } \ [ t r u e \Rightarrow x ] \ = {\text {r e l . c a l c .} } \ [ \sim t r u e \Rightarrow x ] \ = {g a l. (n, n) } \ [ t r u e \Rightarrow \sim x ] \ = {\mathrm {p r e d . c a l c .} } \ [ \sim x ] \ \end{array} $$
(End of Proof.)
One axiom deals with composition only:
A* composition is associative, i.e.
$$ [ (x; y); z \equiv x; (y; z) ] $$
The associativity is the main justification for introducing an infix operator to denote com- position. We shall exploit the associativity (as usual) implicitly by omission of parentheses.
The next axiom deals with a right-identity element of composition:
$\left\lbrack {x;j \equiv x}\right\rbrack$
The last axiom postulates what is known as the "right-exchange":
$\underline{A \times }$ $\left\lbrack {x;y \Rightarrow z}\right\rbrack = \left\lbrack {\sim x;\neg z \Rightarrow {\neg y}}\right\rbrack$
(The way to memorize this to observe that it is a combination of taking the contrapositive (as far as $y$ and $z$ are concerned) and transposing the prefix $x$ of the antecedent.)
We now observe for any $x, y, z$
$$ \begin{array}{l} [ \sim (x; y) \Rightarrow z ] \ = {J ^ {s} i s r i g h t - i d e n t i t y f o r; J \ [ \sim (x; y); ] \Rightarrow z ] \ = {\mathrm {r i g h t - e x c h a n g e}; \mathrm {a s s o c i a t i v i l y} } \ [ x; y; 7 z \Rightarrow 7 ] \ \end{array} $$
$$ \begin{array}{l} = {\mathrm {a s s o c i a t i v i t y}; \mathrm {r i g h t - e x c h a n g e} } \ [ \sim x; J \Rightarrow \neg (y; \neg z) ] \ = {J \mathrm {i s r i g h t - i d e n t i f y} } \ [ \sim x \Rightarrow 7 (y; 7 2) ] \ = {\mathrm {c o n t r a p o s i t i v e} } \ [ y; 7 2 \Rightarrow 7 \sim x ] \ = {\mathrm {r i g h t - e x c h a n g e} } \ [ \sim y; \sim x \Rightarrow z ] \ \end{array} $$
and since the equivalence of first and last term holds for all $z$ ,we have proved our
[\left\lbrack {\sim \left( {x;y}\right) \equiv {\sim }_{y};\sim x}\right\rbrack ]
Remark Note how 5 of the above 6 steps are un- avoidable: 2 appeals to the right-identity element, viz. one to introduce J and one to eliminate J again, and 3 appeals to the right-exchange, our only tool to introduce or eliminate a tilde. (End of Remark.)
Next we observe for any $x$
$$ \begin{array}{l} \begin{array}{r l} & {\mathrm {t r u e}} \ {=} & {{\left. \right] \mathrm {r i g h t - i d e n t i t y} }} \ & {\left[ \sim x; \right] \equiv \sim x ]} \end{array} \ \Rightarrow \begin{array}{r l} & {{\mathrm {L e i b n i z} }} \ & {[ \sim (\sim x; ]) \equiv \sim \sim x ]} \end{array} \ = {\mathrm {r e l . c a l c .} } [ \sim ]; x \equiv x ] \ \end{array} $$
and from this we conclude that $\sim J$ is a left-identity element of composition. Now
$\left\lbrack j \equiv \sim J\right\rbrack$
immediately follows. We leave to the reader to derive from " $\sim$ over ; " and the right-exchange
[\left\lbrack {x;y \Rightarrow z}\right\rbrack \equiv \left\lbrack {{72};y \Rightarrow {7x}}\right\rbrack ]
known as the "left-exchange".
From the exchange rules and the theory of the Galois connection we now derive that
In Composition is universally disjunctive in both operands
In view of the theory of the Galois connection we can conclude that, for all $z$ , $x; z$ is universally disjunctive in its first argument, if we can establish
$$ [ x; z \Rightarrow y ] \equiv [ x \Rightarrow s o m e t h i n g ] f o r a l l x, y, z $$
where the "something" (which plays the role of " $g.y^{\prime \prime }$ ) does not depend on $x$ . The left-
$$ \begin{array}{l} [ x; z \Rightarrow y ] \ = {\mathrm {l e f t - e x c h a n g e} } \ [ \pi y; \sim 2 \Rightarrow 7 x ] \ = {\mathrm {c o n t r a p o s i t i v e} } \ [ x \Rightarrow \neg (\neg y; \sim z) ] \ \end{array} $$
Similarly, the right-exchange establishes composition's universal disjunctivity in its right operand.
From its disjunctivity follows that composition is monotonic in both its arguments. From that and the existence of $J$ , the reader may conclude
$\left{ \begin{array}{ll} {10} & \left\lbrack {x \Rightarrow {x}_{;}\text{ true }}\right\rbrack \ & \text{ and }\left\lbrack {x \Rightarrow \text{ true };x}\right\rbrack \end{array}\right. ,$
from which
[\left\lbrack \text{true};\text{true} \equiv \text{true}\right\rbrack ]
immediately follows.
Remark Hence, postfixing a relation with ";true" or prefixing it with "true;" is what is known as a closure: a monotonic, weakening, and idem-potent operator. (End of Remark.)
If the implication in the other direction holds, there is something special with the relation, which is recognized by the introduction of special terminology:
(p is a left-condition) $\equiv$ [p;true $\Rightarrow$ p]
(q is a right-condition) [true; q ⇒ q]
Note that any left-condition $p$ can be written as $x;$ true for some $x$ (for instance $p$ ).
The notions of left- and right-conditions are
closely related to the last axiom of the rela- tional calculus (to which J. C.P.S. van der Woude gave the name "Cone Rule"). In one of its for- mulations it is
A $x$ For left-condition $p$ and right-condition $q$
$$ [ p \vee q ] \Rightarrow [ p ] \vee [ q ] $$
(Note that the inverse implication holds for un- restricted $p,q$ because [] is monotonic.)
The Cone Rule is of importance because, without it, a satisfactory model of the relational calculus, is obtained by taking
- the identity function for the conjunction for [\text{true}]
Hence, if a lemma of the relational calculus is invalidated by the above substitution, its proof requires the Cone Rule. Conversely, that part of the relational calculus that can be derived without the Cone Rule is a true generalization of the predicate calculus. My experience with the relational calculus is undoubtedly incomplete and one-sided, but I think that, so far, I had no use for the Cone Rule. And that, of course, is very gratifying.
left- and right-conditions emerge quite naturally from considering the standard model of the rela
fitional calculus: there a relation is modelled by a boolean function defined on the Cartesian square of some space, left- and right- conditions are modelled by either a boolean function on that (single) space or, more accurately, as a relation that does not depend on one of its two arguments. It is the mixture of boolean functions of 1 and of 2 arguments that has introduced the conditions into the relational calculus.
In the following we shall only formulate a theorem for left-conditions if a similar one holds for right-conditions. The similarity follows from
$\left( {p\text{is a left-condition}}\right) \equiv \left( {{wp}\text{is a right-condition}}\right) .$
Important for the identification between left- conditions and boolean functions on the single space is the following
The Expressions built from left-conditions and logical operators are left-conditions.
Proof By induction over the syntax it suffices to show this for negation and existential quantification, as all logical operators and constants can be expressed in those two. Our obligations are therefore:
(i) for all $p$ ( $p$ is a left-condition) $\Rightarrow \left( {7p\text{is a left-condition}}\right)$
(ii) for $p$ ranging over a bag of relations
$$ \begin{array}{l} \langle \forall p: p \mathrm {i s a l e f t - c o n d i t i o n} \rangle \Rightarrow (\langle \exists p: p \mathrm {i s a l e f t - c o n d i t i o n} \rangle) \ \mathrm {P r o o f} _ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - \ (7 p i s a l e f t - c o n d i t i o n) \ = {\mathrm {d e f} }. \ [ \neg p; \mathrm {t r u e} \Rightarrow \neg p ] \ = {\mathrm {l e f t - e x c h a n g e} } \ [ p; \sim t r u e \Rightarrow p ] \ = {\left[ \sim t r u e \equiv t r u e \right] } \ [ p; \mathrm {t r u e} \Rightarrow p ] \ = \quad {d e f? } \ (p \mathrm {i s a l e f t - c o n d i t i o n}) \ \mathrm {P r o o f} _ {-} \mathrm {o f} _ {(i i)} \ (\langle \exists p: p \rangle i s a l e f t - c o n d i t i o n) \ = {\mathrm {d e f} \rho } \ [ \langle \exists p:: p \rangle ; t r u e \Rightarrow \langle \exists p:: p \rangle ] \ = {\quad ; \quad u n i v e r s a l l y \quad d i s j u n c h i v e } \ [ < \exists p: p; t r u e > \Rightarrow < \exists p: p > ] \ \Leftrightarrow {\exists i s m o n o t o n i c } \ \langle \forall p: [ p; t r u e \Rightarrow p ] \rangle \ = {\mathrm {d e p} } \ \langle \forall p: p i s a l e f t - c o n d i t i o n \rangle \ \end{array} $$
End of Proof.
[\frac{1}{4}\left( {x + y}\right) + \cdots + \frac{17}{4} + \frac{17}{4} + {17}]
$\left\lbrack {\left( {x \vee \sim x}\right) ;z \Rightarrow z}\right\rbrack \Rightarrow \left\lbrack {x;y \land z \equiv x;\left( {y \land z}\right) }\right\rbrack$ (ii) $\left\lbrack {x;(z \vee z) \Rightarrow x}\right\rbrack \Rightarrow \left\lbrack {x \land {y}{i}z \equiv {\left( x \land y\right) }{i}z}\right\rbrack$
Proof We only prove (ii); by transposition, (i) then follows. We are going to establish the right-hand side by mutual implication, collecting the needed conditions as we go along.
For showing $[x\wedge y;2\Leftarrow (x\wedge y);z]$ we observe
$$ (x \wedge y); z $$
$\Rightarrow$ {monotonicity of ;3}
$$ x; z \land y; z $$
$\Rightarrow \;\left{ {{\operatorname{condition}A : \left\lbrack {x;z \Rightarrow x}\right\rbrack }}\right}$
$$ x \wedge y; z $$
For showing $\left\lbrack {x \land y;2 \Rightarrow \left( {x \land y}\right) ;z}\right\rbrack$ ,we show the equivalent $\left\lbrack {y;2 \Rightarrow {7x} \vee \left( {x \land y}\right) ;z}\right\rbrack$ by observing
$$ \therefore x \vee (x \wedge y); z $$
$\Leftrightarrow \left{ {{\operatorname{condition}}^{y}B : \left\lbrack {{7x};z \Rightarrow {7x}}\right\rbrack }\right}$
$$ \lnot x; z \lor (x \land y); z $$
$$ = {\quad ; \quad o v e r \quad v } $$
$$ (1 x \vee (x \wedge y)); z $$
$$ = {\mathrm {p r e d . c a l c .} } $$
$$ (1 x \vee y); z $$
[\left{ \begin{array}{l} \text{monotonicity of }; \ \end{array}\right. ]
$$ y; z $$
Turning our attention to the conditions, we observe
A
$$ \begin{array}{l} = {\text {d e f i n i t i o n s} } \ [ x; z \Rightarrow x ] \land [ \neg x; z \Rightarrow \neg x ] \ = {\mathrm {l e f t - e x c h a n g e} } \ [ x; z \Rightarrow x ] \land [ x; \sim z \Rightarrow x ] \ = {\mathrm {p r e d . c a l c .} } \ [ x; z \vee x; \sim z \Rightarrow x ] \ = {\quad ; \text {o v e r} v } \ [ x; (z \vee \sim z) \Rightarrow x ] \ \end{array} $$
and this concludes the proof.
(End of Proposition)
In the standard model of the relational calculus, the relational variables in the above range over boolean functions of 2 variables of the same type. We will denote the boolean function corresponding to the relational expression $x$ by an infix $(x)$ . The relational calculus is then modelled by
$$ \begin{array}{l} p (x) q \equiv \neg p (x) q \ p (x \vee y) q \equiv p (x) q \vee p (y) q \ p (x \wedge y) q \equiv p (x) q \wedge p (y) q \ p (x \equiv y) q = p (x) q = p (y) q \ p (x \Rightarrow y) q = p (x) q \Rightarrow p (y) q \ p (\sim x) q \equiv q (x) p \ p (x; y) q = \langle \exists r: p (x) r \land r (y) q \rangle \ p (j) q \equiv p = q \ \end{array} $$
The verification that this model satisfies all the axioms of the relational calculus is left as an exercise for the reader. These axioms, we repeat, are
(i) “;” is universally disjunctive in both arguments (ii) “;” is associative. (iii) $\forall 3,\forall 4$ has an identity element called $J$ (iv) ~ is a monotonic involution $\left\lbrack {x,y \Rightarrow {7z}}\right\rbrack \equiv \left\lbrack {{nx};z \Rightarrow {7y}}\right\rbrack$ for all $x,y,z$ (vi) $\left\lbrack {x;\text{true}v\text{true};y}\right\rbrack \Rightarrow \left\lbrack {x;\text{true}}\right\rbrack \vee \left\lbrack {\text{true};y}\right\rbrack$ for all $x,y$ (or,alternatively,A.Tarski's
formulation of the cone Rule:
$$ [ x; \mathrm {t r u e} ] \vee^ {\prime} [ \mathrm {t r u e}; \neg x ] \quad \mathrm {(f o r a l l} x) $$
We shall now show how an alternative model is provided by the regularity calculus (also known as the calculus of regular expressions).
We interpret predicates as boolean-valued functions over some non-empty set $S$ ,and "everywhere"as universal quantification over $S$ :
$$ [ x ] \equiv \langle \forall s: s \in S: x. s \rangle $$
In the regularity calculus $s$ is the set of finite strings of symbols from some alphabet. With variables $r,s,$ and $t$ ranging over $S$ the composition $(i, j)$ is given by
$$ (x; y). r \equiv \langle \exists s, t: r = s + t: x. s \wedge y. t \rangle \quad \mathrm {f o r a l l} r \in S. $$
where $t$ usually denotes concatenation. From the above definition of "；" in terms of "t" follows
is universally disjunctive in both arguments - "；" is associative $\Leftrightarrow {}^{\prime \prime } + {t}^{\prime \prime }$ is associative - “;” has a right-identity $\Leftrightarrow {}^{6} + {}^{n}$ has a right-identity
Since concatenation is associative and has a right-identity, viz. $\varepsilon$ , the empty string, our composition with for $+$ the concatenation satisfies (i),(ii),(iii). Furthermore “ $J$ ” is modelled by
$$ J. r \equiv r = \varepsilon \quad \mathrm {f o r a l l} r \in S. $$
and this
$$ [ J \Rightarrow x ] \equiv 7 [ J \Rightarrow 7 x ] \quad f o r a l l x $$
(Later we shall formulate this as: "in the regularity calculus, $y$ is a point-predicate".)
We shall now show that this model satisfies the Cone Rule (vi), in Tarski's form:
$$ \begin{array}{l} [ x; t r u e ] \vee [ t r u e; 7 x ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ t r u e ^ {\prime} \Rightarrow x; t r u e ] v [ t r u e \Rightarrow f r u e; 7 x ] \ = {y i s i d e n t i t y e l e m e n t o f c o m p o s i t i o n s } \ [ ]; t r u e \Rightarrow x; t r u e ] \vee [ t r u e; ] \Rightarrow t r u e; 7 x ] \ \Leftarrow \quad {; i s d i s j u n c t i v e, h e n c e m o m o t h u n i c } \ \end{array} $$
$$ [ j \Rightarrow x ] \lor [ j \Rightarrow 2 x ] $$
$$ \begin{array}{l} \Leftrightarrow \quad {\text {p i e d . c a l c .} } \ [ j \Rightarrow x ] \equiv \neg [ j \Rightarrow \neg x ] \ = {\mathrm {t h i s} } \mathrm {i s a p o i n t - p r e d i c a t e} } \ \end{array} $$
The problem lies with (iv) and (v), which mention the $\sim$ , which does not occur in the regularity calculus. Our task is to invent a $\sim$ (and, in the process, to extend the notion of concatenation) so that (iv) and (v) are met.
A way to assure that is a monotonic involution is to define
$$ [ \sim x \equiv (x \circ i n v) ] $$
where $\operatorname{inv}$ is some involution from $S$ to $S$ .
Proof To show that $\sim$ is an involution,we observe for any $x$
$$ \sim (\sim x) $$
$$ = {\mathrm {d e f . o f} \sim } $$
$$ (x \circ i n v) \circ i n v $$
$$ = {0 i s a s s o c i a t i v e } $$
$$ x \circ (\operatorname {i n v} \circ \operatorname {i n v}) $$
$$ = {\text {i n v i s a n i n v o l u t i o n} } $$
$$ \times $$
To show monotonicity, i.e. $\left\lbrack {x \Rightarrow y}\right\rbrack \Rightarrow \left\lbrack {{\sim x} \Rightarrow {\sim y}}\right\rbrack$ we observe
$$ \begin{array}{l} [ \sim x \Rightarrow \sim y ] \ = {\mathrm {d e f} o p [ ] a n d \sim } \ \langle \forall s: s \in S: x. (i n v. s) \Rightarrow y. (i n v. s) \rangle \ = {\mathrm {t r a n s f o r m i n g t h e d u m m y : i n v h a s a n i n v e r s e} } \ \langle \forall t: t \in S: x. t \Rightarrow y. t \rangle \ = {\mathrm {d e f . o p} [ ] } \ [ x \Rightarrow y ] \ \end{array} $$
$$ (\mathrm {E n d o f P r o o f .}) $$
We now turn our attention to (v) in order to derive the proper constraint on inv. We first investigate the expression of $\left\lbrack {x;y \Rightarrow {72}}\right\rbrack$ in terms of our model
$$ \begin{array}{l} [ x; y \Rightarrow 7 2 ] \ = {\mathrm {m o d e l} [ ] \mathrm {a n d} \mathrm {o f}; } \ \langle \forall r: \langle \exists s, t: r = s + t: x. s \wedge y. t \rangle \Rightarrow \neg z. r \rangle \ = {\text {p r e d i c a t e c a l c u l u s} } \ \langle \forall r, s, t: r = s + t: r (x. s \wedge y. t \wedge z. r) \rangle \quad (*) \ \end{array} $$
Thus
$$ [ \sim x; z \Rightarrow \neg y ] $$
$$ \begin{array}{l} = {\text {a b o w e} \quad \text {r e s u l t}; (\sim x). s \equiv x. (\text {i n v . s}) } \ \langle \forall r, s, t: r = s + t: 7 (x. (i n v. s) \land z. t \land y. r) \rangle \ = {\text {c h a n g i n g d l u m m i e s}: r, s, t := t, \text {i n v . s}, r } \ \langle \forall r, s, t: t = i n v. s # r: \neg (x. s \land y. t \land z. r) \rangle \quad () \ \end{array} $$
We satisfy (v) by seeing to it that $()\equiv (x)$ an equivalence that follows from equivalence of the ranges:
$$ r = s + t \equiv t = i n v. s + r $$
By substitutions $r \mathrel{\text{:=}} \varepsilon$ and $t \mathrel{\text{:=}} \varepsilon$ ,respectively, we derive
$$ \varepsilon = s + \operatorname {i n v}. s \quad \mathrm {a n d} \quad \varepsilon = \operatorname {i n v}. s + s. $$
Instead of considering all finite strings of symbols from some alphabet A, we consider a larger set of strings, composed from an alphabet twice as big. Each original letter of alphabet A is introduced in two versions -black and white, say-. Our new S is the set of all finite strings of symbols from the duplicated alphabet such that the two versions of a letter from the single alphabet don't occur next to each other. In the concatenation process, the two versions of the same symbol from the original alphabet annihilate each other; this annihilation does not destroy concatenation's assocativity, nor the existence of an identity element. The operation inv is the combination of two commuting operation: reversing the string and inverting the colour of each symbol, and the functional composition of two commuting inversions is again, an inversion. Since the standard regularity calculus does not use the negation, it is a subsystem in which we only need to distinguish between strings of symbols of one colour. The standard regularity calculus does use a star:"*"; $x^{*}$ denotes the strongest solution of the equation (in y) $\mathbf{y}:\left[y\equiv \mathbf{\mu}\right]\mathbf{v}\mathbf{x};\mathbf{y}]$
Intermezzo By way of illustration we show the
equivalence of the two formulations of the Cone Rule:
$\left\lbrack {x;\operatorname{true}v\operatorname{true};y}\right\rbrack \Rightarrow \left\lbrack {x;\operatorname{true}}\right\rbrack \vee \left\lbrack {\operatorname{true};y}\right\rbrack$
$$ () \quad [ x; t r u e ] \vee [ t r u e; 7 x ] $$
$\left( \right) \Rightarrow \left( { * }\right)$ We observe for any $x$
$$ [ x; t r u e ] \vee [ t r u e; 7 x ] $$
$\Leftrightarrow \;\left{ {\left( x\right) \text{ with }y = x}\right}$
$$ [ x; \mathrm {t r u e} \lor \mathrm {t r u e}; 7 x ] $$
$\Leftrightarrow {$ monotonicity of
$$ [ x; ] \vee [ j; 7 x ] $$
$= { J$ is identity of $p;}$
$$ [ x \vee \neg x ] $$
$= {$ pred. calc}
$$ t r u e $$
$\left( \right) \Leftarrow \left( { * }\right) \;$ We observe for any $x,y$
$$ [ x; t r u e \lor t r u e; y ] $$
pred. calc.
$$ [ \neg (x; t r u e) \Rightarrow t r u e; y ] $$
$\Rightarrow {$ monotonicity of
$$ [ t r u e; \neg (x; t r u e) \Rightarrow t r u e; t r u e; y ] $$
$= \left{ {\left\lbrack \text{true};\text{ true } \equiv \text{ true }\right\rbrack \left( {\text{twice}}\right) \text{ and }\left( {xx}\right) \text{ with }x : y = x;}\right.$
$$ [ t r u e; \neg (x; t r u e) \Rightarrow t r u e; y ] \land ([ x; t r u e ] \lor [ t r u e; \neg (x; t r u e) ]) $$
$= {$ pred. calc. $}$
$$ ([ t r u e; 7 (x; t r u e) \Rightarrow t r u e; y ] \land [ x; t r u e ]) \vee $$
$$ ([ \mathrm {t r u e}; \neg (x; \mathrm {t r u e}) \Rightarrow \mathrm {t r u e}; y ] \land [ \mathrm {t r u e}; \neg (x; \mathrm {t r u e}) ]) $$
$\Rightarrow$ {pred. calc.}
$$ [ x; \mathrm {t r u e} ] \vee [ \mathrm {t r u e}; y ] $$
(End of Intermezzo.)
Point - Predicates
The traditional model for the predicate calculus is known as "the powerset model". The underlying space is a nonempty set $S$ , and each predicate $Q$ corresponds to a subset of $S$ . The predicates that correspond to singleton sets, i.e. to the elements of $S$ , are called "point-predicates", and being a point-predicate is formally defined by
$$ \begin{array}{l} (p \mathrm {i s a p o i n t - p r e d i c a t e}) \equiv \ \langle \forall^ {\prime} Q:: [ p \Rightarrow Q ] ^ {\prime} \equiv \neg [ p \Rightarrow \neg Q ] \rangle \ \end{array} $$
An immediate consequence is that false is not a point-predicate. A next consequence is that there is no predicate "between" false and a point-predicate, more precisely, for point-predicate $p$
$$ [ Q \Rightarrow p ] \Rightarrow [ Q \equiv f a l s e ] \vee [ Q \equiv p ] $$
Proof We observe for any predicate $Q$ and any point-predicate $p$
$$ [ Q \Rightarrow p ] $$
$$ \begin{array}{l} \Rightarrow {p _ {i} \mathrm {i s p o i n t - p r e d i c a t e} } \ [ Q \Rightarrow P ] \land ([ P \Rightarrow i Q ] \lor [ P \Rightarrow Q ]) \ \Rightarrow \quad {\mathrm {p r e d . c a l c .} } \ [ Q \equiv f a s e ] \vee [ Q \equiv p ] \ \end{array} $$
(End of Proof.)
In what follows, $p$ is understood to range over point-predicates.
The crucial decision is whether or not we add as axiom the "power set postulate"
$$ \begin{array}{l} - " P S P" f o r s h o r t - \ (P S P) \quad [ \langle \exists p: p \rangle ] \ \end{array} $$
which postulates the existence of so many "points" that they fill up the underlying space. An alternative formulation is
$$ (P S P ^ {\prime}) \qquad [ \langle \exists p: [ p \Rightarrow Q ]: p \rangle \Leftarrow Q ] \qquad f o r a l l Q $$
(Note that $\left\lbrack {\langle \exists p : \lbrack p \Rightarrow Q\rbrack : p\rbrack \Rightarrow Q}\right\rbrack$ for all $Q$ is a direct consequence of predicate calculus.)
Proof The proof is by mutual implication.
$\left( {P{S}{P}}\right) \Leftarrow \left( {P{S}{P}{}^{\prime }}\right)$ By instantiating ${P}_{S}{}^{\prime }$ with
$$ (P S P) \Rightarrow (P S P ^ {\prime}) \quad W e o b s e r v e f o r a n y R $$
$$ \begin{array}{r l} & {[ \langle \exists p: p \rangle ]} \ {=} & {{\mathrm {d e f i n i t i o n o f p o i n t - p r e d i c a t e} }} \end{array} $$
$$ [ \langle \exists p: \langle \forall Q:: [ p \Rightarrow Q ] \equiv \neg [ p \Rightarrow \neg Q ] \rangle : p \rangle ] $$
$\Rightarrow$ ${$ instantiate $\forall$ with $Q : = R} \exists$ monotonic in range $}$ $\left\lbrack {\langle \exists p : \left\lbrack {p \Rightarrow R}\right\rbrack \equiv \neg \left\lbrack {p \Rightarrow \neg R}\right\rbrack : p}\right\rbrack$ $\Rightarrow$ {pred. calc.} $= \left{ {{r}{1} \cap {r}{2} \cap {r}_{3}}\right}$ $\Rightarrow$ ${$ pred.ca,c.,as noted above $}$ $\left\lbrack {\langle \exists p : \lbrack p \Rightarrow R\rbrack : p\rangle v\neg R}\right\rbrack$
$$ \begin{array}{l} = {\mathrm {p r e d . c a l c .} } \ [ \langle \exists p: [ p \Rightarrow R ], p \rangle \Leftarrow R ] \ \end{array} $$
(End of Proof.)
Point-predicates are of interest, as they provide a concept in terms of which the relational calculus and the regularity calculus can be distinguished: in the latter, $J$ is -as we have seen- a point-predicate, whereas in the former it is not. More interesting, however, is how much can be proved without PSP!
Remark It makes sense to talk about a predicate calculus without P5P, for P5P is truly an independent axiom, as is shown by a model of the predicate calculus that satisfies all axioms of the predicate calculus. (Rough sketch: predicates are associated with sets of open intervals of the real-number line such that their union equals the interior of the closure of that union. Negation, disjunction, and conjunction are modelled by complement, union, and intersection respectively, but always followed by the idempotent operation of taking the interior of the closure. The catchword in the mathematical literature seems to be "regular open". Unless I am mistaken, this construction can be generalized for the relational calculus in such a way that J still exists, for instance by confining the regularization operation (of taking the interior of the closure) to the direction parallel to the diagonal.) (End of Remark.)
The calculi without PSP are known as "pointless predicate calculus" or "pointless logic" and "pointless relational calculus" respectively, and it is amazing - over the years, it was an eye-opener at least for me! - how much can be done in these pointless calculi.
I knew, for instance, what I thought were three equivalent expressions for the well-foundedness of a relation
- the validity of a proof by mathematical induction the existence of minimal elements for nonempty subsets
- the finiteness of all decreasing sequences of elements.
In contrast to the last two definitions, which ex- plicitly mention "elements", the first one admits a pointless formulation:
$$ (S \mathrm {i s l e f t - w e l l f o u n d e d}) \equiv $$
$$ \langle \forall P: [ P \Rightarrow \mathrm {f a l s e} ] \Leftarrow [ P \Rightarrow S; P ] \rangle , $$
a pointless definition of well-foundedness that sufficed to prove a number of fundamental theorems about well-foundedness quite elegantly.
In reasoning about programs, the annotations play the role of the predicates, machine states the role of "points". Machine states are what individual computations are about, and this observation gives us another way of appreciating the transition from set theory to the "pointless logic":
without PSP, the machine states have disappeared from the picture and, of necessity, our considerations become nonoperational. Acknowledgements For direct or indirect contributions I thank A. Tarski, C.A.R. Hoare, He Jifeng, Stephen Brien, Carel S. Scholten, W.H.J. Fegen, A.J.M. van Gasteren, Rutger M. Dijkstra, W.H. Hesselink, Josyula R. Rao, David A. Naumann and Roland C. Backhouse and his collaborators.
References
A. Tarski, "On the calculus of relations", Journal of Symbolic Logic 6,3 (1941) 73-89 Jaap van der Woude, "Calculations with Relations, an Example" in Beauty is our Business, eds. W.H.J.Fegen, A.J.M.van Gasteren,D.Gries,J.Misra (Springer-Verlag, 1990)pp.435-441 C.A.R. Hoare and He Jifeng, Fundamenta Informaticae 9:pp.51-84,217-252,1986 W.H.J. Fegen and A.J.M. van Gasteren "An IntroductiOn to the Relational Calculus" in "C.S. Scholten Dedicata: Van oude machines en neue rekenwyzen", eds. W.H.J. Fegen and A.J.M. van Gasteren, Academic Service, 1991, pp. 57-81 Edsger W. Dgkstra and Carel S. Scholten, "Predicate Calculus and Program Semantics," Springer-Verlag, 1990
Roland C. Backhouse et al., "A Relational Theory of Datatypes", December 13, 1990, Department of Mathematics and Computing Science, Eindhoven University of Technology, The Netherlands Rutger H. Dgjakstrc, Private Communications.
This note has been specially written for the 1992 International Summerschool in Marktobendorf, Germany
Austin, 10 June 1992
prof. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188 USA