λ-calculus as a foundation of mathematics

Klaus Grue^{∗}

August 28, 1997

Abstract

Church introduced λ-calculus in the beginning of the thirties as a foundation of mathematics and map theory from around 1992 fulfilled that primary aim.

The present paper presents a new version of map theory whose axioms are simpler and better motivated than those of the original version from 1992. The paper focuses on the semantics of map theory and explains this semantics on basis of κ-Scott domains.

The new version sheds some light on the difference between Russells and Burali-Fortis paradoxes, and also sheds some light on why it is consistent to allow non-well-founded sets in a ZF-style system.

∗DIKU, University of Copenhagen, Universitetsparken 1, DK-2100 Copenhagen, Denmark, E-mail grue@diku.dk

Contents

1 Introduction 3 1.1 Differences with Churchs approach . . . . . . . . . . . . . . . . . 4 1.2 Inclusion of non-functions . . . . . . . . . . . . . . . . . . . . . . 4 1.3 Set abstraction versus λ-abstraction . . . . . . . . . . . . . . . . 5 1.4 Selection of well-behaved maps . . . . . . . . . . . . . . . . . . . 5 1.5 Relation between MTW and MTC . . . . . . . . . . . . . . . . . 5 1.6 The structure and contents of the paper . . . . . . . . . . . . . . 7

2 The semantics of MTC 7 2.1 Maps over finite sets . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2 Modelling of maps . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.3 Partially ordered sets . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.4 κ-continuity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.5 Maps over R and maps over maps over R . . . . . . . . . . . . . 11 2.6 κ-premodels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.7 Classical maps . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

3 Presentation of MTC 13 3.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.2 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.3 Truth, equality and application . . . . . . . . . . . . . . . . . . . 14 3.4 Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.5 Selection . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.6 Simple existential quantification . . . . . . . . . . . . . . . . . . . 16 3.7 Hilberts ε-operator . . . . . . . . . . . . . . . . . . . . . . . . . . 16

4 Conclusion 17

A Outline of a model of MTC 18 A.1 The κ-denotational semantics . . . . . . . . . . . . . . . . . . . . 18 A.2 Outline of a model . . . . . . . . . . . . . . . . . . . . . . . . . . 19

B Summary of MTC 21 B.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 B.2 Priority . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 B.3 Associativity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 B.4 Definitions used in axioms . . . . . . . . . . . . . . . . . . . . . . 21 B.5 Axioms and inference rules . . . . . . . . . . . . . . . . . . . . . 23

Index 25

References 27

1 Introduction

As mentioned in the abstract, Church introduced λ-calculus [4, 5, 6] in the beginning of the thirties as a foundation of mathematics and map theory from around 1992 fulfilled that primary aim.

In the meanwhile, λ-terms have shown very useful for expressing semantics in computer science, but there has been no natural choice of a theory for reasoning about these λ-terms.

In the lack of such a natural choice, computer science has turned to syntactic methods in which one reasons about the structure and conversion of λ-terms rather than their meaning.

Mathematics, on the contrary, has had set theory which allows to reason about sets rather than syntax. Set theory offers the luxury of referential transparency, in which every term has a meaning and every term implicitly denotes that meaning.

Map theory resembles set theory in that it assigns meaning to λ-terms and treats λ-terms in a referentially transparent fashion. Map theory also resembles set theory when comparing metamathematical power: For every consistent set theory Z there is a consistent map theory M more powerful than Z and vice versa. The deepest difference between set and map theory shows up in the treatment of infinite looping: Russell’s sentence {x | x ∉ x} ∈ {x | x ∉ x} is just a term that takes infinitely long time to compute, but set theory deals with this sentence by forbidding it rather than taking its value serious. Map theory, on the contrary, assigns meaning to the corresponding term (λx.¬(xx))(λx.¬(xx)).

Map theory is not a marriage of convenience between λ-calculus and set theory [7]. Rather, map theory is a theory based entirely on λ-calculus in which, among other, set membership, logical connectives, and quantification over all sets are definable concepts and in which all axioms and inference rules of ZFC are provable without resort to any syntactical considerations.

Map theory has the potential to serve as a foundation of both mathematics (due to its power that is equivalent to that of set theory) and of computer science (due to its treatment of λ-terms). Set and map theory are both inherently difficult to learn due to their level of abstraction, but set theory has the advantage of a century of pedagogical engineering that has made it easier to approach. On the contrary, the version of map theory from 1992 appears as a somewhat random collection of axioms that accidentally have the power of set theory and accidentally describe λ-terms.

Since 1992 it has turned out, however, that map theory is a natural choice of a theory of λ-calculus. More specifically, it has turned out that every sufficiently large so-called κ-Scott domain D for which D ≅ [D → D] ⊕_{⊥} 1 where 1 is a one-element set contains a model for map theory [2]. When Dana Scott invented what is now known as Scott domains he was fully aware that the notion could be generalised to κ-Scott domains, but did not publish this finding as he saw no application of them at that time. Hence, in some sense, a λ-based foundation of mathematics has been around for a long time without anybody recognising it.

The present paper presents a new version of map theory which will be referred to as MTC (Map Theory with Classical maps) as opposed to the version from 1992 which will be referred to as MTW (Map Theory with Well-founded maps). The axioms of MTC are simpler and better motivated than those of MTW. The step from MTW to MTC is intended as a step in the direction of a theory that is easier to learn and teach. The paper focuses on the semantics of MTC and explains this semantics on basis of κ-Scott domains.

1.1 Differences with Churchs approach

It is a pity that Church did not find a theory like map theory right away since that could have saved a lot of work in computer science. There are, however, three good reasons why that did not happen, and these reasons are stated in the next three sections.

1.2 Inclusion of non-functions

The first reason is that Churchs theory may be seen as a theory about functions only, and as such is a theory about only one concept. Classical logic is built around the distinction between truth and falsehood, i.e. the semantic distinction between two concepts. The semantic nature of classical logic and set theory stems from this distinction. λ-calculus, on the contrary, deals with functions only, and in a theory with only one concept it is impossible to make a semantic distinction. For that reason, λ-calculus can merely deal with the provability or non-provability of the equivalence of λ-terms which is syntactic of nature.

In map theory, this problem is solved by insisting that the universe of map theory must contain at least one non-function. Just one non-function is enough to make a distinction, namely a distinction between functions and non-functions. In map theory, the minimalistic approach has been taken to include only one non-function.

Having both functions and non-functions in map theory allows to represent truth and falsehood, and the convention has been chosen to let functions represent falsehood and let non-functions represent truth. This convention has been chosen very carefully on basis of what makes definitions inside map theory easiest to read, but this issue will not be treated here.

Since there is only one non-function in map theory, it is convenient to introduce a name for that non-function, and since the non-function represents truth, the name T has been chosen.

In addition to functions and non-functions, the universe of map theory contains an element which is neither a function, nor a non-function. That element is denoted ⊥ and represents infinite looping. This element violates the axiom of Tertium Non Datur, which in this context says that every object is either a function of a non-function. Nevertheless map theory is still classical of nature because it has another axiom called Quartum Non Datur which says that any map is either a function or T or ⊥, there is no fourth possibility.

The inclusion of the non-function T in map theory is a trivial step, but it is a step that is very important for the semantic nature of the theory.

1.3 Set abstraction versus λ-abstraction

