\underline{\underline{\underline{2}}} On the computational significance of consistency: from ordinary to generalized recursion theory

June 30, 1994^{1}

Abstract. The logical character of a transition-based notion of computation is explored in relation to Turing’s ordinal logics and certain subsequent developments. The addition of Π_{1}^{0} consistency statements in ordinal logics is portrayed as an attempt to extract fast programs computing a theory’s provably recursive functions, and is noted to require (for the attempt to succeed) ordinal notations coding computations extraneous to the ordinal named. This motivates a richer semantic conception of computation based on transitions that include input/output transitions as special cases. In this regard, the equivalence underlying the construction of the next admissible set from trees is linked with the notion of a bisimulation, subsuming both input/output equivalence of programs and equivalence between ordinal notations naming the same ordinals. Complications introduced by non-well-foundedness (reflecting, for instance, non-termination of computational systems) are investigated, including Σ_{1}^{1} − Π_{1}^{1} pre-quotients of r.e. transition predicates. Π_{1}^{1} paths through the Church-Kleene system O of ordinal notations are employed to analyze this leap from syntactic Π_{1}^{0} consistency statements to a semantic Σ_{1}^{1} notion of a computational process.

The starting point of various generalizations of ordinary recursion theory is the statement

(1)  {e}(x) ≃ y

asserting that the program named e returns output y, given input x. In view of Church’s thesis, however, it is not clear what relevance a non-r.e. set of input/output triples e, x, y, can have for mechanical computation. Accordingly, the object of generalization in the present paper is not so much the computational power behind (1), but rather the form of (1) itself, which is

1Added, February 11, 1997 . This paper was the basis of a talk at a conference on Proof Theory, Provability Logic and Computation in Berne (March 1994), and was submitted for refereeing for a special issue of the Annals of Pure and Applied Logic consisting of selected papers from the conference. The two referees reviewing the paper recommended publication on the condition that it be “more or less completely” revised. The style in which it was written was deemed unacceptable for a mathematical journal. But as the thrust of the work was largely philosophical and programmatic, I feared the paper would become pointless if I were to carry out the referees’ advice to “concentrate on the mathematical contents.” Consequently, I withdrew the paper, hoping to return to it at some later point. Some two and a half years later, I have been unable to carry out a single revision and am as uncertain as ever of attracting for it the attention of a sufficiently indulgent reader. But as I still believe the point of the paper is worth making, I include it here for the record.

generalized into a possibly non-deterministic and non-terminal “transition,” collectively forming a set that is r.e. under some syntactic presentation. An abstract semantic analysis of that syntax then takes us beyond the realm of the r.e., and through both syntactic and semantic notions of consistency.

More concretely, consider transitions of the form (s, d) →_{e} (s′, d′) where the transition predicate →_{e} relates pairs (s, d) and (s′, d′) of “control states” s, s′ and “data configurations” d, d′. The input/output relation (1) then assumes the special form (s_{0}, x) →_{e} (√, y), where s_{0} and √ are fixed initial and terminal states, respectively. Not all transitions need end at some (√, y), however, which is to say that reducing a program to the function it computes is inadequate, if intermediate states (s′, d′) (with s′ not terminal, nor initial) in the computation of that function are also of interest. To say that a program is its name (or text, Gödel numbered) e may ultimately be the safest answer to the question what is a program? A more “semantic” characterization would, on the other hand, abstract away syntactic details and provide an answer on the basis simply of the transitions the program can make. That, at least, is what the present paper investigates, employing the notion of a bisimulation (Park [19]) to obtain an equivalence on states based solely on transitions between them, and eventually pointing to a set-theoretic notion of computation. Towards that end, the transition (s, d) →_{e} (s′, d′) is recast as s →^{d,d′}_{e} s′, and then further to

(2)  e ⇝^{d,d′} e′ ,

where a program ê is identified with the initial state of the transition predicate →ê, which is, in turn, embedded in some monster transition predicate ⇝. Shifting the basic picture from input/output statements (1) to transitions (2) is, it is argued, far from a triviality, considering the partiality of computation.

Apart from some faint hope in gaining a “semantic” understanding, the move from (1) to (2) can be motivated by the “no-nonsense” problem of isolating programs that run quickly — or more precisely, the problem of

(∗) extracting fast programs computing a theory’s

provably recursive functions.

A “path” to generalized recursion theory is paved by an explosion in logical complexity from what can be viewed as an early attempt (i.e., Turing [21]) to solve (∗) — an attempt that, upon reflection, leads to a far richer (set-theoretic) notion of computation. Briefly, the point is that the notions of equivalence on (i) ordinal notations from Turing [21], (ii) hyperprojective trees in the Barwise, Gandy and Moschovakis (1971) construction of the next admissible set,^{2} and (iii) accessible pointed graphs in Aczel [1]’s relative consistency argument for the Anti-Foundation Axiom are all bisimilarity (i.e., the largest bisimulation). Thus, the well-known table

2The presentation of the next admissible in Barwise [4] is different, appealing instead to the theory of constructible sets.

ordinary recursion th generalized recursion th
number (∈ ω)  set (∈ L_{α})
Π_{1}^{0}  co-α-r.e

extends to

ordinary recursion th generalized recursion th
syntax (code e)  semantics (set of transitions)
speed-up  substitutivity
consistency  bisimilarity

complementing the move from (1) to (2). The move suggests a step beyond not only equational reasoning, as advocated (for example) in Baeten and Weijland [2], but also first-order logic and, further than that, ω-logic (styled respectively as Σ_{1}^{0}- and Π_{1}^{1}-logic in Girard [11]). Model-theoretic arguments concerning bisimilarity that involve (respectively) saturation (a tool of first-order logic) and omitting types (a property of ω-logic) illustrate the point. The basic fact is that the Π_{1}^{1} bound on bisimilarity relative to well-founded Δ_{1}^{1} transition predicates (implicit in Barwise, Gandy and Moschovakis [3]) is exceeded by bisimilarity relative to a non-well-founded logspace computable predicate.

Of course, the idea of applying generalized recursion theory to programming languages and processes is far from new. Consider, for example, recent papers of Moschovakis (e.g., Moschovakis [18]). The “path” described in the present paper, however, goes back further to ancient work of Alan Turing’s (Turing [21]), analyzed in relation to more modern developments in Feferman [6, 7], on which, in turn, a good deal of the present work builds (motivating the concept of relative computability by analyses based on different transition predicates).

1. Background: between absoluteness and open ended-ness

In a conference held in 1946, Gödel described recursion theory as being singularly successful “in giving an absolute definition of an interesting espistemological notion, i.e., one not depending on the formalism chosen” (Gödel [12], p. 150). Whereas the recursion-theoretic notion of computation is, according to Church’s thesis, stable (capturing, as is claimed, all functions that can be computed mechanically), formal notions of deduction are defined “relative” to a formal theory that is (by contrast) subject to (Gödel) incompleteness. Curiously, the same functional reduction of computation in Church’s thesis has been employed as the basis for a proof-theoretic approach to computation, which, as will be argued shortly, can only imperfectly approximate the “absolute” notion of a program.

Given an input/output specification S(x, y), it is possible, under suitable circumstances, to extract from a constructive proof of

(∀ input x) (∃ output y) S(x, y)

a program e realizing (Kleene [14]) the theorem, where

e realizes (∀x)(∃y)S(x, y) implies

(∀x) {e}(x)↓ & S(x, {e}(x)) . (3)

The correspondence between proofs and programs is developed further in the Curry-Howard isomorphism (e.g., Girard, Lafont and Taylor [10]) between a typed λ-calculus and a natural deduction system, under which computation becomes normalization (roughly, the unwinding of lemmas in a proof). Underlying the isomorphism is a theorem stating

(weak) normalization : (∀ term t) (∃ reduction r)

(4) r takes t to a normal form .

Now, although deduction may not be “absolute”, the proofs of (3) and (4) can be formalized, which is to say that every program e provably extracted in some theory T is provably total in T —

T |− Tot(e) ,

where Tot(e) is (∀x)(∃y)T_{1}(e, x, y) and T_{1} is (the appropriate form of) Kleene’s computation predicate.

1.1. Provably recursive functions versus provably recursive programs. The family of programs e that are provably total may look nice functionally, but is flawed upon closer inspection. More precisely, if the provably recursive functions of T are defined (following Kreisel [15]) as members of the set

Fcn(T) := {{e} | T |− Tot(e)} ,

then

Proposition 1. If T contains primitive recursive arithmetic then Fcn(T) forms a (time-)complexity class — i.e.,

(5)  T |− Tot(e) and t_{e′} < t_{e} a.e. imply {e′} ∈ Fcn(T)

where t_{e} counts the number of steps in the computation given by the Kleene T_{1}-predicate.

On the other hand,

Proposition 2. The conclusion of (5) can be strengthened to T |− Tot(e′) (with or without the assumption {e} = {e′}) if and only if T proves all true Π_{1}^{0} sentences.

Proposition 1 and the sufficiency in Proposition 2 follow from t_{e}(x) being primitive recursively related to (μy)T_{1}(e, x, y), making the clause ‘t_{e′} < t_{e} a.e.’ Π_{1}^{0}. As for the necessity in Proposition 2, given a true Π_{1}^{0} sentence (∀x)R(x) (where R is a primitive recursive predicate), define

e : on input n, check (∀m ≤ n + 1) R(m);

return 0 (in any case).

e′ : on input n, check R(n);

if so return 0, else loop.

Then t_{e′} < t_{e}, {e′} = {e}, T |− Tot(e), and if T |− Tot(e′), then T |− (∀x)R(x). A similar argument occurs in Turing’s completeness theorem below, but first, we pause to ask if such pathological programs can be avoided. Blum’s speed-up theorem stating that some functions have no optimal programs would seem to suggest not, as discussed at further length in Fernando [8] (where the propositions above are drawn from, and where normalization for a calculus under a Curry-Howard isomorphism is cited as an example of such a function). To round off the relationship between Π_{1}^{0} sentences and programs of bounded complexity, Kreisel [15] has shown that

Fcn(T) = Fcn(T + {all true Π_{1}^{0} sentences}) .

That is, overcoming Π_{1}^{0}-incompleteness is equivalent to extracting efficient programs, rather than new, more complex functions. (Normalization implies consistency but not conversely.) The restriction to programs of bounded complexity reduces the Π_{2}^{0}-completeness of totality (and input/output equivalence) to Π_{1}^{0}. A roller-coaster ride through logical complexity will, however, soon take us far beyond Π_{2}^{0}.

1.2. Turing through programs of bounded complexity. The remainder of this section draws considerably from Feferman [6], which describes Turing’s attack on the incompleteness of T by repeatedly adding (for instance) consistency statements transfinitely. To carry this out, the theories must be presented and (in particular) the ordinals 0, 1, …, ω, ω + 1, … must be named. Such a system of ordinal notations can be built, relative to a standard enumeration of the partial recursive functions {e}, by defining an r.e. binary relation ≺ on ω by

\frac{a > 0}{a ≺ 2^{a}}  \frac{\{e\}(n) is defined and > 0}{\{e\}(n) ≺ 3 · 5^{e}}

\frac{a ≺ b b ≺ c}{a ≺ c} ,

and assigning ordinal heights

|a| = {|b| | b ≺ a}

whenever ≺ is well-founded on {b | b ≺ a}.^{3} In particular, | · | is defined on the set O ⊂ ω of Church-Kleene ordinal notations generated by

\overline{1 ∈ O}  \frac{a ∈ O}{2^{a} ∈ O}

\frac{\{e\}(n) ∈ O and \{e\}(n) ≺ \{e\}(n + 1) for all n}{3 · 5^{e} ∈ O} .

The recursive ordinals are the ordinals |a| named by a ∈ O, and collectively form the least non-recursive ordinal ω_{1}^{CK}. The progression {T_{a}}_{a∈O} of theories

T_{1} = T
T_{2^{a}} = T_{a} + Con[T_{a}]
T_{3·5^{e}} = ⋃_{n<ω} T_{{e}(n)}

then constitutes an ordinal logic.

An ordinal logic provides, in Turing’s view, a very rough and admittedly oversimplified model of mathematical reasoning (see Feferman [6], p. 129). A proof of a mathematical assertion A consists of an “intuitive” step (of complexity Π_{1}^{1}) in which an ordinal notation a ∈ O is chosen, and a “mechanical” step (of complexity Σ_{1}^{0}) establishing that T_{a} |− A. It turns out (perhaps not too surprisingly) that the burden of proving a true Π_{1}^{0} sentence can be shoved over to the choice of a.

Theorem (Turing). For every true Π_{1}^{0} sentence A, there is an a ∈ O naming ω such that

T_{a} + Con[T_{a}] |− A .

Proof sketch. For A equal to (∀x)R(x) with R primitive recursive, take a = 3 · 5^{e} where e satisfies (by the second recursion theorem)