Set theory has set abstraction {x | p(x)} and λ-calculus has λ-abstraction λx.p(x). It is tempting to identify the two kinds of abstraction and try to represent the class {x | p(x)} by λx.p(x), i.e. to represent classes by their characteristic functions. This approach, however, has not succeeded, and set abstraction and λ-abstraction seem to be two completely different kinds of abstraction.

In map theory, a function g does not represent the class {x | g(x) = T}. Rather, g represents the class {g(x) | x ∈ S} where S is a fixed class of maps. In MTW, S is the class W of well-founded maps, and in MTC, S is the class C of classical maps. {g(x) | x ∈ S} contains at least one element, so to allow to represent the empty set, the non-function T is taken to represent that set.

With this encoding, all sets of ZFC can be represented by well-founded maps in MTW and by classical maps in MTC. And, opposite, all well-founded maps in MTW and all classical maps in MTC represent sets. Classes may also be represented, but they are represented by maps that are not well-founded/classical.

In conclusion, the non-identification of set abstraction and λ-abstraction has been an important point in turning λ-calculus into a foundation.

1.4 Selection of well-behaved maps

The third problem in turning λ-calculus into a foundation of mathematics was to find a class S of maps that was sufficiently well-behaved to represent the sets of ZFC. In MTW, the class W of well-founded maps was chosen and in MTC, the class C of classical maps was chosen.

Insisting that {g(x) | x ∈ S} should be a set of ZFC for all g ∈ S puts many restrictions on S, and insisting that all sets of ZFC should be representable by an element of S puts strong requirements on the size and richness of S. Nevertheless, these restrictions by no means determine S uniquely, and finding a natural S is no trivial task.

1.5 Relation between MTW and MTC

One advantage of MTC over MTW is that eleven complicated axioms and inference rules that describe well-foundedness in MTW has been replaced by a single definition of classicality in MTC.

Another advantage is that MTC contains some inference rules that were missing in MTW. These are rules Y, M and E in Appendix B.5. In particular, rule Y says that the fixed point operator generates a minimal fixed point. It is interesting that the theorem of transfinite induction is provable in MTC from the minimality of fixed points combined with the recursive definition of classicality used in MTC. The details are worked out in [12].

A third advantage is the distinction between discontinuous and continuous occurrences of variables introduced in Section 3.1 which allows to treat equations as terms. The syntax of MTW specifies the syntax of terms and well-formed formulas. MTC is simpler in that it does not distinguish between terms and well-formed formulas. This may turn out to be convenient in computer assisted proof systems for MTC because it allows to represent both theorems and inference rules as terms. The notion of discontinuous occurrences permits the inference rule a = T ⊢ a which is also valid in the systems of Feferman [8] and Flagg and Myhill [10]. The notion of discontinuous occurrences also permits the opposite rule a ⊢ a = T. The distinction between discontinuous and continuous occurrences of variables seems to be new way to deal with the anomalies of equality.

MTW and MTC may be compared both on a syntactic and a semantic basis. A syntactic comparison is made in [12] with the following result:

If the classicality predicate of MTC is used to simulate the well-foundedness predicate in MTW, then all axioms and inference rules of MTW except Axiom Well-2 in [11] are provable in MTC. Axiom Well-2 in MTW is disprovable in MTC, which is just a consequence of the slight difference between wellfoundedness and classicality. In [11], Axiom Well-2 is only used to prove Lemma C-K and Lemma C-P, both of which are provable in MTC. Hence, all theorems of MTW proved in [11] are also provable in MTC.

Among other, [11] proves all axioms and inference rules of ZFC in MTW. Combining these observations we have that all axioms and inference rules of ZFC are provable in MTC. This shows that MTC is adequate as a foundation of mathematics (provided ZFC is considered adequate).

MTW and MTC may also be compared semantically. This paper introduces the semantics of MTC by means of a κ-Scott domain D = (D, ≤) where D is the universe of all maps and ≤ is a partial order on all maps. The κ-Scott domain used has the property that it models both MTW and MTC, so it makes sense to compare MTW and MTC in this particular model. A class A of maps will be said to be “coherent” if any two elements of A has an upper bound in D. The correspondence between the classes W and C of well-founded and classical maps, respectively, may now be formulated as follows:

• Any well-founded map is classical.

• Any non-empty, coherent class of well-founded maps has a greatest lower bound, and that greatest lower bound is classical.

• Any classical map is the lower bound of a coherent class of well-founded maps.

Hence, the class C of classical maps can be seen as the closure of W under greatest lower bounds of non-empty, coherent sets. An important difference between W and C is:

• For all well-founded maps g except T there exists a well-founded map h such that h < g.

• For all classical maps g there exists a minimal classical map h such that h ≤ g (h is a minimal classical map if h′ ≤ h ⇒ h′ = h for all classical maps h′).

1.6 The structure and contents of the paper

Section 2 describes the semantics of MTC based on the κ-denotational framework developed in [2]. Section 3 gives a rather quick tour through the syntax, axioms and inference rules of MTC. Section 4 concludes by remarks on Russells and Burali-Fortis paradoxes and non-well-founded sets. Appendix A outlines a model of MTC based on the model of MTW in [2]. Merely the definition of the model is stated. The satisfaction of the axioms and inference rules remains to be proved. Appendix B summarises MTC.

A more detailed description of the individual axioms and inference rules and explanations of how they are used may be found in [12]. Note that the system in [12] contains an inconsistent axiom as pointed out by Chantal Berline. [12] plus errata may be obtained from //www.diku.dk/~grue.

2 The semantics of MTC

2.1 Maps over finite sets

In the following, words in italics and mathematical concepts in boxes occur in the index. Figure 1 shows a map over the set I = {1, 2, 3}.

[figure: f; t; b; f; t; t; b; 1; 2; 3; 1; 2; 3]

Figure 1: A map over {1, 2, 3}

In general, a map over I is a tree where each node is labelled by t , f or b , where each edge is labelled by an element of I, where each node labelled f has one downward edge for each element of I, and where each node labelled t or b has no downward edges. Maps may be infinitely deep. As an example, Figure 2 shows a map over {1, 2}.

If I is a set, if x ∈ I and if g is a map over I, then we define g applied to x, denoted g′x , to be the subtree of g attached to the edge labelled x that extends downwards from the root of g. As an example, if g is the map in Figure 1 then Figure 3, 4 and 5 shows g′1, g′2 and g′3, respectively.

[figure: f; t; f; f; b; t; f; b; ⋮; 1; 2; 1; 2; 1; 2; 1; 2]

Figure 2: A map over {1, 2}

t

Figure 3: The map T

Application is left associative so that e.g. g′3′1 means (g′3)′1. If g is the map in Figure 1 then g′3′1 is the map in Figure 3. If h is the map in Figure 2 then h′2′1 = h.

The trees in Figure 3 and 4 will be denoted T and ⊥ , respectively. No edges extend downwards from the roots of T and ⊥, so the definition of g′x does not make sense for g = T and g = ⊥. To make g′x defined for all x ∈ I and all maps g over I, we more or less arbitrarily define:

\begin{aligned}T′x & = & T \\ ⊥′x & = & ⊥ \end{aligned}

2.2 Modelling of maps