\{e\}(n) = \{ \begin{matrix}n_{O} & if (∀x < n) R(x) \\ Suc_{≺}(3 · 5^{e}) & otherwise \end{matrix}

with 0_{O} = 1, (n + 1)_{O} = 2^{n_{O}}, and Suc_{≺}(a) = 2^{a}. ⊣

Commenting on the proof of the theorem, Turing [21] had this to say. The completeness theorem as usual is of no value. Although it shows, for instance, that it is possible to prove Fermat’s last theorem … (if it is true), yet the truth of the theorem would really be assumed by taking a certain formula as an ordinal formula [ordinal notation].

3The assumption of well-foundedness can be dropped so long as |a| is allowed to be a non-well-founded set, as in the set theory of Aczel [1]; see subsection 2.2 below.

With an eye on a more general notion of ordinal logics T_{a} not necessarily based on the addition of consistency statements, Turing had further established the incompatibility of completeness with invariance under the choice of an ordinal notation: the property that whenever |a| = |a′|, T_{a} ≡ T_{a′}. Referring the interested reader to Feferman [6] for details on Turing’s work, let us turn instead to a fundamental negative result concerning ordinal logics obtained after Turing, two ideas behind which will be of use to us later, namely

Σ_{1}^{1} boundedness: the height of every Σ_{1}^{1} well-order is a recursive ordinal.

Non-standard ordinal notations: a Σ_{1}^{1} set O^{∗} ⊃ O indistinguishable from O up to Δ_{1}^{1} sets can be defined by requiring that for such a ∈ O^{∗}, there are no Δ_{1}^{1} ≺-descending sequences from a. More precisely, O^{∗} is the intersection of all Δ_{1}^{1} sets X of natural numbers that contain (i) 1, (ii) 2^{a} whenever a ∈ X, and (iii) 3 · 5^{e} whenever (∀n) {e}(n) ∈ X & {e}(n) ≺ {e}(n + 1).

Defining a path Z through O as a subset Z of O linearly ordered by ≺ such that for every a ∈ O there is a unique b ∈ Z with |a| = |b|, the negative result is

Theorem (Feferman and Spector). Π_{1}^{1} paths through O exist, and for all such paths Z, there is a true Π_{1}^{0} sentence not provable in ⋃_{a∈Z} T_{a}.

It is not altogether surprising then that Turing should be dissatisfied with ordinal logics as a practical method towards proving theorems (Feferman [6], p. 140). As an investigation into computation, rather than deduction, however, it would seem fair to say the following. Although Turing is remembered now mainly for “low level” programming (i.e., Turing machines, and perhaps even more importantly, cryptanalysis hacking), at least two somewhat abstract lines of research can be extracted from the work above that he initiated. First, one might carry on with an ordinal classification of programs of bounded complexity, paying careful attention to the notations used, and perhaps (in view of incompleteness along Π_{1}^{1} paths through O) abandoning any hope of assigning all such programs a recursive ordinal. Second, as to his completeness proof being “of no value”, one might argue that, on the contrary, by loading computations into an ordinal notation, he, in fact, anticipated a richer notion of computation, of not inconsiderable interest to current theoretical investigations. That notion of computation is essentially the “intuitive” component of his ordinal logics that, moreover, by resisting elimination, led (already in Turing [21]) to the concept of relative computability. Pursuing this line of investigation further, the present paper is intended as a contribution to the argument made in Feferman [7] that relative computability is relevant to ordinary computation, in view of the myriad levels of abstraction relative to which a computation can be analyzed.

2. From ordinal notations to processes: bisimulations

The ordinal notations isolated in Turing’s completeness proof constitute early examples of computational processes with the following “open-ended” features: intermediate computational states, non-provable termination, and countable non-determinism. These features are presently fleshed out.

2.1. Programs as states in a transition system. Without spelling out precisely what a transition is, it would appear plausible from Church’s thesis to stipulate that the transitions undergone by a machine form, under a suitable syntactic presentation, an r.e. set. That is, to say that a transition predicate is mechanical is to assert that its transitions t can be named as theorems of some formal system. Indeed, an automaton (= program) e is typically characterized by its legal moves i |− i′ between so-called “instantaneous descriptions” i and i′. An instantaneous description i consists of a control state s and a data (e.g., tape) component d (plus an indication of the tape symbol currently being scanned, which we will assume is made implicit in the presentation of d). Roughly, what we will do is rewrite (s_{0}, d) →_{e} (s′, d′) as (e, d) → (e′, d′) where e′ is the program described by →_{e} with initial state s′, and → contains a copy of →_{e}. Replacing e by p, the picture

(p, d) → (p′, d′)

appears explicitly in so-called mixed computation (Bjørner, Ershov and Jones [5], p. xxvi), which we will recast as

(6)  p ⇝^{d,d′} p′

to set the stage for an analysis of programs p relative to data d. That is, packaging the pairs (d, d′) as labels l forming a set L, and passing from a program p back to the somewhat more abstract notion of a state s populating some set S, (6) leads to the notion of a (labelled) transition system, a triple (L, S, →) where → ⊆ S × L × S. By presenting programs as states (following so-called structural operational semantics, Plotkin [20]), we can use a notion of equivalence on states to get a notion of equivalence on programs. But first, returning to the transition predicate ⇝ ⊆ ω × ω × ω occuring in (6), observe

Proposition 3. There is an r.e. predicate ⇝ ⊂ ω × ω × ω that contains a copy of every r.e. transition predicate in that for every r.e. → ⊆ ω × ω × ω, there is a function f (that is, in fact, 1-1 and recursive) with domain equal to the set {s | (∃l, t) s →^{l} t or t →^{l} s} of →-states such that (i) for all s, l, t,

s →^{l} t iff f(s) ⇝^{l} f(t) ,

and (ii) for every u,

f(s) ⇝^{l} u or u ⇝^{l} f(s) implies (∃t ∈ dom(f)) f(t) = u .

Proof. Fix a binary primitive recursive function ⟨·, ·⟩ : ω × ω → ω and unary primitive recursive functions i, j : ω → ω such that for all n, m < ω,

i(⟨n, m⟩) = n , j(⟨n, m⟩) = m and ⟨i(n), j(n)⟩ = n .

Let U be an r.e. set such that {U_{e}}_{e<ω} enumerates all r.e. sets, where

U_{e} = {n | ⟨e, n⟩ ∈ U} ,

and define ⇝ to be

{(s, l, s′) ∈ ω × ω × ω | i(s) = i(s′) and
⟨j(s), ⟨l, j(s′)⟩⟩ ∈ U_{i(s)}} .

Note that ⇝ is slightly different from a standard parametrization of binary r.e. predicates (although the modifications are minor enough). It is, in a suitable sense, an effective disjoint sum of all r.e. transition systems: given an r.e. →,

define f on →-states s by f(s) = ⟨e, s⟩ where U_{e} = {⟨s, ⟨l, t⟩⟩ | s →^{l} t}. ⊣

There are countably many transition predicates meeting the specification of ⇝ given in Proposition 3, although, as will become plain shortly, they share the same abstract structure. For now, observe that ⇝ generalizes the functional analysis of programs, {e}(x) ≃ y being the special case [e] ⇝^{x,y} √, for some fixed encoding [e] of e. More generally, returning to a transition predicate → with data pair labels as in (6), it is simple enough to define transformations from → to →_{∗}

\frac{p →^{d,d′} q}{p →^{d,d′}_{∗} q}  \frac{p →^{d,d′′}_{∗} q  q →^{d′′,d′} p′}{p →^{d,d′}_{∗} p′} ,

and then to →_{at}

\frac{p →^{d,d′}_{∗} √}{p →^{d,d′}_{at} √} ,

setting the stage for a characterization of input/output equivalence by a more general notion to be defined next. (Note that if → is r.e., then →_{∗} and →_{at} are r.e. as well; i.e., ·_{∗} and ·_{at} can be interpreted inside ⇝.)

2.2. Bisimulations and extensionality generalized. For an equivalence R on states to “respect” →, it is natural to expect that if sRs′ then s′ can “simulate” every transition from s

(∀l ∈ L) (∀x ←^{l} s)(∃y ←^{l} s′) xRy ,

and conversely, s can simulate s′

(∀l ∈ L) (∀y ←^{l} s′)(∃x ←^{l} s) xRy .

It will prove useful to consider binary relations R ⊆ S × S′ between the states of possibly two distinct transition systems ⟨L, S, →⟩ and ⟨L, S′, →′⟩ and to formulate the requirements above within the “back-and-forth” operator ·^{bf} that sends R to the relation R^{bf} consisting of pairs (s, s′) ∈ S × S′ such that for every l ∈ L,

(∀x ←^{l} s)(∃y ←′^{l} s′) xRy and (∀y ←′^{l} s′)(∃x ←^{l} s) xRy} .

R is a bisimulation (Park [19]) if R ⊆ R^{bf}. Because R occurs positively in R^{bf}, the operator R ↦ R^{bf} is (⊆-)monotone, and the largest bisimulation \underline{↔} (between ⟨L, S, →⟩ and ⟨L, S′, →′⟩) can be calculated co-inductively as ⋂\{\underline{↔}_{α} | α < card(S × S′)^{+}\}, where

\underline{↔}_{α} = ⋂_{β<α} (\underline{↔}_{β})^{bf}

(e.g., Milner [16]). The relation \underline{↔} is also called bisimilarity and is manifestly Σ_{1}^{1} in → and →′

s \underline{↔} s′ iff (∃R) R is a bisimulation relating s to s′ .

The extensional character of bisimilarity \underline{↔} is nicely illustrated by two simple examples. First, input/output equivalence can be recovered as bisimilarity relative to the transition predicate →_{at} described in the end of subsection 2.1^{4}

p and q are input/output equivalent iff p \underline{↔}_{at} q .

This example is somewhat degenerate inasmuch as the notion of a bisimulation is of interest mainly for transition predicates ⇁ with long chains of transitions s ⇁^{l} s′ ⇁^{l′} s′′ ⇁^{l′′} s′′′ · · ·. Our second example is of this kind, and furthermore makes do with a singleton label set (i.e., |L| = 1), in contrast to →_{at}, which uses labels heavily. More specifically, a binary relation B is turned into a transition predicate →_{B}= {(a, ∗, b) | aBb}, by introducing some fixed label ∗ to the pairs in B. We will henceforth speak of bisimulations and bisimilarity over a binary relation B, when we actually have in mind the transition predicate →_{B} formed from it. Now, defining the Mostowski collapse c_{B} of a well-founded binary relation B by

c_{B}(a) = {c_{B}(b) | bBa} ,

then, as pointed out in Aczel [1],

c_{B}(a) = c_{B}(a′) iff a\underline{↔}a′ ,

where \underline{↔} is bisimilarity relative to B (i.e., →_{B}). Aczel [1] goes on to develop a set theory supporting this equivalence, whether or not B is well-founded (so that, in particular, c_{B} is always well-defined).

s →^{√} t iff s = t = √ .

4The map ·_{at} can be arranged to respect bisimilarity (i.e., s \underline{↔}_{at} t if s \underline{↔} t) by adjoining a fresh label √ and postulating Note that the last condition above is not satisfiable in ⇝, but in some r.e. transition predicate with a copy in ⇝.

Returning to the coinductive characterization of \underline{↔}, note that S × S′ = \underline{↔}_{0} ⊇ \underline{↔}_{1} ⊇ ⋯ ⊇ \underline{↔}_{ω} ⊇ \underline{↔}_{ω+1} ⊇ ⋯ ⊇ \underline{↔}, where \underline{↔} may differ from \underline{↔}_{ω}, as illustrated by the notorious pair

Figure 1

Confusing these trees is problematic inasmuch as the infinite branch can be interpreted as a failure of termination (or, say, an unfair merging of an infinite stream 1^{∞} of 1’s with 0, where 0 is forever neglected). The Approximation Induction Principle (AIP) of (for example) Baeten and Weijland [2] is (under an interpretation of equality as bisimilarity) the statement \underline{↔} = \underline{↔}_{ω}. Just how badly AIP fails is a measure of the complexity (and hence, scope) of \underline{↔}. Nevertheless, a routine saturation argument can be employed to justify \underline{↔} = \underline{↔}_{ω}.

Proposition 4. For every transition predicate → ⊆ S × L × S, there is a transition predicate →′ ⊆ S′ × L × S′ with \underline{↔}′ = \underline{↔}′_{ω} such that the first-order

structure ⟨S, {→^{l}}_{l∈L}⟩ is elementarily equivalent to ⟨S′, {→′^{l}}_{l∈L}⟩.

Proposition 4 is an immediate consequence of the existence of recursively saturated elementary extensions (e.g., Barwise [4], p. 74), and the fact that a coinductive process of the sort that yields bisimilarity closes off at ω for recursively saturated models (e.g., Barwise [4], pp. 139, 210). At any rate, the moral of Proposition 4 is clear: first-order logic is inadequate for analyzing bisimilarity. The opposite of a saturation argument is an omitting types argument, a close companion of ω-completeness, and therefore ω-logic (or, as Girard [11] would put it, Π_{1}^{1}-logic). Curiously, omitting types is employed in Fernando [9] to bring out the first-order dependence on data, which is analyzed by reformulating transitions of the form p →^{d,d′} p′ as d →^{p,p′} d′. An altogether different use of omitting types is in proving the Gandy-Kreisel-Tait theorem (e.g., Barwise [4], p. 116) stating that the only sets a Π_{1}^{1} theory is committed to are Δ_{1}^{1}. This fact is worth keeping in mind when establishing (as we will below) the non-Π_{1}^{1} nature of bisimilarity relative to a certain logspace computable binary relation.

3. Pushing the analogy: semantics from syntax

Whereas termination is essential to an input/output (e.g., functional) view of computation, the question of termination takes on a different character within a more general theory of computational transitions that includes input/output transitions as special cases. Indeed, as has often been pointed out, non-termination is perfectly respectable, if not desirable, in so-called reactive systems (e.g., operating systems) that cease to be of service as soon as they terminate. The cost of admitting such immortality (formulated mathematically as non-well-foundedness) particularly in the presence of countable non-determinism is the subject of the present section.

As is implicit in Barwise, Gandy and Moschovakis [3], bisimilarity \underline{↔} is Δ_{1}^{1} in a transition predicate →, provided → (or, more precisely, {(s, t) | (∃l) s →^{l} t}) is well-founded. It is easy to see why this should be the case. Recall that R ⊆ S × S is a bisimulation iff R ⊆ R^{bf}. Dually, call R a co-bisimulation if R^{bf} ⊆ R. Note that \underline{↔} is a cobisimulation, and that there is a least cobisimulation ∼ which can be calculated inductively in the usual fashion, and which is a fixed point of ·^{bf}. Thus, since \underline{↔} is the largest bisimulation, it remains to prove \underline{↔} ⊆ ∼, assuming → is well-founded. That is, it is enough to establish