Let t, f and b be three distinct objects. For all maps g over I we define r(g) to be the label of the root of g. Hence, r(T) = t, r(⊥) = b and r(g) = f for all maps g over I except T and ⊥.

Let I^{<ω} denote the set of finite lists ⟨x_{1}, …, x_{n}⟩ of elements of I. For all maps g over I and all \overline{x} = ⟨x_{1}, …, x_{n}⟩ ∈ I^{<ω} let g[\overline{x}] denote g′x′_{1} ⋯′ x_{n}. As an example, h[⟨2, 1, 2, 1, 2, 1⟩] = h where h is the map in Figure 2. If \overline{x} is the empty tuple ⟨ ⟩, then g[\overline{x}] denotes g itself.

If g is a map over I and if x ∈ I^{<ω}, then r(g[\overline{x}]) will be referred to as the label indexed by \overline{x}. As an example, if g is the map in Figure 1, then the labels indexed by ⟨1⟩, ⟨3⟩ and ⟨3, 3⟩ are t, f and b, respectively. The label indexed by

b

Figure 4: The map ⊥

[figure: f; t; t; b; 1; 2; 3]

Figure 5: A map over {1, 2, 3}

⟨3, 3, 2⟩ is also b as shown by the following:

g[⟨3, 3, 2⟩] = g′3′3′2
= (g′3′3)′2
= ⊥′2
= ⊥

Hence, computation of r(g[⟨3, 3, 2⟩]) depends on the convention that ⊥′x = ⊥.

In general, if r(g[⟨x_{1}, ⋯, x_{m}⟩]) = b then r(g[⟨x_{1}, ⋯, x_{m}, y_{1}, ⋯, y_{n}⟩]) = b. Now for all \overline{x}, \overline{y} ∈ I^{<ω} let \overline{x} · \overline{y} denote the concatenation of the tuples x and y. We have

\begin{aligned}r(g[\overline{x}]) = b & ⇒ & r(g[\overline{x} · \overline{y}]) = b \\ r(g[\overline{x}]) = t & ⇒ & r(g[\overline{x} · \overline{y}]) = t \end{aligned}

These two statements may be combined into one:

r(g[\overline{x}]) ≠ f ⇒ r(g[\overline{x} · \overline{y}]) = r(g[\overline{x}])

Now let L = {t, f, b}. For all functions u let dom u and rng u denote the

domain and range of u, respectively. For all sets G and H let G → H denote the set of functions u for which dom u = G and rng u ⊆ H.

If g is a map over I and if \overline{x} ∈ I^{<ω}, then r(g[\overline{x}]) ∈ L. Two maps u and v over I are considered equal if r(g[\overline{x}]) = r(h[\overline{x}]) for all \overline{x} ∈ I^{<ω}. Hence, a map g may be modelled by the function ĝ ∈ I^{<ω} → L for which ĝ(\overline{x}) = r(g[\overline{x}]) for all x ∈ I^{<ω}. From now on, maps are modelled this way which motivates to define the set M_{I} of maps over I by