(∃s, s′) s \underline{↔} s′ & s ≁ s′ implies

(∃l, t, t′) t \underline{↔} t′ & t ≁ t′ & s →^{l} t ,

as this yields an infinite ⋃{→^{l} | l ∈ L}-descending sequence. But then, as ∼ is a cobisimulation, it follows from s ≁ s′ that for some l, either (i) for some t ←^{l} s, (∀y ←^{l} s′) t ≁ y, in which case s \underline{↔} s′ implies there is a t′ ←^{l} s′ such that t \underline{↔} t′, or (ii) for some t′ ←^{l} s′, (∀x ←^{l} s) x ≁ t′, and symmetrically, a t ←^{l} s such that t \underline{↔} t′ follows from s \underline{↔} s′. Thus, if → is well-founded then \underline{↔} is the unique fixed point of ·^{bf} and \underline{↔} is ∼

s \underline{↔} s′ iff (∃R) Bis(R) & Cobis(R) & sRs′
iff (∀R) Bis(R) & Cobis(R) ⊃ sRs′
iff (∀R) Cobis(R) ⊃ sRs′ ,

where Bis(R) and Cobis(R) are the obvious predicates (arithmetic in →) defining bisimulations and cobisimulations, respectively. Note that, in general, s \underline{↔} s′ is not equivalent to (∃R) Cobis(R) & sRs′ nor to (∀R) Bis(R) ⊃ sRs′ (because of relations such as S × S and =).

Turning now to non-well-foundedness, what price must be paid for it? And what, in abstract, structural terms, do we get in return?

3.1. The challenge of non-well-foundedness. Recall that an admissible set (e.g., Barwise [4]) is a transitive set that (under the standard interpretation of ∈) is a model of a certain weak set theory, KP. KP is characterized (among other axioms) by restricted, so-called Δ, forms of comprehension and collection. The paradigmatic example is where Δ is interpreted as (hereditarily) Δ_{1}^{1}, a principal motivation being to capture various facts about the Δ_{1}^{1} sets on which a generalization can be based. In particular, two facts that generalize to some degree or another will interest us.

(a) The Π_{1}^{1} sets are exactly the inductive sets — i.e., sets of the form {n | I_{φ}(0, n)} for some elementary formula φ(x, y, R) positive in the binary relation symbol R, where I_{φ}(x, y) is the least fixed point of the operator

B ↦ {(m, n) | φ(m, n, B)}

on binary relations B. Thus, the Δ_{1}^{1} sets are exactly the sets that are both inductive and coinductive; in other words, the hyperelementary sets. This fact (due to Kleene and Spector) generalizes to countable sets, but may fail for uncountable sets (e.g., Moschovakis [17]).

(b) The set of Δ_{1}^{1} well-orders is not Σ_{1}^{1}, implying that there are non-well-founded Δ_{1}^{1} linear orders that have no Δ_{1}^{1} descending sequences — socalled pseudo-well-orders. Defining the well-founded part wf(⊏) of a linear order ⊏ as the set of pairs (x, y) such that x ⊏ y and there are no ⊏-descending sequences from y, it follows that such a pseudo-well-order must have a well-founded part containing a copy of every Δ_{1}^{1} wellorder (as in the Feferman-Spector [6] result mentioned in section 1.2 above). Of course, there are no pseudo-well-orders if well-foundedness is hyperelementary (i.e., when the β-axiom mentioned in Barwise [4] holds).

Given a set A, Barwise, Gandy and Moschovakis [3] define

A^{+} = ⋂{M | M is admissible and A ∈ M}

and go on to construct A^{+} by a quotient construction similar to that of Aczel [1], where transitions are unlabelled and taken to be ordered pairs. It is crucial that \underline{↔} be hyperelementary to push the argument in Aczel [1] through KP’s restricted schemes of separation and collection. Assuming A is a nonempty transitive set closed under pairing, Barwise, Gandy and Moschovakis [3] encode A^{+} by hyperelementary subsets of A that are well-founded trees. An inessential difference from Aczel [1] is that the transition predicates are unwound into trees, and subjected to the Mostowski collapse. An essential difference is that the predicates are assumed to be well-founded — an inductive condition, just as hyperelementarity is. But whereas well-foundedness makes \underline{↔} inductive (in →), hyperelementarity alone does not. To make this point, it will be sufficient to consider a linear order, which simplifies matters considerably. As usual, if ⊏ is a well-order, we will write | ⊏ | for its ordinal copy.

Proposition 5. Let ⊏ be a linear order on ω, and for a ∈ ω, write wf(a) for the well-founded part of the order \{(x, y) | x ⊏ y ⊏ a\}. Let \underline{↔} be bisimilarity relative to ⊏, with αth coinductive approximation \underline{↔}_{α}.

(i) For all a, b ∈ ω, and for every ordinal α,

a \underline{↔}_{α} b iff |wf(a)| ∩ α = |wf(b)| ∩ α ,

whence \underline{↔} = \underline{↔}_{β} for β = |wf(⊏)| + 1, and

a \underline{↔} b iff a = b or neither a nor b is in wf(⊏) .

(ii) Let A be an infinite set, and ⊏ be A-hyperelementary, non-well-founded but have no A-hyperelementary descending sequences. If A-hyperelementary sets admit hyperelementary well-orderings, then \underline{↔} cannot be A-inductive.

Proof. Prove part (i) by induction on ordinals α; the case where α is 0 or a limit is immediate. If α = β + 1, then

a \underline{↔}_{α} b iff (∀x ⊏ a)(∃y ⊏ b) x \underline{↔}_{β} y &
(∀y ⊏ b)(∃x ⊏ a) x \underline{↔}_{β} y (by definition)
iff (∀x ⊏ a)(∃y ⊏ b) |wf(x)| ∩ β = |wf(y)| ∩ β
& (∀y ⊏ b)(∃x ⊏ a)
|wf(x)| ∩ β = |wf(y)| ∩ β (by ind. hyp.)
iff |wf(a)| ∩ α = |wf(b)| ∩ α ,

where the last equivalence follows from the linearity of ⊏.

As for part (ii), assume towards a contradiction that \underline{↔} were A-inductive. Then (adapting the proof of the Closure Theorem of Moschovakis [17], p. 33) the formula

ψ(t, n, m, T) iff [t = 0 & (n, m) ∈ {(x, y) | T (0, x, y)}^{bf}] or
[t = 1 & (∃x, y)(T (0, x, y) & x \underline{↮} y)]