M_{I} = \{g ∈ I^{<ω} → L | ∀\overline{x}, \overline{y} ∈ I^{<ω} : (g(\overline{x}) ≠ f ⇒ g(\overline{x} · \overline{y}) = g(\overline{x}))

2.3 Partially ordered sets

A p.o D is a partially ordered set (D, ≤). As an example, L = (L, ≤_{L}) is a p.o where

p ≤_{L} q ⇔ p = b ∨ p = q

For all non-empty sets I, M_{I} = (M_{I}, ≤) is a p.o where

g ≤ h ⇔ ∀x ∈ I^{<ω} : g(x) ≤_{L} h(x)

For all p.o’s D = (D, ≤) define the p.o D^{<ω} by D^{<ω} = (D^{<ω}, ≤^{∗} ) where

⟨x_{1}, …, x_{m}⟩ ≤^{∗} ⟨y_{1}, …, y_{n}⟩ ⇔ m = n ∧ x_{1} ≤ y_{1} ∧ ⋯ ∧ x_{m} ≤ y_{m}

For all p.o’s D = (D, ≤) and E = (E, ≤) let x ∈ D, A ⊆ D and g ∈ D → E be shorthand for x ∈ D, A ⊆ D and g ∈ D → E, respectively.

For all non-empty sets I define ⊥_{I} , T_{I} , F_{I} ∈ M_{I} by

⊥_{I}(⟨x_{1}, …, x_{n}⟩) = b T_{I}(⟨x_{1}, …, x_{n}⟩) = t F_{I}(⟨ ⟩) = f F_{I}(⟨u, x_{1}, …, x_{n}⟩) = t

for all n ≥ 0 and all u, x_{1}, …, x_{n} ∈ I. ⊥_{I} is the unique bottom element of M_{I}. T_{I} and F_{I} are two among many maximal elements.

2.4 κ-continuity

For all sets A and κ, A is said to be κ-small if A has cardinality strictly less than κ. From now on let κ be an infinite set.

An element x of a p.o D = (D, ≤) is said to be an upper bound of A ⊆ D if ∀y∈A : y ≤ x. A subset H ⊆ D is said to be a κ-chain if all κ-small subsets of H have an upper bound in H. In particular, the empty set must have an upper bound in H so any κ-chain is non-empty. A p.o D = (D, ≤) is a κ-cpo if every κ-chain H ⊆ D has a supremum sup H in D. As an example, for all non-empty sets I, M_{I} and (M_{I})^{<ω} are κ-cpo’s. M_{I} is an example of a κ-cpo with a bottom element and (M_{I})^{<ω} is an example of one without.

For all κ-cpo’s D and E, a function g ∈ D → E is said to be κ-continuous if

g(sup H) = sup {g(x) | x ∈ H}

for all κ-chains H ⊆ D. Let [D → E]_{κ} denote the κ-cpo of κ-continuous g ∈ D → E, ordered by pointwise ordering. For all D = (D, ≤) define

\begin{aligned}M_{D}^{κ} & = & \{g∈M_{D} | g ∈ [D^{<ω} → L]_{κ}\} \\ M_{D}^{κ} & = & (M_{D}^{κ}, ≤) \end{aligned}

We shall refer to elements of M_{D}^{κ} as κ-continuous maps over D.

2.5 Maps over R and maps over maps over R

At this point a few examples may show useful. Let R be the set of real numbers, let Z ⊆ R be the set of integers, and let G = (G, ≤) = M_{R} be the p.o of maps over R. We have that Z is R-small since Z has cardinality strictly less than R.

For all A ⊆ R define the characteristic map χ_{A} ∈ G by

χ_{A}(⟨ ⟩)  = f
χ_{A}(⟨u, x_{1}, …, x_{n}⟩) = \{ \begin{matrix}t & if u ∈ A \\ b & otherwise \end{matrix}

As an example of a non-trivial R-chain in G^{<ω} we have

H = {⟨χ_{A}⟩ | A ⊆ R ∧ A is R-small}

The supremum sup H of this chain is ⟨χ_{R}⟩.

Now consider the set M_{G} of maps over G = M_{R}, i.e. of maps over maps over R. For all B ⊆ R define ∀_{B} ∈ M_{G} by

∀_{B}(⟨ ⟩)  = f
∀_{B}(⟨u, x_{1}, …, x_{n}⟩) = \{ \begin{matrix}b & if ∃v∈B : u(⟨v⟩) = b \\ t & if ∀v∈B : u(⟨v⟩) = t \\ F_{G}(x_{1}, …, x_{n}) & otherwise \end{matrix}

∀_{B} satisfies

∀_{B}′u = \{ \begin{matrix}⊥_{G} & if ∃v ∈ B : u′v = ⊥_{R} \\ T_{G} & if ∀v ∈ B : u′v = T_{R} \\ F_{G} & otherwise \end{matrix}

If we take T, F and ⊥ to represent truth, falsehood and undefined, respectively, then ∀_{B} represents a universal quantifier that quantifies over B. The quantifier is strict in the sense that ∀_{B}g is undefined if gx is undefined for some x ∈ B.

We have ∀_{R}(sup H) = t and sup {∀_{R}(x) | x ∈ H} = b which shows that ∀_{R} is R-discontinuous. On the contrary it is straightforward to prove that ∀_{Z} is R-continuous (the proof is a somewhat lengthy proof by cases, but the point in the proof is that for all R-chains H′ there exists a function h′′ ∈ H′ such that ∀n∈Z: h′′(n) = h′(n) where h′ = sup H′). In general, ∀_{B} is R-continuous if and only if B is R-small. Even more generally, quantification over a set B is κ-continuous if and only if B is κ-small.

2.6 κ-premodels

We have now seen maps over {1, 2, 3}, maps over R and R-continuous maps over maps over R. The maps of MTC are κ-continuous maps over maps of MTC. In other words, the domain D of all maps of MTC satisfies D ≅ M_{D}^{κ}.

If D is a κ-Scott domain [2], if σ is a strongly inaccessible ordinal [3], if κ is a regular cardinal [3] greater than σ and if D ≅ M_{D}^{κ} then it follows from [2] that D can be expanded into a model of MTW (to see that one needs to prove D ≅ M_{D}^{κ} ⇒ D ≅ [D → D]_{κ} ⊕_{⊥} {T_{D}}; then let A ∈ D → [D → D]_{κ} ⊕_{⊥} {T_{D}} be an order isomorphism, let λ be the inverse of A and apply Theorem 7.2.1 in [2] to (D, A, λ)).

A model of MTC needs to satisfy more than this, partly because of the classical maps, partly because MTC contains inference rules that were missing in MTW.

From now on assume that there exist strongly inaccessible ordinals, assume that σ is the least strongly inaccessible ordinal and assume that κ is a regular cardinal greater than σ.

A κ-premodel P of MTC is a structure (D, a, C, q) which satisfies the five properties below plus one more property which is stated in Section 2.7.

• D = (D, ≤) is a κ-Scott domain (and, in particular, a κ-cpo)

• a ∈ [D → M_{D}^{κ}]_{κ} is an isomorphism

• C ⊆ D is a κ-small set of so-called κ-compact elements (c.f. [2] and Appendix A.1).

• q is a choice function over D, i.e. q(A) ∈ A for A ⊆ D, A ≠ ∅

• q(∅) ∈ C

κ-premodels are introduced here to present the intuitions behind MTC. The construction of a κ-premodel is outlined later. The detailed development and the verification of axioms and inference rules of MTC remains to be done. Now define

\overline{a} is the inverse of a T = \overline{a}(T_{D})

⊥ = \overline{a}(⊥_{D})

F = \overline{a}(F_{D})

For all g, x ∈ D let g′x be the unique element of D for which

a(g′x)(⟨y_{1}, …, y_{n}⟩) = a(g)(⟨x, y_{1}, …, y_{n}⟩)

This defines the notion of applying a map g to an argument x which was first mentioned in Section 2.1. This concludes a circle: informal considerations about application of maps led to a representation of maps which was refined into a model of maps which allows to define application.

2.7 Classical maps

For all S ⊆ D and x, y ∈ D define x =_{S} y ⇔ ∀z ∈ S^{<ω}: a(x)(z) = a(y)(z). For

all x, y ∈ D^{<ω} define x =_{S}^{∗} y by

⟨x_{1}, ⋯, x_{m}⟩ =_{S}^{∗} y⟨y_{1}, ⋯, y_{n}⟩ ⇔ m = n ∧ x_{1} = y_{1} ∧ ⋯ ∧ x_{m} = y_{m}

Let P_{σ}(A) denote the set of σ-small subsets of A. Let C′ be the least subset of D which satisfies

\begin{aligned}g ∈ C′ & ⇔ & ∀x ∈ C : g′x ∈ C′ ∧ \\ & & ∃V ∈ P_{σ}(C′)∀x, y ∈ C^{<ω}: (x =_{V}^{∗} y ⇒ a(g)(x) = a(g)(y)) \end{aligned}

The existence of such a C′ is easy to verify. For all x ∈ D and A ⊆ D let

↑x = {y ∈ D | x ≤ y} and ↑A = ⋃{↑x | x ∈ A}. A κ-premodel P of MTC is

a structure (D, a, C, q) which satisfies the five properties in Section 2.6 plus the one below:

• C′ = ↑C

3 Presentation of MTC

3.1 Syntax

The syntax V of variables and T of terms of MTC reads:

\begin{aligned}V & ::= & x_{1} | x_{2} | ⋯ \\ T & ::= & V | T | T T | λV.T | P | ε | ¯∃ | ϵ(T ) | T = T \end{aligned}

The construct T T has higher priority than λV.T , which in turn has higher priority than T = T , so that e.g. λx_{1}.x_{1}x_{1} = x_{2} means (λx_{1}.(x_{1}x_{1})) = x_{2}.

An occurrence of a variable v in a term t is said to be discontinuous if v occurs free in a subterm t′ of t which has one of the forms ϵ(t′′) or t′′ = t′′′. Occurrences that are not discontinuous are said to be continuous. As an example, the second occurrence of x_{1} in Px_{1}x_{2}(x_{1} = λx_{1}.x_{1}) is discontinuous whereas the other occurrences of variables are continuous.

The following purely syntactical restriction is put on terms of MTC: Discontinuous occurrences of variables are not allowed to be bound. As an example, λx_{1}.(x_{1} = T) is not a well-formed term.

3.2 Proofs

A proof in MTC is a sequence of terms in which each term is either an instances of an axiom scheme of follows from previous terms in the sequence by an inference rule. All axioms and inference rules of MTC are listed in Appendix B.5.

The interpretation of a proof is that it proves the last term in the proof, i.e. it proves that the last term in the proof equals T for all values of free variables.

3.3 Truth, equality and application

The term T in Section 3.1 denotes the value T defined in Section 2.6. The term a = b equals T when a equals b and a = b equals F otherwise. The value of a = b may depend on the values of free variables in a and b. As an example, x_{1} = T equals T when x_{1} equals T and equals F otherwise. The inference rules of truth and equality read:

T Transitivity a = b; a = c ⊢ b = c.
SA Substitutivity a = c; b = d ⊢ ab = cd.
Sλ Substitutivity a = b ⊢ λx.a = λx.b.
Sϵ Substitutivity a = b ⊢ ϵ(a) = ϵ(b).
=⊢ Equality  a = T ⊢ a
⊢= Equality  a ⊢ a = T

In inference rules, a, b, c, d, g and h denote arbitrary terms whereas x, y and z denote arbitrary, distinct variables.

The inference rule a = T ⊢ a is inspired by [8, 10]. The opposite rule a ⊢ a = T is made possible by the notion of discontinuous occurrences of variables which seems to be a new way of dealing with the discontinuity of equality.

For all terms a and b, ab denotes a applied to b, i.e. ab denotes a′b. Since T applied to anything equals T by convention, we have the axiom

AT Application Ta = T.

As an example of a proof we have

1 AT  Ta = T
2 AT  Ta = T
3 1, 2, T T = T
4 3, =⊢ T

3.4 Abstraction

For all variables x and terms A of ZFC let x ↦ A be shorthand for {(x, A) | x ∈ D}, i.e. let x ↦ A be the unique function g for which dom g = D and g(x) = A. For all g ∈ [D → D]_{κ} let λ(g) be the unique element of D for which

\begin{aligned}λ(g)(⟨ ⟩) & = & f \\ λ(g)(⟨u, x_{1}, …, x_{n}⟩) & = & g(u)(⟨x_{1}, …, x_{n}⟩) \end{aligned}

Finally define

λx.A = λ(x ↦ A)

whenever (x ↦ A) ∈ [D → D]_{κ}, i.e. whenever x ↦ A is a κ-continuous function from maps to maps.

If x is a variable and A is a term of MTC, then (x ↦ A) ∈ D → D. If, furthermore, there are no discontinuous free occurrences of x in A then x ↦ A is κ-continuous so that (x ↦ A) ∈ [D → D]_{κ} and (λx.A) ∈ D. This gives an interpretation of λx.A whenever λx.A is a well-formed term. We may now formulate two more axioms, namely

Aλ Application (λx.a)b = ⟨a | x:=b⟩

if b is free for x in a.

R Renaming λx.⟨a | y:=x⟩ = λy.⟨a | x:=y⟩.

if x is free for y in a and vice versa.

Here ⟨a | x:=b⟩ is the term that arises when replacing all free x in a by b. See [14] for a definition of free for. Axiom R allows renaming of bound variables and Axiom Aλ expresses that two terms are equal if they are β-equivalent. (Note, however, that terms may be equal in map theory without being β-equivalent. This holds even for terms that contain only variables, abstraction and application. The notion of equality in map theory is the semantic notion introduced in Section 2.2 and this semantic notion is not fully captured by β-equivalence).

Having abstraction and application allows to define the fixed point operator Y and the bottom element ⊥:

\begin{aligned}Y & = & λf.(λx.f(xx))λx.f(xx) \\ ⊥ & = & Yλx.x \end{aligned}

Having the bottom element we may state one more axiom and one more inference rule:

A⊥ Application  ⊥a = ⊥.
QND Quartum Non Datur aT = bT; a⊥ = b⊥; aλy.xy = bλy.xy
⊢ ax = bx.

Axiom A⊥ expresses that ⊥ applied to anything yields ⊥. Inference rule QND expresses that the root of any map is t, f or b, there is no fourth possibility. QND together with the map P described in Section 3.5 allows to develop classical propositional calculus (c.f. [11, 2, 12]). In the present paper, only the intended meaning of axioms and inference rules will be stated. The details of why they express the intended meaning and how they are used is stated in [12].

3.5 Selection

The map P is best described by the following three axioms:

PT Selection PabT = a.
Pλ Selection Pabλx.c = b
P⊥ Selection Pab⊥ = ⊥.

The map P allows to define many auxiliary concepts such as logical connectives (c.f. Appendix B.4) and to develop classical propositional calculus on basis of QND.

For a, b ∈ D = (D, ≤), the constructs introduced so far allow to define a ⪯ b such that a ⪯ b equals T if a ≤ b and equals F otherwise. The definition of a ⪯ b is stated in Appendix B.4 and reads

a⪯b ≐ (a = a↓b)

where a↓b is defined on basis of P in Appendix B.4. The definition of ⪯ uses = which is a discontinuous construct in the sense that free occurrences of variables in a = b are discontinuous occurrences. ⪯ inherits the discontinuity from = so that free occurrences of variables in a ⪯ b are discontinuous, and no λ is allowed to bind a variable occurrence that is free in a subterm of form a ⪯ b.

We may now state three further inference rules and one more axiom:

Y Minimality  ga ⪯ a ⊢ Yg ⪯ a.
M Monotonicity b ⪯ c ⊢ ab ⪯ ac.
E Extensionality ≀gxy = ≀hxy; gxyz = gab; hxyz = hab ⊢ gxy = hxy

if x, y and z are not free in g and h

!= Equality  !(a = b)

Rule Y states that Yg is minimal among all fixed points of g (this does not hold in all κ-premodels, but it holds in the particular one outlined in Appendix A). Rule M states that all maps a are monotonic in the sense that b ≤ c implies ab ≤ ac. Rule E states that two maps g and h are equal if a(g)(\overline{x}) = a(h)(\overline{x}) for all \overline{x} ∈ D^{<ω} (see [12] for details on the interpretation and applications of rule E). Axiom != states that a = b is either true or false.

3.6 Simple existential quantification

The quantifier ¯∃ is a particularly primitive quantifier. ¯∃g = T if gx = T for some x ∈ D and ¯∃g = ⊥ otherwise. Contrary to ∃, which is defined in Section B.4, ¯∃g cannot be false. ϵ(g) is an x ∈ D such that gx = T if such an x exists. More formally, define E ∈ D → D by

E(g) = \{ \begin{matrix}T & if ∃x ∈ D: gx = T \\ ⊥ & otherwise \end{matrix}

Then define

\begin{aligned}¯∃ & = & λ(E) \\ ϵ(g) & = & q(\{x ∈ D | gx = T\}) \end{aligned}

Here we use the choice function q from the premodel (D, a, C, q). The requirement q(∅) ∈ C ⊆ D ensures that ϵ(g) is a map even when gx ≠ T for all maps x. The following axioms describe ¯∃:

→¯∃ Existence ab → ¯∃a
¯∃→ Existence ¯∃a → aϵ(a)
?¯∃ Existence ¯∃a = ?¯∃a

Axiom →¯∃ expresses that if ab is true for some particular b, then ¯∃a is true. Axiom ¯∃→ expresses that if ax is true for some x then, in particular, it is true for x = ϵ(a). Axiom ?¯∃ expresses that ¯∃a equals either T or ⊥. See Appendix B.4 for definitions of a → b and ?a.

3.7 Hilberts ε-operator

Define

Q(g) = \{ \begin{matrix}⊥ & if ∃x ∈ C: gx = ⊥ \\ q(\{x ∈ C | gx = T\}) & otherwise \end{matrix}
ε  = λ(Q)

The map ε is Hilberts ε-operator [13]. The map ε allows to define many auxiliary concepts such as the universal and existential quantifiers (c.f. Appendix B.4) and to develop first order predicate calculus. Furthermore, C is rich enough to allow all sets of ZFC to be modelled by classical maps which allows to define set membership and prove all axioms and inference rules of ZFC inside MTC. The details may be found in [11, 12].

The constructs introduced so far allows to define the map ℓ (the definition is stated in Appendix B.4). Now let

C′ = {x ∈ D | ℓx = T}

(this C′ is actually the same C′ as the one defined in Section 2.7). The axioms that describe ε read:

Q1 Quantification ℓa ∧ ∀b → ba
Q2 Quantification εx: a = εx: ℓx ∧ a
Q3 Quantification ℓ(εx: a) = ∀x: !a
Q4 Quantification !∀x: a = ∀x: !a.

Axiom Q1 states C′ ⊆ C and Axiom Q2 states C ⊆ C′ so that C = C′ as in Section 2.7. Axiom Q2 furthermore expresses Ackermanns axiom ([9], p.244). The definition of ε entails that εg ∈ C if ∀x∈C: gx ≠ ⊥ and εg = ⊥ if ∃x∈C: gx = ⊥. The former is expressed directly by Axiom Q3 and the latter is expressed indirectly by Axiom Q4.

4 Conclusion

The most immediate translation of Russells paradoxical sentence {x | x ∉ x} ∈ {x | x ∉ x} into MTC is the term (λx.¬(xx))(λx.¬(xx)) whose value is ⊥. Hence, Russells paradox is essentially avoided by having a third truth value ⊥ which is the value of terms that make a computer loop indefinitely. An important point in MTC is that this third truth value can be introduced without loosing the classical, semantic flavour of the theory and without resort to intuitionistic logic.

The above translation of Russells paradox to MTC translates set abstraction to λ-abstraction, which gives insight to how Russells paradox is avoided. As noted in Section 1.3, set abstraction is not the same as λ-abstraction, so one may also look at how Russells paradox is avoided when modelling set abstraction as in [11]. This turns out to be trivial, however, since that modelling ensures that all sets are well-founded so that all sets x satisfy x ∉ x. Furthermore, that modelling ensures that classes that contain all sets are not sets themselves.

A map x in MTC is classical if ℓx = T where

ℓ ≐ λf.f \{ \begin{matrix}T \\ (∀x: ℓ(fx)) ∧ ¯∃S: ℓS ∧ ∀x∀y: x ∼_{S}^{2} y ⇒ fx ∼ fy \end{matrix}

The precise structure and meaning of this definition is not important here. The important observation is that the definition of ℓ is recursive in that ℓ occurs on the right hand side of ≐ (recursive definitions are shorthand for definitions that use the fixed point operator Y explicitly).

The two occurrences of ℓ in the definition combined with the minimality of fixed points implies that classical maps are well-founded in two, distinct ways. The first occurrence of ℓ makes classical maps well-founded in the sense that for all classical maps g, x_{1}, x_{2}, … there exists an n such that gx_{1} ⋯ x_{n} = T. This kind of well-foundedness corresponds to the well-foundedness of sets expressed by the axiom of restriction in ZFC (no infinitely descending ∈-chains).

The second occurrence of ℓ makes classical maps well-founded in a much more subtle sense. The closest analogue in ZFC to this well-foundedness is the limitation of size present in ZFC. However, maps contain more structure than sets and the second kind of well-foundedness is more a limitation of complexity than just a simple limitation of size. In any case, it is this second kind of well-foundedness that avoids Burali-Fortis paradox.

The first kind of well-foundedness does not avoid paradoxes. If the first kind of well-foundedness is abandoned, if the second kind is kept, and if the representation of sets used in [11] is used, then the representable sets become those of Aczel’s AFA set theory [1] (the one in which the equation X = {X} has exactly one solution). Hence, it is consistent to allow infinite descending ∈-chains because the paradoxes are avoided by the second kind of well-foundedness.

As noted by Aczel, all known theories about non-well-foundedness share the peculiarity that they start by constructing a well-founded universe and then proceed to the non-well-founded. It is an interesting topic for further work to try to formulate a version of map theory which does not share this peculiarity. Such a theory could be a theory about non-well-founded, classical maps, i.e. maps that satisfy the second kind of well-foundedness without satisfying the first.

Acknowledgement

My thanks are due to the referee from who’s report I copied a paragraph to the abstract.

A Outline of a model of MTC

A.1 The κ-denotational semantics

The following exposition follows [2] except that in the following exposition, the empty set is κ-small and κ-cpos need not have a bottom element.

A p.o D is a partially ordered set, (D, ≤). We use x ∈ D and x ⊆ D as shorthand for x ∈ D and x ⊆ D, respectively. ↓u means {v | v ≤ u}. A ⊆ D is κ-chain if every κ-small B ⊆ A is bounded by an element of A. D is a κ-cpo if every κ-chain A has a sup (i.e. least upper bound). D is a κ-ccpo if moreover every bounded A has a sup (hence, like in [2], every κ-ccpo has a bottom). A κ-compact element of a κ-cpo D is an element u ∈ D such that, for all κ-chains A, u ≤ sup (A) implies u ≤ v for some v ∈ A. D_{c} is the set of κ-compact

elements and ↓_{c}u = ↓u ∩ D_{c}. A κ-ccpo D is a κ-Scott domain iff for all u ∈ D, u = sup ↓_{c}u. A prime element of a κ-ccpo D is an element u such that, for all bounded A, u ≤ sup A implies u ≤ v for some v ∈ A. D_{p} is the set of prime

elements of D, and ↓_{p}u = ↓u ∩ D_{p}. A κ-Scott domain is κ-prime algebraic if for all u ∈ D, u = sup ↓_{p}u.

A.2 Outline of a model

A model of MTC is outlined in the following. Merely the definition of the model will be stated. The satisfaction of the axioms and inference rules remains to be proved.

The model construction has many similarities with the construction in Section 8 of [2]. The construction below differs from that in [2] in the following ways: (1) The domain of the model is constructed as coherent, complete, initial segments of κ-compact elements rather than coherent, initial segments of κ-prime elements and the PCS of κ-prime elements is not constructed at all below. (2) The model construction is based on two fixed point constructions rather than one. The first fixed point generates the σ-compact maps of MTW which is a set large enough to contain the well-founded maps of MTW. Then the well-founded maps are turned into classical maps by discarding information, and then a second fixed point construction is used to generate the κ-compact maps of MTC. Finally, the κ-premodel of MTC is constructed from coherent, initial segments of κ-compact elements.

To simplify the exposition, assume that κ is strongly inaccessible, i.e. assume σ is the least strongly inaccessible ordinal and assume κ is a strongly inaccessible ordinal greater than σ. The assumption that κ is inaccessible rather than just regular is merely a luxury.

For all relations ⪯ define ⪯^{∗} by

⟨x_{1}, …, x_{m}⟩ ⪯^{∗} ⟨y_{1}, …, y_{n}⟩ ⇔ m = n ∧ x_{1} ⪯ y_{1} ∧ ⋯ ∧ x_{m} ⪯ y_{m}

An applicative structure D is a pair (D, a) where D is a set and a ∈ D → M_{D}. For applicative structures D = (D, a) define ≤_{D} and M_{D} by

\begin{matrix}x ≤_{D} y ⇔ a(x) ≤ a(y) \\ M_{D} = \{g∈M_{D} | ∀x, y∈D^{<ω}: (x ≤_{D}^{∗} y ⇒ a(g)(x) ≤_{L} a(g)(y))\} \end{matrix}

An applicative structure D = (D, a) is said to be monotonic if ⊥_{D} ∈ rng a ⊆ M_{D}. For all monotonic applicative structures D = (D, a) define

D_{D} = D ∪ M_{D}
a_{D}^{+} ∈ D_{D} → M_{D} a_{D}^{+}(x) = \{ \begin{matrix}a(x) & if x ∈ D \\ x & otherwise \end{matrix}
g ⪯_{D} h ⇔ a_{D}^{+}(g) ≤ a_{D}^{+}(h)
a_{D} ∈ D_{D} → M_{D_{D}} a_{D}(g)(x) = sup {a_{D}^{+}(g)(y) | y ∈ D^{<ω} ∧ y ⪯_{D}^{∗} x}
D^{+} = (D_{D}, a_{D})

To ensure the soundness of the definition, we make the arbitrary convention that sup A = b when A ⊆ L has no supremum.

For applicative structures D = (D, a) and D′ = (D′, a′) define D ⊑ D′ ⇔ D ⊆ D′ ∧ ∀g∈D∀x∈D^{<ω}: a(g)(x) = a′(g)(x). We have D ⊑ D^{+}. Now define D^{α} for all ordinals α by transfinite induction as follows:

D^{0}  = D
D^{α+1} = (D^{α})^{+}
D^{δ}  = ⊔_{α∈δ}D^{α} for limit ordinals δ

Above, ⊔_{α∈δ} has the obvious interpretaion, i.e. if D^{α} = (D_{α}, a_{α}) then D_{δ} = ∪_{α∈δ}D_{α} and a_{δ}(g)(x) = a_{α}(g)(x) whenever g∈D_{α} and x∈D_{α}^{<ω}.

Let ⊥ be an arbitrary element of the universe of ZFC which is not a function, let D_{1} = (D_{1}, a_{1}) where D_{1} = {⊥} and where a_{1} ∈ D_{1} → (D_{1}^{<ω} → L)

is defined by a_{1}(g)(x) = b. Furthermore, let D_{2} = (D_{2}, a_{2}) = D_{1}^{σ}. D_{2} is essentially the set of σ-compact elements of MTW.

Let S^{∞} denote the set of infinite lists of elements of S. For all x = (x_{1}, …) and n ∈ ω let (x|n) denote the tuple ⟨x_{1}, ⋯, x_{n}⟩.

Define G^{∘} = {g∈D_{2} | ∀x∈D_{2}^{∞}∃n∈ω: a_{2}(g)(x|n) = t}, and let Φ be the least subset of D_{2} for which G^{∘∘} ⊆ Φ whenever G ⊆ Φ is σ-small. This Φ is essentially the set of well-founded maps introduced in [2, 11].

Now let D_{3} = (D_{3}, a_{3}) where D_{3} = Φ∪{⊥} and where a_{3} ∈ D_{3} → (D_{3}^{<ω} → L) is defined by a_{3}(g)(x) = a_{2}(g)(x). D_{3} is Φ from which some information is discarded, namely the information about the applicative behaviour of wellfounded maps when applied to non-well-founded maps. This makes D_{3} useful as a model of the classical maps.

Now let D_{4} = (D_{4}, a_{4}) = D_{3}^{κ}. D_{4} is essentially the set of κ-compact elements of MTC. Transfinite induction up to κ gives the κ-compact elements because κ is assumed inaccessible. More care would be needed in the definition of D^{+} and D^{α} if κ was not assumed inaccessible.

A ⊆ D_{4} is an initial segment if A is non-empty and x ≤_{D_{4}} y∧y ∈ A ⇒ x ∈ A. A is coherent if any two elements of A have an upper bound in D_{4}. A is complete if any subset of A that has an upper bound in D also has an upper bound in A. Let D_{5} be the set of coherent, complete, initial segments and define the relation ≤_{5} on D_{5} by x ≤_{5} y ⇔ x ⊆ y. Define a_{5} ∈ D_{5} → (D_{5}^{<ω} → L) by a_{5}(g)(⟨x_{1}, …, x_{n}⟩) = sup {a_{4}(h)(⟨y_{1}, …, y_{n}⟩) | h ∈ g ∧ y_{1} ∈ x_{1} ∧ ⋯ ∧ y_{n} ∈ x_{n}}. Define C_{5} = {↓x | x ∈ D_{3} \ {⊥}} and let q ∈ P(D_{5}) → D_{5} satisfy q(A) ∈ A when A is non-empty and q(A) ∈ C_{5} when A is empty.

P = ((D_{5}, ≤_{5}), a_{5}, C_{5}, q_{5}) is claimed to be a κ-premodel which satisfies all axioms and inference rules of MTC.

B Summary of MTC

B.1 Syntax

\begin{aligned}V & ::= & x_{1} | x_{2} | ⋯ \\ T & ::= & V | T | T T | λV.T | if(T , T , T ) | ε | ¯∃ | ϵ(T ) | T = T \end{aligned}

B.2 Priority

The priority is as follows. Functional application fx has highest priority and appears at the top of the table. Operators on the same line have the same priority.

fx x, y x ↓ y ↓x x ∼ y x∈y x∈∈y x ∼_{S}^{2} y ¬x ≀x !x ?x x ∧ y x ˜∧ y x ∨ y x ˜∨ y x ⇒ y x ˜⇒ y x ⇔ y

x \{ \begin{matrix}y \\ z \end{matrix}

λx.y

x = y x ⪯ y

x → y

B.3 Associativity

fx, x ∧ y, x ˜∧ y, x ∨ y and x ˜∨ y are left associative so that e.g. fxy means (fx)y.

x ∼ y, x∈y, x∈∈y, x ∼_{S}^{2} y, x ⇒ y, x ˜⇒ y, x ⇔ y, x = y, x ⪯ y, and x → y are “and”-associative so that e.g. x ∼ y ∼ z means (x ∼ y) ∧ (y ∼ z) and x ⇒ y ⇒ z means (x ⇒ y) ∧ (y ⇒ z).

B.4 Definitions used in axioms

F  ≐ λx.T

x \{ \begin{matrix}a \\ b \end{matrix} ≐ Pabx

Y  ≐ λf.(λx.f(xx))(λx.f(xx))
⊥  ≐ Yλx.x
¬x  ≐ x \{ \begin{matrix}F \\ T \end{matrix}
≀x  ≐ x \{ \begin{matrix}T \\ F \end{matrix}
!x  ≐ x \{ \begin{matrix}T \\ T \end{matrix}
?x  ≐ x \{ \begin{matrix}T \\ ⊥ \end{matrix}

x ˜∧ y ≐ x \{ \begin{matrix}y \\ F \end{matrix}

x ˜⇒ y ≐ x \{ \begin{matrix}y \\ T \end{matrix}

x ∧ y  ≐ x \{ \begin{matrix}y \{ \begin{matrix}T \\ F \end{matrix} \\ y \{ \begin{matrix}F \\ F \end{matrix} \end{matrix}

x ⇒ y ≐ x \{ \begin{matrix}y \{ \begin{matrix}T \\ F \end{matrix} \\ y \{ \begin{matrix}T \\ T \end{matrix} \end{matrix}

x ⇔ y ≐ (x ⇒ y) ∧ (y ⇒ x) x → y ≐ x ˜∧ y = x ˜∧ T

∃  ≐ λf.≀f(εf)
∃x: a  ≐ ∃λx.a
∀x: a  ≐ ¬∀x: ¬a
∀  ≐ λf.∀x: fx

f ∼ g ≐ f \{ \begin{matrix}g \{ \begin{matrix}T \\ F \end{matrix} \\ g \{ \begin{matrix}F \\ ∀λx.fx ∼ gx \end{matrix} \end{matrix}

x ∈ y ≐ y \{ \begin{matrix}F \\ ∃z: xz ∼ y \end{matrix}

x ∈∈ y ≐ ∃z: x ∈ z ∧ z ∈ y ∀x∈∈a: b ≐ (λy.∀x: x ∈∈ y ˜⇒ b)a

f ∼_{S}^{2} g ≐ f \{ \begin{matrix}g \{ \begin{matrix}T \\ F \end{matrix} \\ g \{ \begin{matrix}F \\ ∀x∈∈S: fx ∼_{S}^{2} gx \end{matrix} \end{matrix}

ℓ  ≐ λf.f \{ \begin{matrix}T \\ (∀x: ℓ(fx)) ∧ ¯∃S: ℓS ∧ ∀x∀y: x ∼_{S}^{2} y ⇒ fx ∼ fy \end{matrix}
x ↓ y  ≐ x \{ \begin{matrix}y \{ \begin{matrix}T \\ ⊥ \end{matrix} \\ y \{ \begin{matrix}⊥ \\ λz.xz ↓ yz \end{matrix} \end{matrix}

x ⪯ y ≐ x = x ↓ y

B.5 Axioms and inference rules

Below, a, b, c, d, f and g denote arbitrary terms whereas x, y and z denote arbitrary, distinct variables.

T  Transitivity  a = b; a = c ⊢ b = c.
SA  Substitutivity  a = c; b = d ⊢ ab = cd.
Sλ  Substitutivity  a = b ⊢ λx.a = λx.b.
Sϵ  Substitutivity  a = b ⊢ ϵ(a) = ϵ(b).
PT  Selection  PabT = a.
Pλ  Selection  Pabλx.c = b
P⊥  Selection  Pab⊥ = ⊥.
AT  Application  Ta = T.
Aλ  Application  (λx.a)b = ⟨a | x:=b⟩

if b is free for x in a.

A⊥ Application  ⊥a = ⊥.
R Renaming λx.⟨a | y:=x⟩ = λy.⟨a | x:=y⟩.

if x is free for y in a and vice versa.

QND Quartum Non Datur aT = bT; a⊥ = b⊥; aλy.xy = bλy.xy

⊢ ax = bx.

Q1  Quantification  ℓa ∧ ∀b → ba
Q2  Quantification  εx: a = εx: ℓx ∧ a
Q3  Quantification  ℓ(εx: a) = ∀x: !a
Q4  Quantification  !∀x: a = ∀x: !a.
Y  Minimality  ga ⪯ a ⊢ Yg ⪯ a.
M  Monotonicity  b ⪯ c ⊢ ab ⪯ ac.
E  Extensionality  ≀gxy = ≀hxy; gxyz = gab; hxyz = hab

⊢ gxy = hxy if x, y and z are not free in g and h

→¯∃ Existence  ab → ¯∃a
¯∃→ Existence  ¯∃a → aϵ(a)
?¯∃  Existence  ¯∃a = ?¯∃a
=⊢  Equality  a = T ⊢ a
⊢=  Equality  a ⊢ a = T
!=  Equality  !(a = b)

Index

(x|n), 20 G → H, 9 G^{∘}, 20 I^{<ω}, 8 S^{∞}, 20 [D → E]_{κ}, 10 Φ, 20 ⊥, 8, 12, 15, 20 ⊥_{I}, 10 κ, 12 ⟨a | x:=b⟩, 15 ≤^{∗}, 10 ≤_{D}, 19 \overline{x} · \overline{y}, 9 ⪯^{∗}, 19 σ, 12 ab, 14 g ≤ h, 10 g′x, 7, 12 x =_{S}^{∗} y, 13 x =_{S} y, 13 D ⊑ D′, 20 D^{<ω}, 10 D^{α}, 20 ↓u, 18 ↑x, 13

\overline{a}, 12 applicative structure, 19 applied to, 7

b, 7

D_{c}, 19 ↓_{c}u, 19 κ-ccpo, 18 κ-chain, 10, 18 κ-compact, 19 continuous, 13 κ-continuous, 10 κ-continuous maps over D, 10 κ-cpo, 10, 18

D_{1}, 20 D_{2}, 20 D_{3}, 20 D_{4}, 20 discontinuous, 13 dom u, 9

F, 12 F_{I}, 10 f, 7 free for, 15

indexed, 8

L, 9

p ≤_{L} q, 10 L, 10

M_{I}, 9 M_{D}, 19 M_{D}^{κ}, 10 M_{I}, 10 M_{D}^{κ}, 10 map, 7 monotonic, 19 MTC, 4 MTW, 4

P_{σ}(A), 13 D_{p}, 19 ↓_{p}u, 19 partially ordered set, 10 p.o, 10 κ-premodel, 12 prime, 19 κ-prime algebraic, 19

r(g), 8

regular cardinal, 11

rng u, 9

κ-Scott domain, 11, 19

κ-small, 10

strongly inaccessible ordinal, 11 sup H, 10 T, 8, 12 T_{I}, 10 t, 7

upper bound, 10

Y, 15

References

[1] P. Aczel. Frege structures and the notions of proposition, truth and set. In J. Barwise, H. J. Keisler, and K. Kunen, editors, The Kleene Symposiom, pages 31–59, Amsterdam, 1980. North-Holland.

[2] C. Berline and K. Grue. A κ-denotational semantics for Map Theory in ZFC+SI. Theoretical Computer Science, 179(1–2):137–202, June 1997.

[3] C. C. Chang and K. J. Keisler. Model Theory, volume 73 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1973.

[4] A. Church. A set of postulates for the foundations of logic I. Ann. Math., 1933.

[5] A. Church. A set of postulates for the foundations of logic II. Ann. Math., 1934.

[6] A. Church. The Calculi of Lambda Conversion. Princeton University Press, 1941.

[7] S. Feferman. Recursion theory and set theory, a marriage of convenience. In J. E. Fenstad, R. O. Gandy, and G. E. Sacks, editors, Generalized Recursion Theory II, Proceedings of the 1977 Oslo Symposium, pages 55–98. North-Holland, 1978.

[8] S. Feferman. Toward useful type-free theories.I. Journal of Symbolic Logic, 49:75–111, 1984.

[9] U. Felgner. Choice functions on sets and classes. In Sets and Classes: On the works by Paul Bernays, pages 217–255. North-Holland, 1976.

[10] R.C. Flagg and J. Myhill. A type-free system extending ZFC. Annals of Pure and Applied Logic, 43:79–97, 1989.

[11] K. Grue. Map theory. Theoretical Computer Science, 102(1):1–133, July 1992.

[12] K. Grue. Stable map theory. DIKU Report 96/10, Department of Computer Science, University of Copenhagen, DIKU, Universitetsparken 1, DK–2100 Copenhagen, Denmark, April 1996. Available from //www.diku.dk/~grue.

[13] D. Hilbert and P. Bernays. Grundlagen der Mathematic, volume 2. Springer-Verlag, 1939.

[14] E. Mendelson. Introduction to Mathematical Logic. Wadsworth and Brooks, 3. edition, 1987.

[15] D. Scott. Models for various type-free λ-calculi. In Studies in Logic and The Foundation of Mathematics, volume 74, pages 157–187. Proceedings of the IVth Int. Congress for Logic, Methodology and Philosophy of Science, 1973.