(with \underline{↔} equal to the 0-th section J_{ψ}(0, ·, ·) of the largest fixed point J_{ψ}) defines a coinduction that takes one more step than coinduction based on ·^{bf} (but not more than the least A-hyperelementary ordinal). Hence, \underline{↔} = \underline{↔}_{α} for some A-hyperelementary ordinal α, and there is an a (∉ wf(⊏)) such that whenever b \underline{↔}_{α} a, there is a descending sequence from b. Now, using an A-hyperelementary well-ordering of \{x | x \underline{↔}_{α} a\}, construct an Ahyperelementary descending sequence from a, contradiction. ⊣

The significance of A-inductiveness is shown in part by its identification, over countable admissible sets A, with A-recursive enumerability. Setting aside the matter of inductiveness (which follows from well-foundedness) and concentrating simply on the ordinals, note that \underline{↔} cannot equal \underline{↔}_{β} for some ordinal β in A^{+}, or else β and β +1 would be indistinguishable in A^{+}, which is absurd. This suggests the following elaboration of a picture found in Barwise

Figure 2

The idea behind Figure 2 is that a process is an equivalence class of (syntactic) programs, a minimal requirement on such an equivalence being that it be a bisimulation. The ordinal α is (among other things) a tight bound on the closure ordinal of an operator ·^{bf} determining whether or not there is a bisimulation relating two programs. Indeed, the explicit Σ_{1}^{1} formulation of s \underline{↔} s′, (∃R) R is a bisimulation relating s to s′, can be read as

there is a model where s and s′ are equal ,

since a bisimulation R yields a model after division: define →/R by

s →^{l}/R t iff (∃s′, t′) s′Rs & t′Rt & s′ →^{l} t′ ,

which, by the definition of a bisimulation, amounts to

s →^{l}/R t iff (∃t′Rt) s →^{l} t′ .

Note that {(s, s) | (∃l, t) s →^{l} t} is a bisimulation between → /R and →, and that →/R and → induce the same relation of bisimilarity, with, further, (→ /R)/R′ = → /R′ = (→ /R′)/R when R′ ⊇ R. We will be mainly concerned with →/\underline{↔}, which will be abbreviated as →_{∘}. For a binary relation >, we will also write >_{∘} for →_{∘} where → is {(n, 0, m) | n > m}. Call a transition predicate → reduced if → is →_{∘}. (Note that →_{∘} is reduced.) If, further, \underline{↔} is = (i.e., a \underline{↔} b implies a = b), then the transition predicate → is strongly extensional (Aczel [1]). (We will confine ourselves to → ⊆ ω × ω × ω, so that the states in strongly extensional quotients are not \underline{↔}-equivalence classes, but representatives of such.)

A non-inductive notion of bisimilarity can be obtained over a transition predicate that is not only hyperarithmetic, but by Grigorieff [13] computable in logspace. The key is Σ_{1}^{1} boundedness.

Theorem 6. (i) (Fernando [9]) Bisimilarity \underline{↔} over ≻ is Σ_{1}^{1} − Π_{1}^{1}.

(ii) ≻_{∘} is Σ_{1}^{1} − Π_{1}^{1}.

Proof. Membership in Σ_{1}^{1} is obvious. To see that the predicates lie outside Π_{1}^{1}, fix an a_{0} ∈ O^{∗} − O, and conclude from Proposition 5 (not to mention the extraction from O^{∗} of Π_{1}^{1} paths) that

{(b, 0, c) | a_{0} ≻ b & b ≻ c & b ∈ O} =
\{(b, 0, c) | a_{0} ≻ b & b ≻ c & b \underline{↮} a_{0}\} =
{(b, 0, c) | a_{0} ≻ b & b ≻ c & b ⊁_{∘} a_{0}}

is well-founded with height ω_{1}^{CK}. ⊣

Before closing this subsection, let us remark that an infinite descending sequence in a transition system may also reflect computations over infinite streams of data — e.g. infinite precision reals.

3.2. Operational semantics reduced. The measure of complexity provided by Theorem 6 concerns a particular presentation of ⇝_{∘}; its robustness might be tested by trading off the complexity of transition predicate with the complexity of bisimilarity over that transition predicate. Towards that end, the following definitions will be useful. Given two transition predicates → and →′ ⊆ ω × ω × ω, a binary relation R (on ω) copies → into →′ if R is a bisimulation between → and →′ such that

dom(R) = {s | (∃l, t) s →^{l} t or t →^{l} s} .

The predicate → has a copy in →′ if there is a binary relation R copying → into →′.

Theorem 7. Fix an a_{0} ∈ O^{∗} − O, and suppose R copies {(b, 0, c) | a_{0} ≻ b & b ≻ c} into a predicate →.

(i) If → is Σ_{1}^{1}, then bisimilarity \underline{↔} over → is not Π_{1}^{1}.

(ii) If R and \underline{↔} are Π_{1}^{1}, then → is not Π_{1}^{1}. Hence, if → is strongly extensional, then → is not Σ_{1}^{1} nor, if R is Π_{1}^{1}, Π_{1}^{1}.

Proof. Fix a b_{0} ≺ a_{0} such that b_{0} ∉ O, and choose an s_{0} such that b_{0}Rs_{0}. As {(b, 0, c) | a_{0} ≻ b & b ≻ c} is a linear order, R restricted to {b ∈ O | a_{0} ≻ b} must be a function (by Proposition 5), call it f. Appealing again to Proposition 5, note that

\{(s, 0, t) | s_{0} →^{0} s & s →^{0} t & s_{0} \underline{↮} s\} =
{(f(b), 0, f(c)) | b_{0} ≻ b & b ≻ c & b ∈ O} =
{(f(b), 0, f(c)) | b_{0} ≻ b & b ≻ c & f(b) ↛_{∘} f(b)}

is well-founded with height ω_{1}^{CK}, and that →_{∘} is Π_{1}^{1} if both \underline{↔} and → are. (For the last equivalence, recall that Π_{1}^{1} functions are Δ_{1}^{1} — f(x) = y iff (∀z ≠ y) f(x) ≠ z.) ⊣

Moving in the opposite direction, it turns out that, as complex as ⇝_{∘} is, that complexity need not provide a natural reduction of arithmetic transition predicates. That is to say, reducibility to ⇝_{∘} becomes severely restricted if the reduction f of ⟨L, S, →⟩ to ⟨ω, ω, ⇝_{∘}⟩ is required to have the form

f(x, y, z) = (g(x), h(y), g(z))

where for all s, t ∈ S and l ∈ L,

s →^{l} t iff g(s) ⇝^{h(l)}_{∘} g(t)

and, further, for every u ∈ ω,

g(s) ⇝^{h(l)}_{∘} u implies (∃t ∈ S) g(t) = u .

The latter is a form of “end extension” condition, that is essential for g to be a bisimulation. The requirement in a bisimulation that h be the identity is not much of a restriction when there is only one label. Let us be careful about taking the matter of labelling for granted, however, as a great deal of complexity can be shoved over there. For example, consider the embedding

(†) A ↦ {(s_{0}, n, √) | n ∈ A}

of a set A into the transition predicate above with two states s_{0} and √. An obvious consequence of this is

Proposition 8. There is a Π_{1}^{0} strongly extensional transition predicate without a copy in ⇝ (or ⇝_{∘}).

The embedding (†) contrasts with the other more interesting extreme studied in Aczel [1] where the transition predicate is unlabelled (or, if one prefers, |L| = 1) and taken as ∈^{−1} (i.e., {(a, l, b) | b ∈ a} for some fixed l). We will presently consider a more moderate position, to get a sense of how to pass between these two extremes. In particular, the notion of a copy will be relativized to the (computer science) notion of a trace. A trace is, in its simplest form, a sequence (l_{1}, l_{2}, …, l_{n}) of labels on successive transitions

s →^{l_{1}} s_{1} & s_{1} →^{l_{2}} s_{2} & ⋯ & s_{n−1} →^{l_{n}} s_{n}

where s_{n} is a “terminal” state. A terminal state is not meant here to be (necessarily) any element of the set

{s ∈ S | ¬(∃l, t) s →^{l} t} ,

which is co-r.e., assuming → is r.e. Rather, we have in mind a more effective set of states, that can be marked by introducing a fresh label √ and postulating that for all states s and t,

s →^{√} t iff s = t and s is terminal.

This modification to the transition predicate cannot spoil its r.e. character, assuming the terminal states form an r.e. set. Nor can the map ·_{tr} that sends → to the relation →_{tr} consisting of triples (s, (l_{1}, l_{2}, …, l_{n}), t) such that

√ ∉ {l_{1}, l_{2}, …, l_{n}} & t →^{√} t &

(∃s_{1}, …, s_{n−1}) s →^{l_{1}} s_{1} & s_{1} →^{l_{2}} s_{2} & ⋯ & s_{n−1} →^{l_{n}} t .

(Since →_{tr} is r.e. if → is r.e., ·_{tr} can be interpreted within ⇝.) A transition predicate → is now said to have a trace-equivalent copy in →′ if →_{tr} has a copy in →′_{tr}. Observe that trace-equivalence is coarser than bisimilarity.

Moving some of the complexity away from the labelling, the argument (†) behind Proposition 8 can be used for

Proposition 8′. (i) There is a well-founded Π_{1}^{0} transition predicate with |L| = 2 that has no trace-equivalent copy in ⇝.

(ii) There is a Π_{1}^{0} transition predicate with |L| = 2 and branching bound 2 (i.e., for all n |{m | (∃l) n →^{l} m}| ≤ 2) that has no trace-equivalent copy in ⇝.

(iii) There is a strongly extensional Δ_{2}^{0} transition predicate with |L| = 2 that has no trace-equivalent copy in ⇝.

Proof. The idea is to code a subset A of ω into a transition predicate →_{A} which has a copy in ⇝ only if for some fixed label l ≠ √, there is an s such that for all n < ω,

n ∈ A iff (∃t) s ⇝^{l} [t]_{0} & [t]_{0} ⇝^{l} [t]_{1} & ⋯

& [t]_{n−1} ⇝^{l} [t]_{n} & [t]_{n} ⇝^{√} [t]_{n} ,

where [t]_{i} gives the ith component of the finite sequence encoded (under some effective scheme) as t. Note that the above equivalence implies A is r.e. Now, given a binary 1-1 primitive recursive function ⟨·, ·⟩ from ω × ω into ω − {0}, define for (i),

→_{A} = {(0, l, ⟨n, n⟩) | n ∈ A} ∪
{(⟨n, m⟩, l, ⟨n, m − 1⟩) | n ∈ A and 0 < m ≤ n}
∪ {(⟨n, 0⟩, √, ⟨n, 0⟩) | n ∈ A} ,

while for (ii),

→_{A} = {(⟨0, n⟩, l, ⟨0, n + 1⟩) | n < ω} ∪
{(⟨0, n⟩, l, ⟨1, n⟩) | n ∈ A}
∪ {(⟨1, n⟩, √, ⟨1, n⟩) | n ∈ A} .

Note that we cannot require →_{A} (for arbitrary A ⊂ ω) to be both wellfounded and finitely branching (by König) as every finite transition predicate has a copy in ⇝.

As for (iii), let us reduce the transition predicate given by case (i) by choosing representatives of \underline{↔}-equivalence classes as follows. Given an m less than some element of A, let m_{A} be the least x ∈ A that is ≥ m. Note that for m ∈ A, m_{A} = m. Now, set →_{A} to

{(0, l, ⟨n, n⟩) | n ∈ A} ∪ {(⟨a_{0}, 0⟩, √, ⟨a_{0}, 0⟩)} ∪
{(⟨m_{A}, m⟩, l, ⟨(m − 1)_{A}, m − 1⟩) | m > 0 and m is less

than some element of A}

where a_{0} is the least element of A. Observe that x = m_{A} iff x ∈ A & x ≥ m & (∀y < x)(y ∈ A ⊃ y < m), whence →_{A} is Δ_{2}^{0}. ⊣

Next, taking up the case |L| = 1, let us mention two features of a strongly extensional copy ⇒ of ⇝ that would seem to render it unsuitable for a settheoretic characterization (as in Aczel [1] or Barwise, Gandy and Moschovakis [3]). We have in mind here, of course, a restriction of the transition predicate to one label, which we henceforth ignore. Let V = {a | (∃b) a ⇒ b or b ⇒ a}.

(i) A “universal” set exists — i.e., there is an a in V such that a ⇒ b for every b in V. (This a is the copy of state 0 in the r.e. transition predicate {(0, n + 1) | n ∈ ω} ∪ {(n + 1, m + 1) | n ⇝ m} obtained by “rooting” ⇝.)

(ii) V is not closed under very simple comprehension schemes: V contains an x = {x}∪ω_{1}^{CK} but not ω_{1}^{CK} ⊂ x. (This is an immediate consequence of Π_{1}^{1} paths through O and Σ_{1}^{1} boundedness.)

3.3. The question of strongly extensional Π_{1}^{1} approximations. An example of a strongly extensional copy ⇒ of ⇝ is ⇝_{∘} restricted to the set

A_{0} = \{s ∈ ω | (∀s′ < s) s′ \underline{↮}s\}

of least \underline{↔}-representatives. That is, for all s, l, t ∈ ω,

s ⇒^{l} t iff (∃t′\underline{↔}t) s ⇝^{l} t′ & (∀s′ < s) s′ \underline{↮}s &
(∀t′ < t) t′ \underline{↮}t .

Whether ⇒ (or any other strongly extensional copy of ⇝) is Π_{1}^{1} is not known by the present author. The problem is that the first conjunct ⇝_{∘} is Σ_{1}^{1} − Π_{1}^{1}. But now, just as a Π_{1}^{1} path through O can be built from a relativization O^{∗} of O to hyperarithmetic sets, we might consider a notion of pseudo-bisimilarity defined up to hyperarithmetic sets. Given a transition system ⟨L, S, →⟩, with L, S ⊆ ω, define the binary relation ∼ on S by

a ∼ b iff there is a hyperarithmetic bisimulation

relating a to b .

Proposition 9. ∼ is a bisimulation, and, if → is Δ_{1}^{1}, is Π_{1}^{1}.

An obvious Π_{1}^{1} approximation of ⇒ is then {(s, l, t) | s →^{l}/∼ t and s, t ∈ A}, for some Δ_{1}^{1} copy → of ⇝, and some “suitable” Π_{1}^{1} set A. More precisely, a subset A of ω is a suitable representation if

(S1) (∀s ∈ ω)(∃!a ∈ A) a \underline{↔} s
(S2) (∀a ∈ A)(∀b, l s.t. a →^{l} b)(∃c ∈ A) c \underline{↔} b & a →^{l}/∼ c .

Note that (S1) determines a function f_{A}, in terms of which (S2) becomes

(∀a ∈ A)(∀b, l s.t. a →^{l} b) a →^{l}/∼ f_{A}(b) .

For a Π_{1}^{1} suitable representation A, Theorem 7 implies that f_{A} cannot be Π_{1}^{1}. Returning to the set A_{0} of least \underline{↔}-representatives, note that A_{0} is Π_{1}^{1} and (with → = ⇝) meets (S1) by a function that is not manifestly Π_{1}^{1}. Unfortunately, it is unlikely that A_{0} meets (S2) in view of Proposition 10. For all a, b ∈ O^{∗} − O, if a ≻ b then a ≁ b (although a \underline{↔} b).

Proof. Otherwise, construct a hyperarithmetic descending sequence from a, appealing to

a ≻ b and a ∼ b implies (∃c ≺ b) b ∼ c ,

and repeatedly choosing the first c according to some enumeration of ≻. ⊣

That is, a suitable representation (relative to ⇝) cannot contain an element a of O^{∗} − O. This is easily repaired, however; replace a by an a′ bisimilar to a with a′ ≻ a′. Thus, one might try to build successive improvements A_{n+1} of A_{n}, with A = lim_{n→∞} A_{n} (i.e., s ∈ A iff (∃N)(∀n > N) s ∈ A_{n}). Alternatively, we might focus on beefing up →^{0} = ⇝/∼ into a Π_{1}^{1} set →_{ω}= ⋃_{n<ω} →^{n} such that for all a, a′ ∈ A_{0},

(∀b, l) a ⇝^{l} b & b \underline{↔} a′ ⊃ a →^{l}_{ω} a′ ,

a Π_{1}^{1} condition suggesting that a strongly extensional copy of ⇝ be formed from restricting →_{ω} to A_{0}. A combination of improvements on A_{0} and ⇝/∼ might be required, but alas, the author has been unable to carry some such construction to completion.

4. Discussion

The preceding is in no small measure inspired by Feferman [7], which concludes with the remark

... I think that it can be argued that — whatever a “fundamental” theory may tell us is the basic or underlying mechanism for given technological processes or systems — it is necessary for our design and use of such to think of them at various conceptual levels and with various modular forms of organization, that is we must think of them in structural terms. The story of Turing’s “oracle” and its significance for actual computability is but one example among many of this characteristic modus operandi of human intelligence.

While transition predicates constitute “but one example among many” possible formulations of “conceptual levels”, the generality of that approach is promising. Furthermore, that generality can be grounded in processes that are mechanical inasmuch as their transitions can be programmed. Construed in ordinary recursion-theoretic terms, the transitions that can be programmed are based on process names (i.e., syntax) and may fail to be substitutive with respect to non-trivial notions of process equality (requiring, as that does, computational notions for sets — i.e., equivalence classes — rather than for natural numbers). Instead, a weaker form of substitutivity is provided by the (key) concept of a bisimulation (applied to a transition system where programs are states), from which a natural notion of process equality is then derived. The highly uncomputable character of the resulting logical abstractions should not disturb us so long as we do not confuse reasoning about mechanical computation with carrying out a mechanical computation. Recall how the “absolute” character of Church’s thesis contrasts with the “relative” character of Gödel incompleteness (i.e., consistency). “The necessity for intuition” in Turing [21] cannot be “eliminated”; rather, the ineluctability of partiality leads to relative computability and various notions of consistency.

References

[1] Peter Aczel. Non-Well-Founded Sets. CSLI Lecture Notes Number 14, Stanford, 1988.

[2] J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.

[3] J. Barwise, R.O. Gandy, and Y.N. Moschovakis. The next admissible set. Journal of Symbolic Logic, 36(1), 1971.

[4] Jon Barwise. Admissible Sets and Structures. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1975.

[5] D. Bjørner, A.P. Ershov, and N.D. Jones. Partial Evaluation and Mixed Computation. Elsevier, IFIP, 1988.

[6] Solomon Feferman. Turing in the land of 0(z). In R. Herken, editor, The Universal Turing Machine. Kammerer and Unverzagt, 1988.

[7] Solomon Feferman. Turing’s “oracle”: from absolute to relative computability and back. In the proceedings of a symposium on Structures in Mathematical Theories, San Sebastian, Spain, 1990.

[8] Tim Fernando. Provably recursive programs and program extraction. In J. Leach Albert et al, editor, Proc. ICALP ‘91, LNCS 510. Springer-Verlag, Berlin, 1991. A revision of the paper (entitled simply ‘Provably recursive programs’) appears as CWI Technical Report CS-R9212, Amsterdam, March 1992.

[9] Tim Fernando. Bisimulations and predicate logic. Technical Report CS-R9333, Centre for Mathematics and Computer Science (CWI), Amsterdam, May 1993. A revision has been accepted for publication in the Journal of Symbolic Logic.

[10] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, 1989.

[11] Jean-Yves Girard. Proof Theory and Logical Complexity, volume 1. Bibliopolis, Napoli, 1987.

[12] Kurt Gödel. Remarks before the Princeton bicentennial conference on problems in mathematics. In S. Feferman et al, editor, Collected Works, volume II. Oxford University Press, 1990.

[13] Serge Grigorieff. Every recursive linear ordering has a copy in DTIME-SPACE(n, log(n)). Journal of Symbolic Logic, 55(1), 1990.

[14] Stephen Cole Kleene. On the interpretation of intuitionistic number theory. Journal of Symbolic Logic, 10, 1945.

[15] Georg Kreisel. On the interpretation of non-finitist proofs, i. Journal of Symbolic Logic, 16(4), 1951.

[16] Robin Milner. Communication and Concurrency. Prentice Hall, 1989.

[17] Yiannis N. Moschovakis. Elementary Induction on Abstract Structures. North-Holland, Amsterdam, 1974.

[18] Yiannis N. Moschovakis. A model of concurrency with fair merge and full recursion. Information and Computation, 93(1), 1991.

[19] David Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, Proc. 5th GI Conference, LNCS 104. Springer-Verlag, Berlin, 1981.

[20] Gordon D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.

[21] Alan Turing. Systems of logic based on ordinals. Proc. London Math. Soc., 45, 1939.

48 Tim Fernando