Dependently Typed Set Theory

Chad E. Brown FR Informatik, Saarland Univ.

                                cebrown@ags.uni-sb.de

SEKI-Working-Paper SWP–2006–03

SEKI-Working-Paper ISSN 1860-5931 ^{UNIVERSITÄT DES SAARLANDES FACHRICHTUNG INFORMATIK D–66123 SAARBRÜCKEN GERMANY WWW: http://www.ags.uni-sb.de/}

This SEKI-Working-Paper was internally reviewed by: Serge Autexier FR Informatik, Universität des Saarlandes, D–66123 Saarbrücken, Germany

E-mail: autexier@ags.uni-sb.de
WWW: http://www-ags.dfki.uni-sb.de/~serge/

Editor of SEKI series: Claus-Peter Wirth Brandenburger Str. 42, D–65582 Diez, Germany

E-mail: wirth@logic.at
WWW: http://www.ags.uni-sb.de/~cp

Dependently Typed Set Theory

Chad E. Brown FR Informatik, Saarland Univ.

                     cebrown@ags.uni-sb.de

Submitted October 30, 2006 Definitive Print Edition December 1, 2006

Abstract

Dependently Typed Set Theory (DeTSeT) is untyped set theory encoded in a dependent type theory. The dependent type theory includes proof irrelevance and a special Σ-type between objects and proofs. This allows one to create a “class type” from any predicate on the untyped universe of sets. Given this rich type structure, one can represent partial functions as total functions on the appropriately restricted domain. Set theory can be encoded as a finite signature in the type theory. Furthermore, the signature is essentially second-order (in the λ-calculus sense). We develop the basic theory of DeTSeT and a signature for mathematics.

Keywords: Dependent Type Theory, Set Theory, Proof Irrelevance, Foundations of Mathematics

1 Introduction

In this report, we describe a Dependently Typed Set Theory (DeTSeT) as a foundation for formal mathematics. DeTSeT allows one to work with both an untyped universe of all objects and certain typed collections of these objects. Using the framework, one can mediate between untyped and typed objects. Intuitively, in DeTSeT, one has

Sets ⊆ Classes ⊆ T ypes.

Another important aspect of the framework is proof irrelevance. In logic, proofs are often important objects of study. In mathematics, proofs are not the objects of study, but rather a way of determining the “truth” of propositions about mathematical objects.

We give a theoretical account of DeTSeT with typing judgments and denotational semantics. We also give a syntax-directed algorithmic typing judgment.

Currently DeTSeT is implemented in the system Scunak [9, 7]. Soon it will also be implemented as the new logical foundation for the system Ωmega [32, 33].

As a foundation for formal mathematics, DeTSeT could be used to represent a formal library of mathematics as envisioned in the qed Manifesto [28]. There are many motivations for having such a library and these motivations are discussed in the qed Manifesto. Building a formal library (i.e., formalizing mathematics) is a time consuming process. Ideally, one could imagine a program which scans a mathematics book and converts this scanned version into a formal version for the library. We are far from this ideal world, but it is clear that for this to ever be possible, the formal version must correspond closely to the informal version. Attempts to force higher-order concepts into a first-order representation make clear the need for a formal language other than pure first-order logic. Likewise, attempts to treat concepts such as generic sets, partial functions, and algebraic concepts in simple type theory indicate that simple type theory is also not ideal. We introduce DeTSeT as a new form of set theory which is completely formal and yet allows one to represent informal mathematical concepts in a more natural way than previous logical systems.

1.1 What is Set Theory?

A model of set theory is a collection V along with a binary relation ∈. The elements of V are meant to represent sets. Hence each member of V should be uniquely determined by its elements. That is, for all X, Y ∈ V, if ∀z ∈ V.z ∈ X ≡ z ∈ Y, then X = Y. Often one restricts to models in which the members of V actually are sets and ∈ is the usual membership relation. For this to make sense, for every element x of every set X ∈ V, we must have x ∈ X. That is, for every X ∈ V, we have X ⊆ V. In other words, V is a transitive collection of sets.

A reasonably simple example of a set theoretic model V consists of the hereditarily finite sets. We inductively define V_{n} for natural numbers n by V_{0} := ∅ and V_{n+1} := P(V_{n}) (the power set of V_{n}). For each n, V_{n} is transitive. (The base case is trivial. For the inductive case, note that x ∈ X ∈ V_{n+1} implies x ∈ V_{n} implies x ⊆ V_{n} implies x ∈ V_{n+1}.) Hence

V_{0} ⊆ V_{1} ⊆ ⋯ ⊆ V_{n} ⊆ ⋯

Finally, we let V_{ω} := ⋃ V_{n}. Clearly, V_{ω} is transitive as well.

What other properties does V_{ω} satisfy? One can easily verify the following facts:

1. ∅ ∈ V_{ω}.

2. If x, y ∈ V_{ω}, then {x, y} ∈ V_{ω}.

3. If X ∈ V_{ω}, then P(X) ∈ V_{ω}, i.e., V_{ω} is closed under power sets.

4. If X ∈ V_{ω}, then ⋃ X ∈ V_{ω}, i.e., V_{ω} is closed under unions of sets of sets.

These are some of the usual properties expected of a model of set theory. In particular, these correspond to some of the axioms of Zermelo set theory:

• Extensionality: Sets are determined by their elements.

• Emptyset: The empty set is a set.

• Pairing: If x and y are sets, then {x, y} is a set.

• Powerset: If X is a set, then P(X) is a set.

• Union: If X is a set, then ⋃ X is a set.

• Separation: If X is a set and ϕ is a property, then {x ∈ X|ϕ(x)}.

The notion of property is imprecise in the separation axiom, as it was when Zermelo first formulated set theory [38]. The term “Zermelo set theory” has come to mean the interpretation in which ϕ(x) is a first-order proposition. This can be changed to obtain other set theories. For example, if one restricts ϕ(x) to be a first-order formula in which all quantifiers are bounded (i.e., every ∀y occurs as ∀y.y ∈ A ⇒ ⋯ and every ∃y occurs as ∃y.y ∈ A ∧ ⋯), then one obtains the separation axiom for “Mac Lane set theory”.

The foundational significance of set theory is that the usual mathematical objects of interest (pairs, relations, functions, etc.) can be constructed as sets. Within the collection V_{ω}, one can do many of the usual constructions: the (Kurwatowski) ordered pair ⟨x, y⟩ can be defined as the set {{x}, {x, y}}. Binary relations are sets of pairs, and functions are functional relations. So, within the collection V_{ω} we already have many of the mathematical constructions of interest.

What is missing in V_{ω}? The answer to this question is simple: V_{ω} contains no infinite set. In particular, there is no set of natural numbers. The usual way of constructing the natural numbers in set theory is via finite ordinals. That is, ∅ corresponds to 0, and if the set N corresponds to the natural number n, then the set N ∪{N} corresponds to the natural number n + 1. The set ω of natural numbers is the least set such that ∅ ∈ ω and such that N ∈ ω implies N ∪ {N} ∈ ω. Note that ∅ ∈ V_{ω} and for every N ∈ V_{ω}, N ∪ {N} ∈ V_{ω}. Hence, the set ω is a subset of V_{ω}. However, ω is not a “set” relative to V_{ω}, i.e., ω ∉ V_{ω}. While a finitist may be happy working with the collection V_{ω}, most mathematicians want to work with the set of natural numbers as well as the many objects one can construct from sets of natural numbers.

We can obtain an extended collection by continuing the construction using transfinite induction. We have already defined V_{ω}. We can define V_{ω+1} to be P(V_{ω}). Note that ω ∈ V_{ω+1}, so we now have the first infinite set we want. So, V_{ω+1} satisfies another axiom of Zermelo set theory:

• Infinity: ω is a set.

However, V_{ω+1} is not closed under powersets. In particular, ω ∈ V_{ω+1} but P(ω) ∉ V_{ω+1}.

In general, for any ordinal α, we define V_{α+1} := P(V_{α}) (where α + 1 is the ordinal successor α ∪ {α}). For limit ordinals γ (such as ω), we define V_{γ} := ⋃_{α<γ} V_{α}. This yields the von Neumann hierarchy of sets. Let On denote the collection of all ordinals. (The collection On is not a set in Zermelo–Fraenkel set theory.) Let V := ⋃_{α∈On} V_{α}.

The collection V is transitive, satisfies the axioms above, and contains the infinite set ω. To be precise, V_{ω+ω} is already transitive and satisfies the axioms of extensionality, emptyset, pairing, powerset, union, separation, and infinity.

However, V_{ω+ω} does not satisfy another closure condition corresponding to the Fraenkel (and Skolem) axiom of replacement. The axiom of replacement intuitively states that images of sets under “class functions” should be sets. Consider the function f sending each n ∈ ω to ω + n. ω ∈ V_{ω+ω}, but the image of ω under f – {ω, ω + 1, …, ω + n, …} – is not in V_{ω+ω}.

• Replacement: If f is a class function and X is a set, then {f(x)|x ∈ X} is a set.

In the usual first-order formulation of ZFC, replacement implies separation. In DeTSeT we will include a dependently typed form of separation which apparently cannot be so easily reduced to replacement.

Why is it problematic that (ω + ω) ∉ V_{ω+ω}? One of the nice properties of ZFC is that every well-ordered set is isomorphic to an ordinal. That is, the ordinals provide canonical representations of well-ordered sets. This property fails in V_{ω+ω}. One can easily find a set X and well-ordering R in V_{ω+ω} which is isomorphic to ω+ω in the larger set theoretic universe. For example, consider the set X := {⟨0, n⟩|n ∈ ω} ∪ {⟨1, n⟩|n ∈ ω} and well-ordering R given by

⟨0, 0⟩ < ⟨0, 1⟩ < ⋯ < ⟨0, n⟩ < ⋯ < ⟨1, 0⟩ < ⟨1, 1⟩ < ⋯ < ⟨1, n⟩ < ⋯

Further axioms of ZFC include foundation (or regularity) and choice (giving ZFC — Zermelo–Fraenkel with Choice). The set theories omitting one or both of these axioms are also of theoretical interest.

The intuition for the foundation axiom is that the only sets are those which are constructed in the von Neumann hierarchy. Foundation is often formulated as the following elementary statement:

• Foundation: For every nonempty X, there is some x ∈ X such that x ∩ X is empty.

The foundation axiom prevents cyclic sets, such as Ω = {Ω}.

The choice axiom can be formulated in many equivalent ways [30]. For example:

• Choice: If X is a set of nonempty sets, then there is a function f : X → ⋃ X such that f(x) ∈ x for all x ∈ X.

• Well-Ordering principle: For every set X there is some binary relation which wellorders X. (To be definite, we are referring to a reflexive well-ordering.)

In order to describe either of these axioms, one needs to first construct pairs in order to assert the existence of a function or relation. By considering “downward closed” sets relative to an ordering, we can reformulate the Well-Ordering Principle without referring to relations.

• Alternative Well-Ordering Principle: For every set X there is a set C such that:

1. C is a set of subsets of X.

2. For all x, y ∈ X if ∀A ∈ C(x ∈ A ≡ y ∈ A), then x = y. That is, C contains enough sets to distinguish between different elements of X.

3. For all A, B ∈ C, either A ⊆ B or B ⊆ A.

4. For all nonempty Y ⊆ X, there exist A ∈ C and y ∈ Y such that A and Y are disjoint, and for every B ∈ C either B ⊆ A or y ∈ B.

This alternative form of the well-ordering principle can be formulated without needing to construct intermediate concepts such as ordered pairs. To see that the well-ordering principle implies the alternative form, let C be the set of Y ⊆ X such that ∀y ∈ Y ∀x ∈ X.x ≤ y ⊃ x ∈ Y where ≤ is the well-ordering of X (i.e., Y is downward-closed with respect to ≤). To see that the alternative form of the well-ordering principle implies the original form, one can use C to define a well-ordering by x ≤ y if ∀Y ∈ C.y ∈ Y ⊃ x ∈ Y.

1.2 What is Dependent Type Theory?

The usual method for making the axioms of set theory formal is to do so within first-order logic. DeTSeT is a form of set theory which formulates the axioms in a form of dependent type theory. This was done previously in Automath (earlier in [34] and more recently in [37]).

Generally speaking, a type theory includes terms and types and some notion of when a term has a type. In dependent type theory (at least in the form we consider it here), the types are closed under a Π-constructor, and the terms are closed under λ-abstraction and application. That is, we have types of the form (Πx : A.B(x)) where A is a type and B(x) is a type depending on x : A. Semantically, this is the type of functions f with domain A such that for each a ∈ A, f(a) ∈ B(a). Π-types are the dependently typed generalization of simple function types. Given certain types for variables and constants, some terms will be well-typed and some types will be well-formed. That is, we will have an inductive characterization of when a term M inhabits a type A in a context Γ relative to a signature Σ. Likewise, we will have an inductive characterization of when a type is “well-formed” in a context. More accurately, we will define when a type A is well-formed at level i with i ∈ {0, 1, 2} and we will define when two terms M and N can be checked to be equal at type A. We will then say that a term M has type A when it can be checked to be equal to itself at type A.

There is always room for variation in the presentation of type theories. In presentations of “pure type systems” [3], terms and types are combined into a single universe of “pseudoterms”. In presentations of the particular type theory LF [27] there are three levels of “objects,” “families,” and “kinds.” We will not strive for generality and will restrict ourselves to just what we need to define the particular dependent type theory which serves as the framework for the dependently typed set theory DeTSeT.

The particular dependent type theory we will use will be just strong enough to conveniently formulate the set theory described above. The dependent type theory is a modified version of the type theory LF (also called λP) as implemented in Twelf [27], which itself can essentially be traced back to the Automath family of type theories [10]. Simply put, the type theory can be obtained from LF via the following modifications:

1. Restrict LF to three primitive type families: set, prop and pf M where M should be of type prop. In LF, there are no assumed type families and the signature can introduce arbitrary new type families. In our dependent type theory, we fix the type families at the beginning.

2. Restrict LF by restricting the complexity of types (T ype^{0}, T ype^{1} and T ype^{2}). This restricts the terms to be second-order λ-terms (with a further restriction on the occurrence of propositional variables). LF allows arbitrary higher-order types.

3. Extend LF to allow product types Σ_{x:set}(pf (ϕx)) for each term ϕ : set → prop. On the term level, we include the pairing constructor, first and second destructors and the corresponding reductions. LF does not include pairing or Σ-types, but only λ-abstraction, application, and Π-types.

4. Extend LF to include proof irrelevance, so that all terms of type pf M are equal (where M : prop). LF does not contain any proof irrelevance. A more general way of incorporating proof irrelevance into an extension of LF is discussed in [29]. Proof irrelevance was also considered earlier as part of the Automath project.

The purpose of each modifications to LF is to allow a natural representation of mathematics, while keeping the language as restricted and simple as possible.

1.3 What is DeTSeT?

DeTSeT refers to the dependent type theory described above with a fixed set of logical constants appropriate for a ZFC style set theory. Propositions in DeTSeT correspond to terms of type prop. Proofs in DeTSeT correspond to terms of type pf M for some M : prop. Sets (or “untyped objects”) in DeTSeT correspond to terms of type set. Typed objects in DeTSeT correspond to terms of type cl P for some P : set → prop. Many terms will actually be of a type such as

Πx^{1} : A^{1} ⋯ Πx^{n} : A^{n}.B

where B is either prop, pf M, set, or cl P. We can describe these terms as “parameterized” propositions, proofs, sets, or typed objects.

The logical constants of DeTSeT correspond to the ZFC axioms described above, plus a description operator and a dependent set constructor (corresponding to a dependently typed form of separation).

2 An Algorithmic Formulation of DeTSeT

Let V be a countably infinite set of variables. (Note that variables are untyped.) Let L be a set (disjoint from V) consisting of 46 logical constants named as follows:

                in             eq           eqE          not
               imp           equiv         and          or
             xmcases          notE         impI         impE
             equivI1        equivI2     equivEimp1   equivEimp2
             andEquiv        orEquiv        all          ex
               allI           allE        exEquiv        exu
             exuEquiv       setextAx     emptyset    emptysetAx
            setadjoin     setadjoinAx    powerset    powersetAx
             setunion      setunionAx      omega      omega0Ax
             omegaSAx      omegaIndAx     replAx    foundationAx
          wellorderingAx      descr      dsetconstr  dsetconstrI
           dsetconstrEL   dsetconstrERa

Let A, A^{f} and A^{u} be disjoint infinite sets, each disjoint from both V and L. We call the members of A abbreviations, the members of A^{f} folding rules and the members of A^{u} unfolding rules. Taking the union of the disjoint sets L, A, A^{f} and A^{u}, we obtain the set C of constants.

We use a, b, f, g, a^{0}, a^{1}, … to denote generic abbreviations, and use c, c^{0}, c^{1}, … to denote generic constants. For each abbreviation a, we choose a distinguished folding rule (a)^{f} ∈ A^{f} and unfolding rule (a)^{u} ∈ A^{u}. We assume these are chosen distinctly, so that (a)^{f} = (b)^{f} iff a = b iff (a)^{u} = (b)^{u}.

Definition 2.1 The set of terms is inductively defined using the following grammar:

M :: C|V|(M M)|(λVM)|⟨M, M⟩|π_{1}(M)|π_{2}(M)

A term of the form (M N) corresponds intuitively to applying the term M to the term N. A term of the form (λxM) corresponds intuitively to the function returning the value M when given the input x. A pair ⟨M, P ⟩ intuitively corresponds to a term M representing a set and a term P representing a proof that the set M satisfies some property (i.e., belongs to some class). The two projections π_{1}(M) and π_{2}(M) recover the set and proof, respectively, from a pair. We often omit parentheses which should surround application or λ-abstraction. Application associates to the left, as usual.

The set of types is inductively defined using the following grammar:

A :: set|prop|pf M|cl M|ΠV : A.A

The type set is the type of all sets (i.e., all the “objects” of our mathematical universe). The type prop is the type of propositions. A type of the form pf M is the type of proofs of M, where M should be of type prop. (The fact that M should be of type prop is not enforced in the definition of types, but in the judgment of validity, which we define later.)

A type of the form Πx : A.B is the type of functions from A to B, where the value of the type B depends on the input to the function. As is common in dependent type theory, we use the notation A → B to stand for Πx : A.B where x does not occur free in B. Finally, a type of the form cl ϕ is the “class type” of ϕ, where ϕ should be of type set → prop. A class type cl ϕ corresponds to the pairs ⟨M, P ⟩ where M is a set and P is a proof of (ϕM), i.e., a proof that M belongs to the class determined by ϕ.

The set of signatures is inductively defined as follows:

signatures (Σ) ·|Σ, a : A = M

where a ∈ A. We assume each a is listed at most once in any signature Σ.

The set of contexts is inductively defined as follows:

contexts (Γ) ·|Γ, x : A

where x ∈ V. We assume each variable x in a context Γ is listed only once.

We define the set of free variables FV(M) of a term M and the set free variables FV(A) of a type A in the usual way.

Since we use λxM instead of λx : AM, the definition of terms is independent of the definition of types. We choose this representation because we only consider normal terms, for which we can reconstruct the type of x given the intended type of the term.

For terms and types, we have the usual notion of α-conversion for renaming of bound variables. For convenience, we assume α-equivalent terms as “equal” and assume there are no conflicts with bound variable names whenever convenient.

We let [M/x]W denote the term (resp., type) obtained by substituting the term M for free occurrences of the variable x in the term (resp., type) W. This can be technically defined by induction on W. Similarly, we let θ(W) denote the result of simultaneously substituting finitely many variables as defined in the usual way.

We consider reduction relations induced by the following reductions, again, in the usual way:

β: ((λxM)N) →_{β} [N/x]M

π_{1}: π_{1}(⟨M, N⟩) →_{π_{1}} M

π_{2}: π_{2}(⟨M, N⟩) →_{π_{2}} N

We say a term or type is β′-normal if there are no β-redexes, no π_{1}-redexes and no π_{2}-redexes.

Each of these reductions (along with any combinations of the reductions) is substitutive. That is, if θ is a substitution and W (for a term or type W) reduces to W′, then θ(W) reduces to θ(W′). A proof could follow the same outline as Propositions 2.22 and 2.24 in [12].

Note that βπ_{1}π_{2}-reduction is confluent. We use M^{↓} to denote the βπ_{1}π_{2}-normal form of M, which is unique if it exists. Of course, some terms have no normal form.

2.1 Types of Logical Constants

Each logical constant is associated with a type. We list the correspondence here, along with a short explanation for the type. We write L_{T} (c) to denote the type of c ∈ L given in the list below.

First, we have logical constants corresponding to formulas in first-order logic with equality.

•

 in : set → set → prop

– the membership relation. We often write X ∈ Y for the term (in Y X), which has type prop if it is well-typed.

•

 eq : set → set → prop

– the equality relation. We often write X = Y for the term (eq X Y), which has type prop if it is well-typed.

•

 not : prop → prop

– negation. We often write ¬M for the term (not M), which has type prop if it is well-typed.

•

 imp : prop → prop → prop

– implication. We may write (M ⊃ N) for the term (imp M N), which has type prop if it is well-typed.

•

 equiv : prop → prop → prop

– equivalence. We may write (M ≡ N) for the term (equiv M N), which has type prop if it is well-typed.

•

 and : prop → prop → prop

– conjunction. We may write (M ∧ N) for the term (and M N), which has type prop if it is well-typed.

•

 or : prop → prop → prop

– disjunction. We may write (M ∨ N) for the term (or M N), which has type prop if it is well-typed.

•

 all : (set → prop) → prop

– universal quantification. We use ∀x.ϕ to denote the set (all (λxϕ)).

•

 ex : (set → prop) → prop

– existential quantification. We use ∃x.ϕ to denote the set (ex (λxϕ)).

•

 exu : (set → prop) → prop

– unique existential quantification. We use ∃!x.ϕ to denote the set (exu (λxϕ)).

Next we have logical constants corresponding to deduction rules for classical first-order logic with equality. The rules for implication and universal quantification represent standard natural deduction rules. The xmcases constant is a cases rule relying on excluded middle for arbitrary formulas, thus guaranteeing the logic is classical. Equivalence is taken as primitive with corresponding natural deduction rules. Conjunction, disjunction, existential quantification and unique existential quantification are also taken as primitive, but with axioms which essentially define each in terms of implication and universal quantification.

• eqE : Πx:set. Πy:set. ΠP:(set → prop). (pf (x = y)) → (pf (P x)) → pf (P y)

– a rule for replacing equal objects with equal objects in a context. Intuitively, if (eqE x y P u v) is well-typed, then it is a proof of (P y) whenever u is a proof of x = y and v is a proof of (P x).

• xmcases : ΠM:prop. ΠN:prop. ((pf M) → pf N) → ((pf ¬M) → pf N) → pf N

If we can prove N from M and we can prove N from ¬M, then we have a proof of N.

• notE : ΠM:prop. ΠN:prop. (pf M) → (pf ¬M) → pf N If we prove both M and ¬M, then we have a proof of N.

• impI : ΠM:prop. ΠN:prop. ((pf M) → pf N) → pf (M ⊃ N) If we prove N from M, then we have a proof of M ⊃ N.

• impE : ΠM:prop. ΠN:prop. (pf (M ⊃ N)) → (pf M) → pf N If we prove M ⊃ N and M, then we have a proof of N.

• equivI1 : ΠM:prop. ΠN:prop. (pf M) → (pf N) → pf (M ≡ N) If we prove M and N, then we have a proof of M ≡ N.

• equivI2 : ΠM:prop. ΠN:prop. (pf ¬M) → (pf ¬N) → pf (M ≡ N) If we prove ¬M and ¬N, then we have a proof of M ≡ N.

•

 equivEimp1 : ΠM:prop. ΠN:prop. (pf (M ≡ N)) → (pf M) → pf N

If we prove M ≡ N and M, then we have a proof of N.

•

 equivEimp2 : ΠM:prop. ΠN:prop. (pf (M ≡ N)) → (pf N) → pf M

If we prove M ≡ N and N, then we have a proof of M.

• andEquiv : ΠM:prop. ΠN:prop. pf ((M ∧ N) ≡ ¬(M ⊃ ¬N)) This axiom “defines” ∧ in terms of ¬ and ⊃.

• orEquiv : ΠM:prop. ΠN:prop. pf ((M ∨ N) ≡ (¬M ⊃ N)) This axiom “defines” ∨ in terms of ¬ and ⊃.

• allI : ΠP:(set → prop). (Πx:set. pf (P x)) → pf (∀x.P x) If we have a proof of P x for a generic x, then we have a proof of ∀x.P x.

• allE : ΠP:(set → prop). (pf (∀x.P x)) → Πx:set. pf (P x) If we have a proof of ∀x.P x, then we have a proof of P x where x is any set.

• exEquiv : ΠP:(set → prop). pf ((∃x.P x) ≡ ¬(∀x.¬(P x))) This axiom “defines” existential quantification (ex).

• exuEquiv : ΠP:(set → prop). pf ((∃!x.P x) ≡ (∃x.(P x) ∧ (∀y.(P y) ⊃ (x = y))))

This axiom “defines” unique existential quantification (exu).

Now we turn to the set theory itself. We start with extensionality. For most of the axioms of ZFC, we can give constructors along with axioms characterizing the constructed sets. One variation from ZFC is that we take setadjoin (intuitively taking two sets x and y to the set {x} ∪ y) to be a primitive constructor instead of taking unordered pairing (taking x and y to {x, y}) as primitive. There are two reasons for this choice. First, one can easily describe finitely enumerated sets {a_{1}, …, a_{n}} in terms of setadjoin and the empty set. Second, the ordinal successor of α can be represented as (setadjoin α α), thus making the formulation of the axiom of infinity simpler (in terms of primitives).

• setextAx : pf (∀x.∀y.(∀z.(z ∈ x) ≡ (z ∈ y)) ⊃ (x = y))

– Set extensionality. Two sets x and y are equal if they contain the same elements.

•

 emptyset : set

– the empty set. We use ∅ to denote the term emptyset.

•

 emptysetAx : pf (∀x.¬(x ∈ ∅))

– nothing is in the empty set.

•

 setadjoin : set → set → set

– adjoining a set to another set. (setadjoin x y) intuitively represents {x} ∪ y. We will use {M_{1}, …, M_{n}} where M_{1}, …, M_{n} are terms as shorthand for the term

(setadjoin M_{1} (setadjoin · · · (setadjoin M_{n} emptyset) · · ·)).

• setadjoinAx : pf (∀x.∀y.∀z.(z ∈ (setadjoin x y)) ≡ ((z = x) ∨ (z ∈ y)))

– axiom characterizing setadjoin.

•

 powerset : set → set

– the power set constructor. We use P(X) for the term (powerset X).

• powersetAx : pf (∀x.∀y.(y ∈ P(x)) ≡ (∀z.(z ∈ y) ⊃ (z ∈ x)))

– axiom characterizing the power set.

•

 setunion : set → set

– union of a collection of sets. We use ⋃ X for the term (setunion X).

• setunionAx : pf (∀x.∀y.(y ∈ ⋃ x) ≡ (∃z.(y ∈ z) ∧ (z ∈ x)))

– axiom characterizing ⋃.

• omega : set

– the first infinite ordinal. We use ω to denote the term omega.

•

 omega0Ax : pf (∅ ∈ ω)

– the empty set (the zero ordinal) is in ω.

• omegaSAx : pf (∀x.(x ∈ ω) ⊃ ((setadjoin x x) ∈ ω))

– ω is closed under ordinal successor.

• omegaIndAx : pf (∀x.((∅ ∈ x) ∧ (∀y.((y ∈ ω) ∧ (y ∈ x)) ⊃ ((setadjoin y y) ∈ x))) ⊃ (∀y.(y ∈ ω) ⊃ (y ∈ x)))

– ω is the least set containing ∅ (the zero ordinal) and closed under ordinal successor. This is the induction principle for the natural numbers.

The remaining axioms do not correspond directly to set constructors in DeTSeT.

• replAx : ΠR:(set → set → prop). pf (∀A.(∀y.(y ∈ A) ⊃ (∃!z.Ryz)) ⊃ (∃B.∀y.(y ∈ B) ≡ (∃x.(x ∈ A) ∧ (Rxy))))

– Replacement Axiom.

• foundationAx : pf (∀x.(∃y.y ∈ x) ⊃ (∃y.(y ∈ x) ∧ ¬(∃z.(z ∈ y) ∧ (z ∈ x))))

– Foundation Axiom. If x is nonempty, then there is a y ∈ x such that y and x are disjoint.

• wellorderingAx : pf (∀X.∃C.(((∀A.(A ∈ C) ⊃ (∀x.(x ∈ A) ⊃ (x ∈ X)))

∧(∀x.∀y.(((x ∈ X) ∧ (y ∈ X))

⊃ ((∀A.(A ∈ C) ⊃ ((x ∈ A) ≡ (y ∈ A))) ⊃ (x = y)))))

∧(∀A.∀B.((A ∈ C) ∧ (B ∈ C))

⊃ ((∀x.(x ∈ A) ⊃ (x ∈ B)) ∨ (∀x.(x ∈ B) ⊃ (x ∈ A)))))

∧(∀Y.((∀y.(y ∈ Y) ⊃ (y ∈ X)) ∧ (∃y.y ∈ Y))

⊃ (∃A.∃y.(((A ∈ C) ∧ (y ∈ Y))

∧¬(∃z.(z ∈ A) ∧ (z ∈ Y)))
∧(∀B.(B ∈ C) ⊃ ((∀x.(x ∈ B) ⊃ (x ∈ A)) ∨ (y ∈ B))))))

– our formulation of the Alternative Well-Ordering Principle described earlier. The axiom is equivalent to the Axiom of Choice.

The logical constants thus far are sufficient for encoding any ZFC theorem and proof. However, the purpose of DeTSeT is to allow more convenient representations of theorems and proofs than first-order ZFC. For this reason we add two more concepts: a description operator and a dependent set constructor. (We conjecture these new concepts do not change the expressive power or deductive strength of the theory over ZFC.)

• descr : ΠP:(set → prop). (pf (∃!x.P x)) → cl P

– description operator. Given a predicate P and a proof that exactly one set satisfies P, return an object in the class determined by P. Note that the description operator is not defined on predicates for which there is no proof that a unique element satisfies P.

•

 dsetconstr : ΠA:set. ((cl (inA)) → prop) → set

– a dependent set constructor. Given a set A and a proposition ϕ(x) depending on a member x of A, (dsetconstr A (λx(ϕ(x)))) represents the set {x ∈ A|ϕ(x)}. In fact, we use {x ∈ A|ϕ} to denote the term (dsetconstr A (λxϕ)).

• dsetconstrI : ΠA:set. ΠP:((cl (inA)) → prop). Πa:(cl (inA)). (pf (P a)) → pf (π_{1}(a) ∈ {x ∈ A|P x})

– an introduction rule for the dependent set constructor.

• dsetconstrEL : ΠA:set. ΠP:((cl (inA)) → prop). Πy:set. (pf (y ∈ {x ∈ A|P x})) → pf (y ∈ A)

– a left elimination rule for the dependent set constructor.

• dsetconstrERa : ΠA:set. ΠP:((cl (inA)) → prop). Πa:(cl (inA)). (pf (π_{1}(a) ∈ {x ∈ A|P x})) → pf (P a)

– a right elimination rule for the dependent set constructor.

2.2 Eta and Surjective Pairing

Two forms of reduction we do not build into the notion of reduction are η and π:

η: (λx(Mx)) →_{η} M if x is not free in M.

π: ⟨π_{1}(M), π_{2}(M)⟩ →_{π} M

Instead, there will be some rules in the typing judgment where we either want to η-expand or π-expand on the fly. We introduce some notation to facilitate this.

• If M is a term of the form (λxN), then let x_{λ}^{M} denote x and B_{λ}^{M} denote N. If M is any other term, then let x_{λ}^{M} be a variable not occurring in M and B_{λ}^{M} denote (Mx_{λ}^{M}). Note that in the first case, (λx_{λ}^{M}B_{λ}^{M}) is identical to M. In the second case, (λx_{λ}^{M}B_{λ}^{M})η-reduces to M.

• If M is a term of the form ⟨N, P ⟩, then let fst^{M} denote N and snd^{M} denote P. If M is any other term, then let fst^{M} denote π_{1}(M) and snd^{M} denote π_{2}(M). In the first case, ⟨fst^{M}, snd^{M}⟩ is identical to M. In the second case, ⟨fst^{M}, snd^{M}⟩ π-reduces to M.

2.3 Types for Folding and Unfolding Abbreviations

When an abbreviation a : A = M is declared in a signature, we need to be able to fold and unfold occurrences a to the definition M. We could include in the notion of reduction with rules such as

a → M

to expand a by its definition M in place. Such rules are often used to give a notion of δ-reduction. One can combine δ-reduction with βπ_{1}π_{2}-reduction to give a more general notion of structural equality on terms than βπ_{1}π_{2}-reduction alone provides. The advantage of δ-reduction is that this makes type checking more powerful. Unfortunately, it also means that to check if two terms are equal one may need to expand all abbreviations in the two terms and reduce to a normal form. When there are too many nested abbreviations (a situation unavoidable in mathematics), this is an unreasonable operation.

The alternative we take is the following. Whenever a : A = M occurs in a signature, one is allowed to use the fact that a has type A and, when appropriate, use the constant (a)^{f} to fold M to be a and the constant (a)^{u} to unfold a to be M. To make this precise, we define a partial function Leib(A, M, N) which takes a type A and two terms M and N and, if defined, returns a type B. This function is defined by induction on the type A as follows:

• Leib((Πx:B. C), M, N) :=

(Πx:B. Leib(C, [x/x_{λ}^{M}]B_{λ}^{M}, [x/x_{λ}^{N}]B_{λ}^{N}))

when Leib(C, [x/x_{λ}^{M}]B_{λ}^{M}, [x/x_{λ}^{N}]B_{λ}^{N}) is defined.

• Leib(prop, M, N) := pf M → pf N.

• Leib(set, M, N) := (ΠP:(set → prop). pf (P M) → pf (P N)).

• Leib(cl ϕ, M, N) := (ΠP:(set → prop). pf (P π_{1}(M)) → pf (P π_{1}(N))).

Note that there is no case corresponding to when A is pf P. Thus, the function is partial, and in particular is not defined for types of the form Πx^{1} :A^{1} ⋯ Πx^{n}:A^{n}. pf P. One cannot fold or unfold abbreviations of such a type, but due to proof irrelevance, there is no reason to do so. Any two terms of a type of the form Πx^{1} : A^{1} ⋯ Πx^{n} : A^{n}.pf P will already be equal (in terms of the typing judgments).

Intuitively, Leib(A, M, N) represents Leibniz equality of A and is of the form Πx^{1} : A^{1}. · · · Πx^{n} : A^{n}.set or Πx^{1} : A^{1}. · · · Πx^{n} : A^{n}.cl P. If A is of the form Πx^{1} : A^{1}. · · · Πx^{n} : A^{n}.prop, then Leib(A, M, N) corresponds to implication (and so one obtains equivalence by combining Leib(A, M, N) with Leib(A, N, M).

Now, given a definition a : A = M in a signature M, if Leib(A, a, M) and Leib(A, M, a) are defined (either both are defined or both are undefined), then the folding constant (a)^{f} has type Leib(A, M, a) and the unfolding constant (a)^{u} has type Leib(A, a, M). See the rules xaf and xau in Figure 1.

2.4 Typing Judgments

We next introduce judgments relating terms and types in contexts.

• ⊢ Σ sig means Σ is a valid signature.

• ⊢_{Σ} Γ ctx means Γ is a valid context.

• Γ ⊢_{Σ} A : T ype^{i} means the type A is a valid type at level i ∈ {0, 1, 2}.

• Γ ⊢_{Σ} M ∼ N ↑ A means we can check M and N are equal as members of the type A.

• Γ ⊢_{Σ} M ∼ N ↓ A means we can extract a type A such that M and N are equal in A.

We have listed the judgments in the order above because the order seems a natural one for explanation. In terms of dependencies, they are listed in the wrong order. In order to know if a signature Σ or a context Γ is valid, we must check if types are valid. In order to check if a type such as pf M is valid in a context Γ, we must check if M has type prop (i.e., if M equals itself at type prop) in context Γ. One way to check if a term P has a type pf M is to extract a type pf N and check if M and N are equal at type prop.

Accordingly, we begin by giving the algorithmic rules for the last two judgments for determining if two terms are congruent relative to a type, as well as rules for determining if A is a valid type. These rules are given in Figure 1. The rules for validity of signatures and contexts are given in Figure 2. In the rule coercepf (the rule which builds in proof irrelevance), we make use of the normal forms of the terms Q and R. If either of these terms has no normal form, the rule does not apply. (That is, an implicit premiss of the rule is that Q and R have a normal form.) We conjecture that if the signature Σ is valid, the context Γ is valid, and Γ ⊢ M ∼ M ↓ pf Q is derivable, then Q has a normal form. If this is true, then the implicit premiss would also be redundant. For the record, here is the general conjecture:

Conjecture 1: If ⊢ Σ sig, ⊢_{Σ} Γ ctx, and Γ ⊢_{Σ} M ∼ N ↓ A hold, then the type A has a normal form.

For convenience, we refer to two special cases of judgments using shorthand.

• Γ ⊢ M ↑ A stands for Γ ⊢ M ∼ M ↑ A, intuitively meaning we can check the term M has the type A.

• Γ ⊢ M ↓ A stands for Γ ⊢ M ∼ M ↓ A, intuitively meaning we can extract the type A for M.

\begin{aligned}x : A ∈ Γ \\ & xv \\ Γ ⊢_{Σ} x ∼ x ↓ A \end{aligned} \begin{aligned}c ∈ L \\ & xs \\ Γ ⊢_{Σ} c ∼ c ↓ L_{T} (c) \end{aligned} \begin{aligned}a : A = M ∈ Σ \\ & xa \\ Γ ⊢_{Σ} a ∼ a ↓ A \end{aligned}

\begin{aligned}a : A = M ∈ Σ Leib(A, M, a) = B \\ & xaf \\ Γ ⊢_{Σ} (a)^{f} ∼ (a)^{f} ↓ B \end{aligned} \begin{aligned}a : A = M ∈ Σ Leib(A, a, M) = B \\ & xau \\ Γ ⊢_{Σ} (a)^{u} ∼ (a)^{u} ↓ B \end{aligned}

Γ ⊢_{Σ} M ∼ P ↓ (Πx:A.B) Γ ⊢_{Σ} N ∼ Q ↑ A xa

Γ ⊢_{Σ} (MN) ∼ (P Q) ↓ ([N/x]B)

Γ ⊢_{Σ} M ∼ N ↓ cl ϕ xpi1

Γ ⊢_{Σ} π_{1}(M) ∼ π_{1}(N) ↓ set

Γ ⊢_{Σ} M ∼ N ↓ cl ϕ xpi2

Γ ⊢_{Σ} π_{2}(M) ∼ π_{2}(N) ↓ pf (ϕ π_{1}(M))

Γ, z : A ⊢_{Σ} [z/x_{λ}^{M}]B_{λ}^{M} ∼ [z/x_{λ}^{N}]B_{λ}^{N} ↑ [z/x]B z ∈ V fresh

cλ^{z} Γ ⊢_{Σ} M ∼ N ↑ (Πx:A.B)

Γ ⊢_{Σ} fst^{M} ∼ fst^{N} ↑ set Γ ⊢_{Σ} snd^{M} ∼ snd^{N} ↑ pf (ϕ fst^{M})

cp

Γ ⊢_{Σ} M ∼ N ↑ cl ϕ

Γ ⊢_{Σ} M ∼ N ↓ B B ∈ {set, prop} coerce

Γ ⊢_{Σ} M ∼ N ↑ B

Γ ⊢_{Σ} M ∼ M ↓ pf Q Γ ⊢_{Σ} N ∼ N ↓ pf R Γ ⊢_{Σ} Q^{↓} ∼ P ↑ prop Γ ⊢_{Σ} R^{↓} ∼ P ↑ prop

coercepf

Γ ⊢_{Σ} M ∼ N ↑ pf P

Γ ⊢_{Σ} A : T ype^{i} Γ, z : A ⊢_{Σ} [z/x]B : T ype^{j} \begin{matrix}i ∈ \{0, 1\}, j ∈ \{0, 1, 2\} \\ z ∈ V fresh \end{matrix}

vtΠ

Γ ⊢_{Σ} (Πx:A.B) : T ype^{max(i+1,j)}

\frac{vto}{Γ ⊢_{Σ} set:T ype^{0}} \frac{vtp}{Γ ⊢_{Σ} prop : T ype^{1}} Γ ⊢_{Σ} M ∼ M ↑ prop vtpf

Γ ⊢_{Σ} pf M : T ype^{0}

Γ ⊢_{Σ} M ∼ M ↑ (set → prop)

vtcl

Γ ⊢_{Σ} cl M : T ype^{0}

\begin{aligned}Γ ⊢_{Σ} A : T ype^{i} i ∈ \{0, 1\} \\ & vtu \\ Γ ⊢_{Σ} A : T ype^{i+1} \end{aligned}

Figure 1: Rules for Algorithmic Typing Judgments

\frac{emptysig}{⊢ · sig}

⊢ Σ sig · ⊢_{Σ} A : T ype^{2} · ⊢_{Σ} M ∼ M ↑ A a ∈ A \ dom(Σ) conssig

⊢ Σ, a : A = M sig

\frac{emptyctx}{⊢_{Σ} · ctx}

⊢_{Σ} Γ ctx Γ ⊢_{Σ} A : T ype^{1} x ∈ V \ dom(Γ)

consctx ⊢_{Σ} Γ, x : A ctx

Figure 2: Rules for Valid Signatures and Contexts 18

3 Developing a Signature for Basic Mathematics

Starting from the logical constants given above, one can construct a signature of abbreviations which includes the basic inference rules one wants as well as the usual objects of mathematical interest: ordered pairs, Cartesian products, and functions. Note that in particular one can use these abbreviations to encode simply typed λ-calculus within DeTSeT.

Without giving an entire such signature, we list some of the abbreviations along with their types. In some cases we will also include the term defining the abbreviation. Since many terms (especially those corresponding to proofs) will be large and difficult to understand when written out in full detail, we will adopt some notation conventions.

First, we can give a modified form of the right elimination rule for the dependent set constructor dsetconstr. The logical constant corresponding to the right elimination rule is dsetconstrERa. Suppose A has type set, P has type ((cl (in A)) → prop) and a has type (cl (in A)). Then (dsetconstrERa A P a) is a term which expects a proof of π_{1}(a) ∈ {x ∈ A|P x} and returns a proof of (P a). Suppose y is of type set and u is of type pf (y ∈ {x ∈ A|P x}). Can we prove (P y) holds? Strictly speaking, this term is ill-typed since P expects a term of type cl (in A) and y is of type set. However, we can use a proof (any proof) of y ∈ A to form a term, essentially equal to y, of type cl (in A). Note that (dsetconstrEL A P y u) is of type pf (y ∈ A). So, the pair ⟨y, (dsetconstrEL A P y u)⟩ has type cl (in A). Now, we can form the term

                (dsetconstrERa A P ⟨y, (dsetconstrEL A P y u)⟩u)

which has type pf (P ⟨y, (dsetconstrEL A P y u)). This allows us to apply the right elimination rule to an arbitrary y which we do not know a priori is a member of the bounding set A. We will abbreviate this rule using the name dsetconstrER which has type

ΠA:set.ΠP:((cl (inA)) → prop).Πy:set.(pf (y ∈ {x ∈ A|P x}))

                      → pf (P ⟨y, (dsetconstrEL A P y u))

and is defined by the term

           λAλP λyλu(dsetconstrERa A P ⟨y, (dsetconstrEL A P y u)⟩u)

While this proof term is of a reasonable size, and can be understood given the explanation above, more complex proof terms will be large and difficult to understand. A way to avoid this problem, is to use a temporary symbol to denote subterms (except variables) which have the type pf M for some M. Each such subterm can be thought of as a “proof step” or “proof line.” For example, the subterm (dsetconstrEL A P y u) above has type pf (y ∈ A) in the appropriate context Γ. We can use the symbol L1 to denote the proof term and then rewrite the definition of dsetconstrER as

λAλP λyλu(dsetconstrERa A P ⟨y, L1⟩u)

This notation has the advantage that it hides the details of proofs (which are unimportant in type-checking because of proof irrelevance). As we introduce this temporary symbol L1, we should explicitly write what the term L1 denotes. We will call these temporary symbols (which will be named Li for some i) “proof steps” and list them after the term is given. In order to represent the term as a whole, it is enough to know what term each proof step represents. However, to understand the term, it is helpful to also give the type of each proof step. Hence we will give each proof step in the form

Li pf M  by:P

where P is the term Li represents and pf M is the type of P in the appropriate context. When the proof steps are listed in order, they obtain the appearance of a linearized natural deduction proof. We leave the context implicit, but as a further aid to readability, we sometimes include lines of the form

Let x have type A

when x is a bound variable of type A and

D Assume M

when D is a bound variable of type pf M. To be precise, we include these lines whenever the corresponding bound variable is in the context of some but not all proof steps. The “Let” or “Assume” statement will precede the first proof step which assumes the variable is in context, but it is the task of the reader to note when the variable has been discharged from the context. Again, no context or type information is necessary to uniquely reconstruct the term as a whole. All one needs is the unique term associated with each proof step Li.

Using a proof step representation, we can write the abbreviation dsetconstrER as follows

 dsetconstrER : ΠA:set. Πϕ:(cl (in A) → prop). Πx:set.

ΠD:pf (x ∈ {a ∈ A | ϕ a }). pf (ϕ ⟨ x, L1 ⟩) = λA λϕ λx λD dsetconstrERa A ϕ ⟨ x, L1 ⟩ D using proof step

L1 : pf (x ∈ A)  by: dsetconstrEL A ϕ x D

Note that the type of ϕ in dsetconstrER is cl (in A) → prop. One important notational simplification is simply to write any class type cl P as P. Given this simplification, we can write the type of ϕ as (in A) → prop. A further simplification is to omit the “in” in class types induced by sets (as is the case here). That is, we can write the type of ϕ as A → prop. Hence we can write the abbreviation dsetconstrER as follows:

 dsetconstrER : ΠA:set. Πϕ:(A → prop). Πx:set .

ΠD:pf (x ∈ {a ∈ A | ϕ a }). pf (ϕ ⟨ x, L1 ⟩) = λA λϕ λx λD dsetconstrERa A ϕ ⟨ x, L1 ⟩ D using proof step

L1 : pf (x ∈ A)  by: dsetconstrEL A ϕ x D

In addition to the usual quantifiers, we can define dependent bounded quantifiers dall and dex along with inference rules. Intuitively, (dall A (λxϕ)) means ∀x ∈ A.ϕ(x). The reason for saying these are dependent quantifiers is because within the body of the binder one can use the (proof of the) fact that the bound variable is in the bounding set. For example, if P represents the set of positive real numbers, then one can write ∃x ∈ P.(\frac{x^{2}−1}{x} = 0) where one needs to know x ≠ 0 (which should follow from x ∈ P) to form the proposition (\frac{x^{2}−1}{x} = 0). dall : ΠA:set. (A → prop) → prop = λA λϕ {a ∈ A | ϕ a } = A

dex : ΠA:set. (A → prop) → prop = λA λϕ ¬{a ∈ A | ϕ a } = ∅

Note that the term defining dall is

λAλϕ((dsetconstr A (λx(ϕ x))) = A)

That is, (dall A ϕ) is defined to be the proposition {x ∈ A|ϕ(x)} = A. One might try to define (dall A ϕ) as ∀x.x ∈ A ⊃ (ϕ x), except that this is ill-typed (since x would have type set).

From now on, we will use (∀x ∈ A.ϕ) to denote a term of the form (dall A (λxϕ)) and use (∃x ∈ A.ϕ) to denote a term of the form (dex A (λxϕ)).

One can also define dependent versions of conjunction (dand) and implication (dimp). This allows one to represent a proposition such as A ∧ B where one needs to know A is true in order to construct B. For example, consider the proposition (x > 0) ∧ (\frac{x^{2}−1}{x} = 0). In order to facilitate these abbreviations, we first define prop2set, which embeds propositions into sets by taking a proposition ϕ to the set {∅} if ϕ is true and to ∅ if ϕ is false. We also prove a rule prop2setE which says the proposition is true if the corresponding set has an element.

prop2set : prop → set = λϕ {a ∈ P ∅ | ϕ }
prop2setE : Πϕ:prop. Πx:set. pf (x ∈ (prop2set ϕ)) → pf ϕ

= λϕ λx λD dsetconstrER (P ∅) (λa ϕ) x L1 using proof step

L1 : pf (x ∈ {a ∈ P ∅ | ϕ }) by: (prop2set)^{u} ϕ (λA x ∈ A) D

Now we can define dand. Note that the definition of dand makes use of prop2setE in a proof term.

dand : Πϕ:prop. (pf ϕ → prop) → prop = λϕ λψ ∃a ∈ (prop2set ϕ). ψ L2

using proof steps

L1 : pf (π_{1}(a) ∈ (prop2set ϕ))  by: π_{2}(a)
L2 : pf ϕ  by: prop2setE ϕ π_{1}(a) L1

We now simplify the notation by omitting all occurrences of π_{1} and π_{2}. It is left to the reader to recognize when one of these is omitted. The idea is that if a term has a class type, but is used as if it has type set, then a π_{1} has been omitted. If a term has a class type, but is used as if it has a proof type, then a π_{2} has been omitted. We can now present dand as follows:

dand : Πϕ:prop. (pf ϕ → prop) → prop = λϕ λψ ∃a ∈ (prop2set ϕ). ψ L2

using proof steps

L1 : pf (a ∈ (prop2set ϕ))  by: a

L2 : pf ϕ  by: prop2setE ϕ a L1

We define dependent implication similarly:

dimp : Πϕ:prop. (pf ϕ → prop) → prop = λϕ λψ ∀a ∈ (prop2set ϕ). ψ L2

using proof steps

L1 : pf (a ∈ (prop2set ϕ))  by: a

L2 : pf ϕ  by: prop2setE ϕ a L1

We can define false.

false : prop = ∅ ∈ ∅

We use ⊥ to denote the term false.

The following are rules for eliminating the empty set, eliminating false, and introducing negation.

emptysetE : Πx:set. pf (x ∈ ∅) → Πϕ:prop. pf ϕ

= λx λD λϕ notE (x ∈ ∅) ϕ D L2 using proof steps

L1 : pf (∀y. ¬y ∈ ∅)  by: emptysetAx
L2 : pf (¬x ∈ ∅)  by: allE (λy ¬y ∈ ∅) L1 x

falseE : Πϕ:prop. pf ⊥ → pf ϕ = λϕ λD emptysetE ∅ L1 ϕ

using proof step

L1 : pf (∅ ∈ ∅) by: (false)^{u} D

notI : Πϕ:prop. (pf ϕ → pf ⊥) → pf (¬ϕ) = λϕ λD xmcases ϕ (¬ϕ) (λE L2) (λF F) using proof steps

L1 : pf ⊥  by: D E
L2 : pf (¬ϕ) by: falseE (¬ϕ) L1

We can also derive a rule for proof by contradiction:

contradiction : Πϕ:prop. (pf (¬ϕ) → pf ⊥) → pf ϕ

= λϕ λD xmcases ϕ ϕ (λE E) (λF L2) using proof steps

L1 : pf ⊥  by: D F
L2 : pf ϕ by: falseE ϕ L1

The way to construct proof terms should be clear from the examples above. Below we list a number of other logical rules which can be derived. For the sake of brevity, we omit the proof terms and give only the types.

dnegE : Πϕ:prop. pf (¬¬ϕ) → pf ϕ
dnegI : Πϕ:prop. pf ϕ → pf (¬¬ϕ)
contrapositive1 : Πϕ:prop. Πψ:prop. (pf ϕ → pf ψ) → pf (¬ψ) → pf (¬ϕ)
contrapositive2 : Πϕ:prop. Πψ:prop. (pf (¬ϕ) → pf ψ) → pf (¬ψ) → pf ϕ
contrapositive3 : Πϕ:prop. Πψ:prop. (pf (¬ϕ) → pf (¬ψ)) → pf ψ → pf ϕ
contrapositive4 : Πϕ:prop. Πψ:prop. (pf ϕ → pf (¬ψ)) → pf ψ → pf (¬ϕ)

andI : Πϕ:prop. Πψ:prop. pf ϕ → pf ψ → pf (ϕ ∧ ψ)
andEL : Πϕ:prop. Πψ:prop. pf (ϕ ∧ ψ) → pf ϕ
andER : Πϕ:prop. Πψ:prop. pf (ϕ ∧ ψ) → pf ψ
orIL : Πϕ:prop. Πψ:prop. pf ϕ → pf (ϕ ∨ ψ)
orIR : Πϕ:prop. Πψ:prop. pf ψ → pf (ϕ ∨ ψ)

orE : Πϕ:prop. Πψ:prop. pf (ϕ ∨ ψ) → Πχ:prop. (pf ϕ → pf χ) → (pf ψ → pf χ) → pf χ orIDemorgan : Πϕ:prop. Πψ:prop. (pf (¬ϕ) → pf (¬ψ) → pf ⊥) → pf (ϕ ∨ ψ) exE : Πϕ:(set → prop). pf (∃x. ϕ x) → Πψ:prop. (Πx:set. pf (ϕ x) → pf ψ)

→ pf ψ

exI : Πϕ:(set → prop). Πx:set. pf (ϕ x) → pf (∃y. ϕ y) equivI : Πϕ:prop. Πψ:prop. (pf ϕ → pf ψ) → (pf ψ → pf ϕ) → pf (ϕ ≡ ψ)

equivE : Πϕ:prop. Πψ:prop. Πχ:prop. pf (ϕ ≡ ψ) → (pf ϕ → pf ψ → pf χ)

→ (pf (¬ϕ) → pf (¬ψ) → pf χ) → pf χ

We derive natural deduction rules corresponding to the set theory axioms, as well as reflexivity of equality: eqI. We define true and give an introduction rule trueI as well. We use ⊤ to denote the term true. setext : ΠA:set. ΠB:set. (Πx:set. pf (x ∈ A) → pf (x ∈ B)) → (Πx:set. pf (x ∈ B) → pf (x ∈ A)) → pf (A = B) eqI : ΠA:set. pf (A = A)

setadjoinIL : Πx:set. ΠA:set. pf (x ∈ (setadjoin x A))
setadjoinIR : Πx:set. ΠA:set. Πy:set. pf (y ∈ A) → pf (y ∈ (setadjoin x A))
setadjoinE : Πx:set. ΠA:set. Πy:set. pf (y ∈ (setadjoin x A)) → Πϕ:prop .

(pf (y = x) → pf ϕ) → (pf (y ∈ A) → pf ϕ) → pf ϕ

true : prop = ∅ ∈ {∅}
trueI : pf ⊤

powersetI : ΠA:set.ΠX:set.(Πx:set.pf (x ∈ X) → pf (x ∈ A)) → pf (X ∈ (P A)) powersetE : ΠA:set.ΠX:set.Πx:set.pf (X ∈ (P A)) → pf (x ∈ X) → pf (x ∈ A) setunionI : ΠA:set.Πx:set.ΠX:set.pf (x ∈ X) → pf (X ∈ A) → pf (x ∈ (⋃ A)) setunionE : ΠA:set. Πx:set. pf (x ∈ (⋃ A)) → Πϕ:prop . (ΠX:set. pf (x ∈ X) → pf (X ∈ A) → pf ϕ) → pf ϕ

Equality is symmetric and transitive. We also include a few variations on equality rules. symeq : Πx:set. Πy:set. pf (x = y) → pf (y = x) transeq : Πx:set. Πy:set. Πz:set. pf (x = y) → pf (y = z) → pf (x = z) symtrans1eq : Πx:set. Πy:set. Πz:set. pf (x = y) → pf (z = y) → pf (x = z) eqE2 : Πx:set. Πy:set. Πϕ:(set → prop). pf (x = y) → pf (ϕ y) → pf (ϕ x) uniqinunit : Πx:set. Πy:set. pf (x ∈ {y}) → pf (x = y) eqinunit : Πx:set. Πy:set. pf (x = y) → pf (x ∈ {y}) symtrans2eq : Πx:set. Πy:set. Πz:set. pf (x = y) → pf (z = y) → pf (z = x) boxeq : Πx^{1} :set. Πy^{1} :set. Πx^{2} :set. Πy^{2} :set. pf (x^{1} = y^{1}) → pf (x^{2} = y^{2}) → pf (y^{1} = y^{2}) → pf (x^{1} = x^{2})

The following are rules for dependent quantifiers and dependent propositional connectives. dallI : ΠA:set. Πϕ:(A → prop). (Πa:A. pf (ϕ a)) → pf (∀a ∈ A. ϕ a) dallE : ΠA:set. Πϕ:(A → prop). pf (∀a ∈ A. ϕ a) → Πa:A. pf (ϕ a) dexI : ΠA:set. Πϕ:(A → prop). Πa:A. pf (ϕ a) → pf (∃b ∈ A. ϕ b) dexE : ΠA:set. Πϕ:(A → prop). pf (∃a ∈ A. ϕ a) → Πψ:prop . (Πa:A. pf (ϕ a) → pf ψ) → pf ψ dandI : Πϕ:prop. Πψ:(pf ϕ → prop). ΠD:pf ϕ. pf (ψ D) → pf (dand ϕ ψ)

dandEL : Πϕ:prop. Πψ:(pf ϕ → prop). pf (dand ϕ ψ) → pf ϕ

dandER : Πϕ:prop. Πψ:(pf ϕ → prop). ΠD:pf (dand ϕ ψ). pf (ψ L1) using proof step

L1 : pf ϕ by: dandEL ϕ ψ D

dimpI : Πϕ:prop. Πψ:(pf ϕ → prop). (ΠD:pf ϕ. pf (ψ D)) → pf (dimp ϕ ψ) dimpE : Πϕ:prop. Πψ:(pf ϕ → prop). pf (dimp ϕ ψ) → ΠD:pf ϕ. pf (ψ D)

The following rules are useful for special cases, such as when a negated proposition is assumed. Some of the rules are classical in nature.

vacuousImpI : Πϕ:prop. Πψ:prop. pf (¬ϕ) → pf (ϕ ⊃ ψ)
trivialImpI : Πϕ:prop. Πψ:prop. pf ψ → pf (ϕ ⊃ ψ)
excludedmiddle : Πϕ:prop. pf (ϕ ∨ (¬ϕ))

notimpE : Πϕ:prop. Πψ:prop. pf (¬(ϕ ⊃ ψ)) → pf (ϕ ∧ (¬ψ))

notimpE1 : Πϕ:prop. Πψ:prop. pf (¬(ϕ ⊃ ψ)) → pf ϕ

notimpE2 : Πϕ:prop. Πψ:prop. pf (¬(ϕ ⊃ ψ)) → pf (¬ψ)

notorE : Πϕ:prop. Πψ:prop. pf (¬(ϕ ∨ ψ)) → pf ((¬ϕ) ∧ (¬ψ))

notorE1 : Πϕ:prop. Πψ:prop. pf (¬(ϕ ∨ ψ)) → pf (¬ϕ)

notorE2 : Πϕ:prop. Πψ:prop. pf (¬(ϕ ∨ ψ)) → pf (¬ψ)

notandE : Πϕ:prop. Πψ:prop. pf (¬(ϕ ∧ ψ)) → pf ((¬ϕ) ∨ (¬ψ))

notexE : Πϕ:(set → prop). pf (¬∃A. ϕ A) → pf (∀A. ¬ϕ A)

notdexE : ΠA:set.Πϕ:(A → prop).pf (¬∃a ∈ A. ϕ a) → pf (∀a ∈ A. ¬ϕ a)

notallE : Πϕ:(set → prop). pf (¬∀A. ϕ A) → pf (∃A. ¬ϕ A)

notdallE : ΠA:set. Πϕ:(A → prop).pf (¬∀a ∈ A. ϕ a) → pf (∃a ∈ A. ¬ϕ a)

We now give more rules for equivalence.

reflequiv : Πϕ:prop. pf (ϕ ≡ ϕ)
symequiv : Πϕ:prop. Πψ:prop. pf (ϕ ≡ ψ) → pf (ψ ≡ ϕ)
transequiv : Πϕ:prop. Πψ:prop. Πχ:prop. pf (ϕ ≡ ψ) → pf (ψ ≡ χ)

→ pf (ϕ ≡ χ)

symtrans1equiv : Πϕ:prop. Πψ:prop. Πχ:prop. pf (ϕ ≡ ψ) → pf (χ ≡ ψ)

→ pf (ϕ ≡ χ)

boxequiv : Πϕ^{1} :prop. Πψ^{1} :prop. Πϕ^{2} :prop. Πψ^{2} :prop. pf (ϕ^{1} ≡ ψ^{1}) → pf (ϕ^{2} ≡ ψ^{2}) → pf (ψ^{1} ≡ ψ^{2}) → pf (ϕ^{1} ≡ ϕ^{2})

The following are modified versions of the rule corresponding to the eqE logical constant, which corresponds to the Leibniz property of equality. The version eqCE here (and the symmetric version eqCE2) allow one to replace equal terms of a class type (as opposed to type set) within a term. Note that the types of a and b below (written as ϕ) are cl ϕ and the type of ψ (written as ϕ → prop) is cl ϕ → prop. (We conjecture that it would not be possible to define a term of the types of eqCE or eqCE2 using the signature of logical constants used in DeTSeT if proof irrelevance were not part of the type theory. That is, proof irrelevance seems to be vital for reducing “typed Leibniz equality” in the form of eqCE to “untyped Leibniz equality” in the form of eqE.)

eqCE : Πϕ:(set → prop). Πa:ϕ. Πb:ϕ. Πψ:(ϕ → prop). pf (a = b) → pf (ψ a) → pf (ψ b)

eqCE2 : Πϕ:(set → prop). Πa:ϕ. Πb:ϕ. Πψ:(ϕ → prop). pf (a = b) → pf (ψ b) → pf (ψ a)

The following is a definition of the subset relation:

subset : set → set → prop = λA λB ∀a ∈ A. a ∈ B

We use M ⊆ N to denote a term of the form (subset M N). We next give rules relating to subset and powerset. subsetI1 : ΠA:set. ΠB:set. (Πa:A. pf (a ∈ B)) → pf (A ⊆ B) subsetI2 : ΠA:set.ΠB:set.(Πx:set.pf (x ∈ A) → pf (x ∈ B)) → pf (A ⊆ B) subsetE : ΠA:set. ΠB:set. Πx:set. pf (A ⊆ B) → pf (x ∈ A) → pf (x ∈ B)

subset2powerset : ΠA:set. ΠB:set. pf (A ⊆ B) → pf (A ∈ (P B))

setextsub : ΠA:set. ΠB:set. pf (A ⊆ B) → pf (B ⊆ A) → pf (A = B) powersetI1 : ΠA:set. ΠB:set. pf (B ⊆ A) → pf (B ∈ (P A)) powersetsubset : ΠA:set. ΠB:set. pf (A ⊆ B) → pf ((P A) ⊆ (P B))

The following defines binary union:

binunion : set → set → set = λA λB ⋃ {A, B}

Recall {A, B} is shorthand for the term (setadjoin A (setadjoin B emptyset)) as described in Section 2.1. From now on, we will use A ∪ B to denote the term (binunion A B). The following abbreviations correspond to deduction rules for binary unions: binunionIL : ΠA:set. ΠB:set. Πx:set. pf (x ∈ A) → pf (x ∈ (A ∪ B)) binunionIR : ΠA:set. ΠB:set. Πx:set. pf (x ∈ B) → pf (x ∈ (A ∪ B))

binunionEcases : ΠA:set. ΠB:set. Πx:set. Πϕ:prop. pf (x ∈ (A ∪ B))

→ (pf (x ∈ A) → pf ϕ) → (pf (x ∈ B) → pf ϕ) → pf ϕ binunionE : ΠA:set.ΠB:set.Πx:set.pf (x ∈ (A ∪ B)) → pf ((x ∈ A) ∨ (x ∈ B))

binunionLsub : ΠA:set. ΠB:set. pf (A ⊆ (A ∪ B))
binunionRsub : ΠA:set. ΠB:set. pf (B ⊆ (A ∪ B))

We next define binary intersection and give derived rules.

binintersect : set → set → set = λA λB {a ∈ A | a ∈ B }

We use (M ∩ N) to denote (binintersect M N).

binintersectI : ΠA:set.ΠB:set.Πx:set.pf (x ∈ A) → pf (x ∈ B)

→ pf (x ∈ (A ∩ B)) binintersectEL : ΠA:set. ΠB:set. Πx:set. pf (x ∈ (A ∩ B)) → pf (x ∈ A) binintersectER : ΠA:set. ΠB:set. Πx:set. pf (x ∈ (A ∩ B)) → pf (x ∈ B)

Defining set difference is also easy. setminus : set → set → set = λA λB {a ∈ A | ¬a ∈ B }

We now turn to pairs, Cartesian products and functions. This is enough to interpret simply typed λ-calculus and so should provide the basis for importing the libraries of theorem provers such as Isabelle-HOL [26], HOL-light [15] and HOL4 into DeTSeT.

iskpair : set → prop

= λu ∃a ∈ ⋃ u. ∃b ∈ ⋃ u. u = {{a}, {a, b}}

kpairiskpair : Πx:set. Πy:set. pf (iskpair {{x}, {x, y}})
kpair : set → set → iskpair = λx λy ⟨ {{x}, {x, y}}, kpairiskpair x y ⟩

We will use ⟨⟨M, N⟩⟩ to denote the term (kpair M N).

cartprod : set → set → set

We use A × B to denote the term (cartprod A B). cartprodpairin : ΠA:set. ΠB:set. Πa:A. Πb:B. pf (⟨⟨ a, b ⟩⟩ ∈ (A × B))

cartprodpair : ΠA:set. ΠB:set. A → B → (A × B)
cartprodfst : ΠA:set. ΠB:set. (A × B) → A
cartprodsnd : ΠA:set. ΠB:set. (A × B) → B
cartprodfstpairEq : ΠA:set. ΠB:set. Πa:A. Πb:B .
pf (cartprodfst A B (cartprodpair A B a b) = a)
cartprodsndpairEq : ΠA:set. ΠB:set. Πa:A. Πb:B .
pf (cartprodsnd A B (cartprodpair A B a b) = b)
cartprodpairsurjEq : ΠA:set. ΠB:set. Πa:(A × B) .
pf (cartprodpair A B (cartprodfst A B a) (cartprodsnd A B a) = a)
breln : set → set → set → prop
dpsetconstr : ΠA:set. ΠB:set. (A → B → prop) → set

We use the notation {⟨⟨x, y⟩⟩ ∈ A × B|ϕ} to denote the term (dpsetconstr A B (λxλyϕ)).

funcSet : set → set → set

ap2 : ΠA:set. ΠB:set. (funcSet A B) → A → B lam2 : ΠA:set. ΠB:set. (A → B) → (funcSet A B)

funcext2 : ΠA:set. ΠB:set. Πf:(funcSet A B). Πg:(funcSet A B) .

(Πa:A. pf (ap2 A B f a = ap2 A B g a)) → pf (f = g) beta2 : ΠA:set.ΠB:set.Πf:(A → B).Πa:A. pf ((ap2 A B (lam2 A B f) a) = (f a)) eta2 : ΠA:set. ΠB:set. Πf:(funcSet A B). pf ((lam2 A B (ap2 A B f)) = f)

An if operator is useful for defining objects or functions that depend on conditions. if : ΠA:set. prop → A → A → A iftrue : ΠA:set. Πϕ:prop. Πa:A. Πb:A. pf ϕ → pf (if A ϕ a b = a) iffalse : ΠA:set. Πϕ:prop. Πa:A. Πb:A. pf (¬ϕ) → pf (if A ϕ a b = b) iftrueorfalse : ΠA:set. Πϕ:prop. Πa:A. Πb:A. pf (if A ϕ a b ∈ {a, b})

4 The Distributivity Example

An example considered several times within the Ωmega group is the distributivity property of binary union and intersection A∩(B ∪C)) = (A∩B)∪(A∩C). (This is part of Theorem 1.1.4(d) in [4]. The proof in [4] was studied in [1, 9].) We formalize the problem as the type of the abbreviation bs114d and give a proof as a term of this type in Figure 3.

5 Wizard of Oz DiaLog Examples

5.1 Formalizing the First DiaLog Wizard of Oz Experiment: Typed Sets

The following abbreviations concern typed sets and are relevant to the first Wizard of Oz experiment in the DiaLog project [5]. We begin by defining “typed” versions of set operations such as binary intersection, powerset, and complement relative to a set U. That is, we define the operations restricted to subsets of a given set. Since the power set of U is the set of subsets of U, we can use this set as the class type of subsets of U. First, we can prove that if X and Y are subsets of U, then so is X ∩ Y:

binintersectT_lem : ΠU:set. ΠA:(P U). ΠB:(P U). pf ((A ∩ B) ∈ (P U))

Next we can use this fact to define the “typed” binary intersection operator which carries the information that the inputs and outputs are subsets of U:

binintersectT : ΠU:set. (P U) → (P U) → (P U)

 = λU λA λB ⟨ A ∩ B, binintersectT_lem U A B ⟩

We use Aˆ∩B to denote the term (binintersectT U A B) (where U is a fixed bound variable). We could overload the symbol ∩ to be typed intersection if the two arguments have type cl (in U) and untyped intersection otherwise, but we choose to avoid overloading symbols for the sake of clarity.

A similar process defines a “typed” binary union operator.

binunionT_lem : ΠU:set. ΠA:(P U). ΠB:(P U). pf ((A ∪ B) ∈ (P U))

binunionT : ΠU:set. (P U) → (P U) → (P U) = λU λA λB ⟨ A ∪ B, binunionT_lem U A B ⟩

We use Aˆ∪B to denote the term (binunionT U A B).

We define a “typed” powerset operator (note that the output type is one “untyped” powerset higher than the input type).

powersetT_lem : ΠU:set. ΠA:(P U). pf ((P A) ∈ (P P U))

powersetT : ΠU:set. (P U) → (P P U)

 = λU λA ⟨ P A, powersetT_lem U A ⟩

We use P̂A to denote the term (powersetT U A). bs114d : ΠA:set.ΠB:set.ΠC:set.pf ((A ∩ (B ∪ C)) = ((A ∩ B) ∪ (A ∩ C))) = λA λB λC setextsub (A ∩ (B ∪ C)) ((A ∩ B) ∪ (A ∩ C)) L10 L21 using proof steps

Let a have type (A ∩ (B ∪ C))

L1 : pf (a ∈ (A ∩ (B ∪ C)))  by: a
L2 : pf (a ∈ (B ∪ C))  by: binintersectER A (B ∪ C) a L1
D  Assume a ∈ B
L3 : pf (a ∈ A)  by: binintersectEL A (B ∪ C) a L1
L4 : pf (a ∈ (A ∩ B))  by: binintersectI A B a L3 D
L5 : pf (a ∈ ((A ∩ B) ∪ (A ∩ C))) by: binunionIL (A ∩ B) (A ∩ C) a L4
E  Assume a ∈ C
L6 : pf (a ∈ A)  by: binintersectEL A (B ∪ C) a L1
L7 : pf (a ∈ (A ∩ C))  by: binintersectI A C a L6 E
L8 : pf (a ∈ ((A ∩ B) ∪ (A ∩ C))) by: binunionIR (A ∩ B) (A ∩ C) a L7
L9 : pf (a ∈ ((A ∩ B) ∪ (A ∩ C)))
by: binunionEcases B C a (a ∈ ((A ∩ B) ∪ (A ∩ C))) L2 (λD L5) (λE L8)
L10 : pf ((A ∩ (B ∪ C)) ⊆ ((A ∩ B) ∪ (A ∩ C)))
by: subsetI1 (A ∩ (B ∪ C)) ((A ∩ B) ∪ (A ∩ C)) (λa L9)
Let b have type ((A ∩ B) ∪ (A ∩ C))
L11 : pf (b ∈ ((A ∩ B) ∪ (A ∩ C)))  by: b
F  Assume b ∈ (A ∩ B)

L12 : pf (b ∈ A)  by: binintersectEL A B b F
L13 : pf (b ∈ B)  by: binintersectER A B b F

L14 : pf (b ∈ (B ∪ C))  by: binunionIL B C b L13
L15 : pf (b ∈ (A ∩ (B ∪ C)))  by: binintersectI A (B ∪ C) b L12 L14
G  Assume b ∈ (A ∩ C)

L16 : pf (b ∈ A)  by: binintersectEL A C b G
L17 : pf (b ∈ C)  by: binintersectER A C b G

L18 : pf (b ∈ (B ∪ C))  by: binunionIR B C b L17
L19 : pf (b ∈ (A ∩ (B ∪ C)))  by: binintersectI A (B ∪ C) b L16 L18
L20 : pf (b ∈ (A ∩ (B ∪ C)))

by: binunionEcases (A ∩ B) (A ∩ C) b (b ∈ (A ∩ (B ∪ C)))

L11 (λF L15) (λG L19)
L21 : pf (((A ∩ B) ∪ (A ∩ C)) ⊆ (A ∩ (B ∪ C)))
by: subsetI1 ((A ∩ B) ∪ (A ∩ C)) (A ∩ (B ∪ C)) (λb L20)

Figure 3: Proof of Distributivity Property

We next define a typed version of set difference (setminusT) and a typed version of complement (complementT).

setminusT_lem : ΠU:set. ΠA:(P U). ΠB:(P U). pf ((setminus A B) ∈ (P U))

setminusT : ΠU:set. (P U) → (P U) → (P U)

= λU λA λB ⟨ setminus A B, setminusT_lem U A B ⟩
complementT_lem : ΠU:set. ΠA:(P U). pf ((setminus U A) ∈ (P U))
complementT : ΠU:set. (P U) → (P U)
= λU λA ⟨ setminus U A, complementT_lem U A ⟩

We use K̂A to denote (complementT U A).

We next give proof principles (omitting definitions, i.e., proof terms) for “typed sets”:

setextT : ΠU:set. ΠA:(P U). ΠB:(P U). (Πx:U. pf (x ∈ A) → pf (x ∈ B)) → (Πx:U. pf (x ∈ B) → pf (x ∈ A)) → pf (A = B)

subsetTI : ΠU:set. ΠA:(P U). ΠB:(P U). (Πx:U. pf (x ∈ A) → pf (x ∈ B)) → pf (A ⊆ B)

powersetTI : ΠU:set. ΠA:(P U). ΠB:(P U). pf (A ⊆ B) → pf (A ∈ P̂ B)

powersetTE : ΠU:set. ΠA:(P U). ΠB:(P U). pf (A ∈ P̂ B) → pf (A ⊆ B)

powersetTI1 : ΠU:set. ΠA:(P U). ΠB:(P U). (Πx:U. pf (x ∈ A) → pf (x ∈ B)) → pf (A ∈ P̂ B)

powersetTE1 : ΠU:set. ΠA:(P U). ΠB:(P U). Πx:U. pf (A ∈ P̂ B) → pf (x ∈ A) → pf (x ∈ B)

complementTI : ΠU:set. ΠA:(P U). Πx:U. pf (¬x ∈ A) → pf (x ∈ K̂ A)

complementTE : ΠU:set. ΠA:(P U). Πx:U. pf (x ∈ K̂ A) → pf (¬x ∈ A)

complementTI1 : ΠU:set. ΠA:(P U). Πx:U. pf (x ∈ A) → pf (¬x ∈ K̂ A)

complementTE1 : ΠU:set. ΠA:(P U). Πx:U. pf (¬x ∈ K̂ A) → pf (x ∈ A)

binintersectTEL : ΠU:set. ΠA:(P U). ΠB:(P U). Πx:U. pf (x ∈ A ˆ∩ B) → pf (x ∈ A)

binintersectTER : ΠU:set. ΠA:(P U). ΠB:(P U). Πx:U. pf (x ∈ A ˆ∩ B) → pf (x ∈ B)

binintersectTI : ΠU:set. ΠA:(P U). ΠB:(P U). Πx:U . pf (x ∈ A) → pf (x ∈ B) → pf (x ∈ A ˆ∩ B)

binintersectTELcontra : ΠU:set. ΠA:(P U). ΠB:(P U). Πx:U . pf (¬x ∈ A) → pf (¬x ∈ A ˆ∩ B) binintersectTERcontra : ΠU:set. ΠA:(P U). ΠB:(P U). Πx:U . pf (¬x ∈ B) → pf (¬x ∈ A ˆ∩ B) contrasubsetT : ΠU:set. ΠA:(P U). ΠB:(P U). Πx:U. pf (A ⊆ K̂ B) → pf (x ∈ B) → pf (¬x ∈ A) contrasubsetT1 : ΠU:set. ΠA:(P U). ΠB:(P U). Πx:U. pf (A ⊆ B) → pf (¬x ∈ B) → pf (¬x ∈ A) contrasubsetT2 : ΠU:set. ΠA:(P U). ΠB:(P U). pf (A ⊆ B) → pf (K̂ B ⊆ K̂ A) contrasubsetT3 : ΠU:set. ΠA:(P U). ΠB:(P U). pf (K̂ B ⊆ K̂ A) → pf (A ⊆ B) doubleComplementI1 : ΠU:set. ΠA:(P U). Πx:U. pf (x ∈ A) → pf (x ∈ K̂ (K̂ A)) doubleComplementE1 : ΠU:set. ΠA:(P U). Πx:U. pf (x ∈ K̂ (K̂ A)) → pf (x ∈ A)

doubleComplementSub1 : ΠU:set. ΠA:(P U). pf (A ⊆ K̂ (K̂ A))
doubleComplementSub2 : ΠU:set. ΠA:(P U). pf (K̂ (K̂ A) ⊆ A)
doubleComplementEq : ΠU:set. ΠA:(P U). pf (A = K̂ (K̂ A))

binintersectTSub1 : ΠU:set. ΠA:(P U). ΠB:(P U). pf (A ˆ∩ B ⊆ A) binintersectTSub2 : ΠU:set. ΠA:(P U). ΠB:(P U). pf (A ˆ∩ B ⊆ B)

complementTnotintersectT : ΠU:set. ΠA:(P U). ΠB:(P U). Πx:U .

pf (x ∈ K̂ A) → pf (¬x ∈ A ˆ∩ B)

complementImpComplementIntersect : ΠU:set. ΠA:(P U). ΠB:(P U). Πx:U .

pf (x ∈ K̂ A) → pf (x ∈ K̂ (A ˆ∩ B))

complementSubsetComplementIntersect : ΠU:set. ΠA:(P U). ΠB:(P U) .

pf (K̂ A ⊆ K̂ (A ˆ∩ B))

complementInPowersetComplementIntersect : ΠU:set. ΠA:(P U). ΠB:(P U) .

pf (K̂ A ∈ P̂ (K̂ (A ˆ∩ B)))

contraSubsetComplement : ΠU:set. ΠA:(P U). ΠB:(P U) .

pf (A ⊆ K̂ B) → Πx:U. pf (x ∈ B) → pf (x ∈ K̂ A)

complementTcontraSubset : ΠU:set.ΠA:(P U).ΠB:(P U).pf (A ⊆ K̂ B)

→ pf (B ⊆ K̂ A) binunionTIL : ΠU:set. ΠA:(P U). ΠB:(P U). Πx:U. pf (x ∈ A) → pf (x ∈ A ˆ∪ B) binunionTIR : ΠU:set. ΠA:(P U). ΠB:(P U). Πx:U. pf (x ∈ B) → pf (x ∈ A ˆ∪ B) binunionTILcontra : ΠU:set.ΠA:(P U).ΠB:(P U).Πx:U.pf (¬x ∈ Aˆ∪B) → pf (¬x ∈ A) binunionTIRcontra : ΠU:set.ΠA:(P U).ΠB:(P U).Πx:U.pf (¬x ∈ Aˆ∪B) → pf (¬x ∈ B) binunionTSub1 : ΠU:set. ΠA:(P U). ΠB:(P U). pf (A ⊆ A ˆ∪ B) binunionTSub2 : ΠU:set. ΠA:(P U). ΠB:(P U). pf (B ⊆ A ˆ∪ B) inIntersectImpInUnion : ΠU:set. ΠA:(P U). ΠB:(P U). ΠC:(P U). Πx:U . pf (x ∈ A ˆ∩ B) → pf (x ∈ A ˆ∪ C) inIntersectImpInUnion2 : ΠU:set. ΠA:(P U). ΠB:(P U). ΠC:(P U). Πx:U . pf (x ∈ A ˆ∩ B) → pf (x ∈ B ˆ∪ C)

inIntersectImpInIntersectUnions : ΠU:set.ΠA:(P U).ΠB:(P U).ΠC:(P U).

Πx:U. pf (x ∈ A ˆ∩ B) → pf (x ∈ (A ˆ∪ C) ˆ∩ (B ˆ∪ C))

intersectInPowersetIntersectUnions : ΠU:set.ΠA:(P U).ΠB:(P U).ΠC:(P U).

pf (A ˆ∩ B ∈ P̂ ((A ˆ∪ C) ˆ∩ (B ˆ∪ C)))

inComplementUnionImpNotIn1 : ΠU:set. ΠA:(P U). ΠB:(P U). Πx:U .

pf (x ∈ K̂ (A ˆ∪ B)) → pf (¬x ∈ A)

inComplementUnionImpInComplement1 : ΠU:set. ΠA:(P U). ΠB:(P U). Πx:U .

pf (x ∈ K̂ (A ˆ∪ B)) → pf (x ∈ K̂ A) binunionTE1 : ΠU:set. ΠA:(P U). ΠB:(P U). Πx:U. pf (x ∈ A ˆ∪ B) → pf ((x ∈ A) ∨ (x ∈ B)) binunionTE : ΠU:set. ΠA:(P U). ΠB:(P U). Πϕ:prop. Πx:U. pf (x ∈ A ˆ∪ B) → (pf (x ∈ A) → pf ϕ) → (pf (x ∈ B) → pf ϕ) → pf ϕ binunionTEcontra : ΠU:set. ΠA:(P U). ΠB:(P U). Πx:U . pf (¬x ∈ A) → pf (¬x ∈ B) → pf (¬x ∈ A ˆ∪ B)

The following are versions of the DeMorgan’s Law. demorgan2a1 : ΠU:set.ΠA:(PU).ΠB:(PU).Πx:U.pf (x ∈ K̂(Aˆ∪B)) → pf (x ∈ K̂A) demorgan2a2 : ΠU:set.ΠA:(PU).ΠB:(PU).Πx:U.pf (x ∈ K̂(Aˆ∪B)) → pf (x ∈ K̂B) demorgan1 : ΠU:set.ΠA:(PU).ΠB:(PU).pf (K̂(Aˆ∩B) = (K̂A)ˆ∪(K̂B)) demorgan2 : ΠU:set.ΠA:(PU).ΠB:(PU).pf (K̂(Aˆ∪B) = (K̂A)ˆ∩(K̂B))

The following rules are especially relevant to the problem woz1_3. woz13rule0 : ΠU:set. ΠA:(P U). ΠB:(P U). ΠC:set. pf (C ∈ A ˆ∩ B) → pf (C ∈ U) woz13rule1 : ΠU:set. ΠA:(P U). ΠB:(P U). ΠC:(P U). pf (A ⊆ C) → pf (A ˆ∩ B ⊆ C) woz1_1 : ΠU:set. ΠA:(P U). ΠB:(P U). pf (K̂ A ∈ P̂ (K̂ (A ˆ∩ B))) = λU λA λB powersetTI1 U (K̂ A) (K̂ (A ˆ∩ B)) (λx λD L3) using proof steps

L1 : pf (¬x ∈ A)  by: complementTE U A x D

L2 : pf (¬x ∈ A ˆ∩ B)  by: binintersectTELcontra U A B x L1

L3 : pf (x ∈ K̂ (A ˆ∩ B))  by: complementTI U (A ˆ∩ B) x L2

Figure 4: woz1_1

woz1_2 : ΠU:set. ΠA:(P U). ΠB:(P U). ΠC:(P U). ΠD:(P U) . pf (K̂ ((A ˆ∪ B) ˆ∩ (C ˆ∪ D)) = ((K̂ A) ˆ∩ (K̂ B)) ˆ∪ ((K̂ C) ˆ∩ (K̂ D))) = λU λA λB λC λD eqCE (in (P U)) (K̂ (C ˆ∪ D)) ((K̂ C) ˆ∩ (K̂ D)) (λX K̂ ((A ˆ∪ B) ˆ∩ (C ˆ∪ D)) = ((K̂ A) ˆ∩ (K̂ B)) ˆ∪ X) L1 L4 using proof steps

L1 : pf (K̂ (C ˆ∪ D) = (K̂ C) ˆ∩ (K̂ D))  by: demorgan2 U C D
L2 : pf (K̂ (A ˆ∪ B) = (K̂ A) ˆ∩ (K̂ B))  by: demorgan2 U A B
L3 : pf (K̂ ((A ˆ∪ B) ˆ∩ (C ˆ∪ D)) = (K̂ (A ˆ∪ B)) ˆ∪ (K̂ (C ˆ∪ D)))
by: demorgan1 U (A ˆ∪ B) (C ˆ∪ D)
L4 : pf (K̂ ((A ˆ∪ B) ˆ∩ (C ˆ∪ D)) = ((K̂ A) ˆ∩ (K̂ B)) ˆ∪ (K̂ (C ˆ∪ D)))

by: eqCE (in (P U)) (K̂ (A ˆ∪ B)) ((K̂ A) ˆ∩ (K̂ B)) (λX K̂ ((A ˆ∪ B) ˆ∩ (C ˆ∪ D)) = X ˆ∪ (K̂ (C ˆ∪ D))) L2 L3

Figure 5: woz1_2

woz13rule2 : ΠU:set. ΠA:(P U). ΠB:(P U). ΠC:(P U). pf (B ⊆ C) → pf (A ˆ∩ B ⊆ C)

woz13rule3 : ΠU:set. ΠA:(P U). ΠB:(P U). ΠC:(P U). pf (A ⊆ B) → pf (A ⊆ C) → pf (A ⊆ B ˆ∩ C)

woz13rule4 : ΠU:set.ΠA:(P U).ΠB:(P U).ΠC:(P U).ΠD:(P U). pf (A ⊆ C) → pf (B ⊆ D) → pf (A ˆ∩ B ⊆ C ˆ∩ D)

Finally, we formulate abbreviations with types corresponding to the five problems in the Wizard of Oz experiment described in [5]. We also give sample proof terms. To analyze the proof attempts of students, alternative proofs will likely need to be considered. In fact, one likely needs to consider partial proof terms which could be represented by terms which have free variables of proof type which need to be instantiated with subproofs. These abbreviations are woz1_1 (see Figure 4), woz1_2 (see Figure 5), woz1_3 (see Figure 6), woz1_4 (see Figure 7), and woz1_5 (see Figure 8). woz1_3 : ΠU:set. ΠA:(P U). ΠB:(P U). ΠC:(P U) . pf (A ˆ∩ B ∈ P̂ ((A ˆ∪ C) ˆ∩ (B ˆ∪ C))) = λU λA λB λC powersetTI U (A ˆ∩ B) ((A ˆ∪ C) ˆ∩ (B ˆ∪ C)) L5 using proof steps

L1 : pf (A ⊆ A ˆ∪ C)  by: binunionTSub1 U A C
L2 : pf (A ˆ∩ B ⊆ A ˆ∪ C)  by: woz13rule1 U A B (A ˆ∪ C) L1
L3 : pf (B ⊆ B ˆ∪ C)  by: binunionTSub1 U B C
L4 : pf (A ˆ∩ B ⊆ B ˆ∪ C)  by: woz13rule2 U A B (B ˆ∪ C) L3
L5 : pf (A ˆ∩ B ⊆ (A ˆ∪ C) ˆ∩ (B ˆ∪ C))
by: woz13rule3 U (A ˆ∩ B) (A ˆ∪ C) (B ˆ∪ C) L2 L4

Figure 6: woz1_3

woz1_4 : ΠU:set. ΠA:(P U). ΠB:(P U). pf (A ⊆ K̂ B) → pf (B ⊆ K̂ A) = λU λA λB λD subsetTI U B (K̂ A) (λx λE L2) using proof steps

L1 : pf (¬x ∈ A)  by: contrasubsetT U A B x D E
L2 : pf (x ∈ K̂ A)  by: complementTI U A x L1

Figure 7: woz1_4

woz1_5 : ΠU:set. ΠA:(P U). ΠB:(P U). pf (K̂ (A ˆ∪ B) ∈ P̂ (K̂ A)) = λU λA λB powersetTI1 U (K̂ (A ˆ∪ B)) (K̂ A) (λx λD L1) using proof step

L1 : pf (x ∈ K̂ A)  by: demorgan2a1 U A B x D

Figure 8: woz1_5

5.2 Formalizing the Second DiaLog Wizard of Oz Experiment: Relations

The following abbreviations concern relations and are relevant to the second Wizard of Oz experiment in the DiaLog project [6, 31].

We omit the definition of breln1, but the idea is that (breln1 M R) holds iff R ⊆ M×M (i.e., R is a binary relation on M). We will use (breln1 M) – which has type set → prop – as a class type.

breln1 : set → set → prop

The following correspond to derivable rules which are useful for this domain:

breln1all1 : ΠM:set. ΠR:(breln1 M). Πϕ:(set → prop) .

(Πa:M. Πb:M. pf (⟨⟨ a, b ⟩⟩ ∈ R) → pf (ϕ ⟨⟨ a, b ⟩⟩)) → pf (∀c ∈ R. ϕ c)

subbreln1 : ΠM:set. ΠR:(breln1 M). ΠS:(breln1 M) .

(Πa:M. Πb:M. pf (⟨⟨ a, b ⟩⟩ ∈ R) → pf (⟨⟨ a, b ⟩⟩ ∈ S)) → pf (R ⊆ S)

eqbreln1 : ΠM:set. ΠR:(breln1 M). ΠS:(breln1 M) .

(Πa:M. Πb:M. pf (⟨⟨ a, b ⟩⟩ ∈ R) → pf (⟨⟨ a, b ⟩⟩ ∈ S)) → (Πa:M. Πb:M. pf (⟨⟨ a, b ⟩⟩ ∈ S) → pf (⟨⟨ a, b ⟩⟩ ∈ R)) → pf (R = S)

We define the inverse of a binary relation R on M using the “set of pairs constructor” dpsetconstr. We will do this in three steps: define the untyped set which is the inverse of R, prove this untyped set is a binary relation on M, pair the previous two abbreviations to have an inverse operator which expects a binary relation on M and returns a binary relation on M. Explicitly defining the untyped set is optional.

breln1invset : ΠM:set. (breln1 M) → set

= λM λR {⟨⟨a, b⟩⟩ ∈ M × M | ⟨⟨ b, a ⟩⟩ ∈ R }

breln1invprop : ΠM:set. ΠR:(breln1 M). pf (breln1 M (breln1invset M R))
breln1inv : ΠM:set. (breln1 M) → (breln1 M)
= λM λR ⟨ breln1invset M R, breln1invprop M R ⟩

We use R^{−1} to denote the term (breln1inv M R) where M is a fixed bound variable.

Now that we have defined the inverse operator, we can derive two proof rules. We can always use these two proof rules instead of expanding the definition of breln1inv or

breln1invset above.

breln1invI : ΠM:set. ΠR:(breln1 M). Πa:M. Πb:M. pf (⟨⟨ a, b ⟩⟩ ∈ R) → pf (⟨⟨ b , a ⟩⟩ ∈ R^{−1})

breln1invE : ΠM:set. ΠR:(breln1 M). Πa:M. Πb:M. pf (⟨⟨ b, a ⟩⟩ ∈ R^{−1}) → pf (⟨⟨ a, b ⟩⟩ ∈ R)

Following a similar outline, we define the composition of two relations on a set.

breln1compset : ΠM:set. (breln1 M) → (breln1 M) → set

= λM λR λS {⟨⟨a, b⟩⟩ ∈ M × M | ∃c ∈ M. (⟨⟨ a, c ⟩⟩ ∈ R) ∧ (⟨⟨ c, b ⟩⟩ ∈ S) }

breln1compprop : ΠM:set.ΠR:(breln1 M).ΠS:(breln1 M).
pf (breln1 M (breln1compset M R S))
breln1comp : ΠM:set. (breln1 M) → (breln1 M) → (breln1 M)
= λM λR λS ⟨ breln1compset M R S, breln1compprop M R S ⟩

We use R ∘ S to denote the term (breln1comp M R S) where M is a fixed bound variable. Introduction and elimination rules for ∘ follow:

breln1compI : ΠM:set. ΠR:(breln1 M).ΠS:(breln1 M).Πa:M.Πb:M.Πc:M. pf (⟨⟨ a, c ⟩⟩ ∈ R) → pf (⟨⟨ c, b ⟩⟩ ∈ S) → pf (⟨⟨ a, b ⟩⟩ ∈ R ∘ S)

breln1compE : ΠM:set. ΠR:(breln1 M). ΠS:(breln1 M). Πa:M. Πb:M . pf (⟨⟨ a, b ⟩⟩ ∈ R ∘ S) → pf (∃c ∈ M. (⟨⟨ a, c ⟩⟩ ∈ R) ∧ (⟨⟨ c, b ⟩⟩ ∈ S))

Finally, we define a notion of binary union on binary relations on M. This time we do not explicitly define the untyped set since in fact the untyped set is already defined by binunion (for which we use the infix notation ∪). Note that in the definition of breln1union below the term (R ∪ S) is shorthand for (binunion R S) which in turn is shorthand for (binunion π_{1}(R) π_{1}(S)).

breln1unionprop : ΠM:set.ΠR:(breln1 M).ΠS:(breln1 M).pf (breln1 M (R ∪ S))
breln1union : ΠM:set. (breln1 M) → (breln1 M) → (breln1 M)

= λM λR λS ⟨ R ∪ S, breln1unionprop M R S ⟩

Note that X ∪Y is already used for untyped binary union (binunion X Y) and ˆ∪ is already used for typed binary union (binunionT U A B) relative to a fixed U. For binary union of binary relations on a fixed set M, we use R ˙∪S to denote (breln1union M R S). Rules for ˙∪ follow:

breln1unionIL : ΠM:set. ΠR:(breln1 M). ΠS:(breln1 M). Πa:M. Πb:M . pf (⟨⟨ a, b ⟩⟩ ∈ R) → pf (⟨⟨ a, b ⟩⟩ ∈ R ˙∪ S)

breln1unionIR : ΠM:set. ΠR:(breln1 M). ΠS:(breln1 M). Πa:M. Πb:M . pf (⟨⟨ a, b ⟩⟩ ∈ S) → pf (⟨⟨ a, b ⟩⟩ ∈ R ˙∪ S)

breln1unionI : ΠM:set. ΠR:(breln1 M). ΠS:(breln1 M). Πa:M. Πb:M . pf ((⟨⟨ a, b ⟩⟩ ∈ R) ∨ (⟨⟨ a, b ⟩⟩ ∈ S)) → pf (⟨⟨ a, b ⟩⟩ ∈ R ˙∪ S)

breln1unionE : ΠM:set. ΠR:(breln1 M). ΠS:(breln1 M). Πa:M. Πb:M . pf (⟨⟨ a, b ⟩⟩ ∈ R ˙∪ S) → pf ((⟨⟨ a, b ⟩⟩ ∈ R) ∨ (⟨⟨ a, b ⟩⟩ ∈ S))

breln1unionEcases : ΠM:set.ΠR:(breln1 M).ΠS:(breln1 M).Πa:M.Πb:M.

pf (⟨⟨ a, b ⟩⟩ ∈ R ˙∪ S) → Πϕ:prop. (pf (⟨⟨ a, b ⟩⟩ ∈ R) → pf ϕ) → (pf (⟨⟨ a, b ⟩⟩ ∈ S) → pf ϕ) → pf ϕ

breln1unionCommutes : ΠM:set.ΠR:(breln1 M).ΠS:(breln1 M).pf (R ˙∪S = S ˙∪R)

We now give four abbreviations woz2Ex (see Figure 9), woz2W (see Figure 10), woz2A (see Figures 11 and 12), and woz2B (see Figure 13). The types of these abbreviations correspond to the problem in the Wizard of Oz experiment described in [31]. We include sample proof woz2Ex : ΠM:set. ΠR:(breln1 M). pf (R = (R^{−1})^{−1}) = λM λR setextsub R (R^{−1})^{−1} L3 L6 using proof steps

Let a have type M Let b have type M

D  Assume ⟨⟨ a, b ⟩⟩ ∈ R
L1 : pf (⟨⟨ b, a ⟩⟩ ∈ R^{−1})  by: breln1invI M R a b D
L2 : pf (⟨⟨ a, b ⟩⟩ ∈ (R^{−1})^{−1})  by: breln1invI M R^{−1} b a L1
L3 : pf (R ⊆ (R^{−1})^{−1})  by: subbreln1 M R ((R^{−1})^{−1}) (λa λb λD L2)

Let a have type M Let b have type M

E  Assume ⟨⟨ a, b ⟩⟩ ∈ (R^{−1})^{−1}
L4 : pf (⟨⟨ b, a ⟩⟩ ∈ R^{−1})  by: breln1invE M R^{−1} b a E
L5 : pf (⟨⟨ a, b ⟩⟩ ∈ R)  by: breln1invE M R a b L4
L6 : pf ((R^{−1})^{−1} ⊆ R)  by: subbreln1 M ((R^{−1})^{−1}) R (λa λb λE L5)

Figure 9: woz2Ex

terms as well. As with the other Wizard of Oz experiment, one should consider other proof terms and partial proofs (proof terms with variables) to evaluate student responses. woz2W : ΠM:set.ΠR:(breln1 M).ΠS:(breln1 M).pf ((R ∘ S)^{−1} = S^{−1} ∘ R^{−1}) = λM λR λS setextsub (R ∘ S)^{−1} (S^{−1} ∘ R^{−1}) L9 L18 using proof steps

Let a have type M Let b have type M

D  Assume ⟨⟨ a , b ⟩⟩ ∈ (R ∘ S)^{−1}
L1 : pf (⟨⟨ b , a ⟩⟩ ∈ R ∘ S)  by: breln1invE M (R ∘ S) b a D
L2 : pf (∃c ∈ M. (⟨⟨ b , c ⟩⟩ ∈ R) ∧ (⟨⟨ c , a ⟩⟩ ∈ S))

                                         by: breln1compE M R S b a L1

Let c have type M

E  Assume (⟨⟨ b , c ⟩⟩ ∈ R) ∧ (⟨⟨ c , a ⟩⟩ ∈ S)
L3 : pf (⟨⟨ c , a ⟩⟩ ∈ S)  by: andER (⟨⟨ b , c ⟩⟩ ∈ R) (⟨⟨ c , a ⟩⟩ ∈ S) E
L4 : pf (⟨⟨ a , c ⟩⟩ ∈ S^{−1})  by: breln1invI M S c a L3
L5 : pf (⟨⟨ b , c ⟩⟩ ∈ R)  by: andEL (⟨⟨ b , c ⟩⟩ ∈ R) (⟨⟨ c , a ⟩⟩ ∈ S) E
L6 : pf (⟨⟨ c , b ⟩⟩ ∈ R^{−1})  by: breln1invI M R b c L5
L7 : pf (⟨⟨ a , b ⟩⟩ ∈ S^{−1} ∘ R^{−1})  by: breln1compI M S^{−1} R^{−1} a b c L4 L6
L8 : pf (⟨⟨ a , b ⟩⟩ ∈ S^{−1} ∘ R^{−1})
by: \begin{matrix}dexE M (λc (⟨⟨ b , c ⟩⟩ ∈ R) ∧ (⟨⟨ c , a ⟩⟩ ∈ S)) L2 \\ (⟨⟨ a , b ⟩⟩ ∈ S^{−1} ∘ R^{−1}) (λc λE L7) \end{matrix}
L9 : pf ((R ∘ S)^{−1} ⊆ S^{−1} ∘ R^{−1})
by: subbreln1 M ((R ∘ S)^{−1}) (S^{−1} ∘ R^{−1}) (λa λb λD L8)

Let a have type M Let b have type M

F  Assume ⟨⟨ a , b ⟩⟩ ∈ S^{−1} ∘ R^{−1}
L10 : pf (∃c ∈ M. (⟨⟨ a , c ⟩⟩ ∈ S^{−1}) ∧ (⟨⟨ c , b ⟩⟩ ∈ R^{−1}))
by: breln1compE M S^{−1} R^{−1} a b F

Let c have type M

G  Assume (⟨⟨ a , c ⟩⟩ ∈ S^{−1}) ∧ (⟨⟨ c , b ⟩⟩ ∈ R^{−1})
L11 : pf (⟨⟨ c , b ⟩⟩ ∈ R^{−1})  by: andER (⟨⟨ a , c ⟩⟩ ∈ S^{−1}) (⟨⟨ c , b ⟩⟩ ∈ R^{−1}) G
L12 : pf (⟨⟨ b , c ⟩⟩ ∈ R)  by: breln1invE M R b c L11
L13 : pf (⟨⟨ a , c ⟩⟩ ∈ S^{−1})  by: andEL (⟨⟨ a , c ⟩⟩ ∈ S^{−1}) (⟨⟨ c , b ⟩⟩ ∈ R^{−1}) G
L14 : pf (⟨⟨ c , a ⟩⟩ ∈ S)  by: breln1invE M S c a L13
L15 : pf (⟨⟨ b , a ⟩⟩ ∈ R ∘ S)  by: breln1compI M R S b a c L12 L14
L16 : pf (⟨⟨ a , b ⟩⟩ ∈ (R ∘ S)^{−1})  by: breln1invI M (R ∘ S) b a L15
L17 : pf (⟨⟨ a , b ⟩⟩ ∈ (R ∘ S)^{−1})
by: \begin{matrix}dexE M (λc (⟨⟨ a , c ⟩⟩ ∈ S^{−1}) ∧ (⟨⟨ c , b ⟩⟩ ∈ R^{−1})) L10 \\ (⟨⟨ a , b ⟩⟩ ∈ (R ∘ S)^{−1}) (λc λG L16) \end{matrix}
L18 : pf (S^{−1} ∘ R^{−1} ⊆ (R ∘ S)^{−1})
by: subbreln1 M (S^{−1} ∘ R^{−1}) ((R ∘ S)^{−1}) (λa λb λF L17)

Figure 10: woz2W

woz2A : ΠM:set. ΠR:(breln1 M). ΠS:(breln1 M). ΠT:(breln1 M) .

pf ((R ˙∪ S) ∘ T = (R ∘ T) ˙∪ (S ∘ T)) = λM λR λS λT setextsub (R ˙∪ S) ∘ T (R ∘ T) ˙∪ (S ∘ T) L12 L27 using proof steps

Let a have type M Let b have type M

D  Assume ⟨⟨ a , b ⟩⟩ ∈ (R ˙∪ S) ∘ T
L1 : pf (∃c ∈ M. (⟨⟨ a , c ⟩⟩ ∈ R ˙∪ S ∧ ⟨⟨ c , b ⟩⟩ ∈ T))
by: breln1compE M (R ˙∪ S) T a b D

Let c have type M

E  Assume ⟨⟨ a , c ⟩⟩ ∈ R ˙∪ S ∧ ⟨⟨ c , b ⟩⟩ ∈ T
L2 : pf (⟨⟨ a , c ⟩⟩ ∈ R ˙∪ S)  by: andEL (⟨⟨ a , c ⟩⟩ ∈ R ˙∪ S) (⟨⟨ c , b ⟩⟩ ∈ T) E
L3 : pf ((⟨⟨ a , c ⟩⟩ ∈ R) ∨ (⟨⟨ a , c ⟩⟩ ∈ S))  by: breln1unionE M R S a c L2
F  Assume ⟨⟨ a , c ⟩⟩ ∈ R
L4 : pf (⟨⟨ c , b ⟩⟩ ∈ T)  by: andER (⟨⟨ a , c ⟩⟩ ∈ R ˙∪ S) (⟨⟨ c , b ⟩⟩ ∈ T) E
L5 : pf (⟨⟨ a , b ⟩⟩ ∈ R ∘ T)  by: breln1compI M R T a b c F L4
L6 : pf (⟨⟨ a , b ⟩⟩ ∈ (R ∘ T) ˙∪ (S ∘ T))
by: breln1unionIL M (R ∘ T) (S ∘ T) a b L5
G  Assume ⟨⟨ a , c ⟩⟩ ∈ S
L7 : pf (⟨⟨ c , b ⟩⟩ ∈ T)  by: andER (⟨⟨ a , c ⟩⟩ ∈ R ˙∪ S) (⟨⟨ c , b ⟩⟩ ∈ T) E
L8 : pf (⟨⟨ a , b ⟩⟩ ∈ S ∘ T)  by: breln1compI M S T a b c G L7
L9 : pf (⟨⟨ a , b ⟩⟩ ∈ (R ∘ T) ˙∪ (S ∘ T))
by: breln1unionIR M (R ∘ T) (S ∘ T) a b L8
L10 : pf (⟨⟨ a , b ⟩⟩ ∈ (R ∘ T) ˙∪ (S ∘ T))
by: \begin{matrix}orE (⟨⟨ a , c ⟩⟩ ∈ R) (⟨⟨ a , c ⟩⟩ ∈ S) L3 \\ (⟨⟨ a , b ⟩⟩ ∈ (R ∘ T) ˙∪ (S ∘ T)) (λF L6) (λG L9) \end{matrix}
L11 : pf (⟨⟨ a , b ⟩⟩ ∈ (R ∘ T) ˙∪ (S ∘ T))
by: \begin{matrix}dexE M (λc (⟨⟨ a , c ⟩⟩ ∈ R ˙∪ S) ∧ (⟨⟨ c , b ⟩⟩ ∈ T)) L1 \\ (⟨⟨ a , b ⟩⟩ ∈ (R ∘ T) ˙∪ (S ∘ T)) (λc λE L10) \end{matrix}
L12 : pf ((R ˙∪ S) ∘ T ⊆ (R ∘ T) ˙∪ (S ∘ T))
by: subbreln1 M ((R ˙∪ S) ∘ T) ((R ∘ T) ˙∪ (S ∘ T)) (λa λb λD L11)

Figure 11: woz2A, Part 1 Let a have type M Let b have type M

E^{0}  Assume ⟨⟨ a , b ⟩⟩ ∈ (R ∘ T) ˙∪ (S ∘ T)
L13 : pf ((⟨⟨ a , b ⟩⟩ ∈ R ∘ T) ∨ (⟨⟨ a , b ⟩⟩ ∈ S ∘ T))
by: breln1unionE M (R ∘ T) (S ∘ T) a b E^{0}
F^{0}  Assume ⟨⟨ a , b ⟩⟩ ∈ R ∘ T
L14 : pf (∃c ∈ M. (⟨⟨ a , c ⟩⟩ ∈ R) ∧ (⟨⟨ c , b ⟩⟩ ∈ T))

                                           by: breln1compE M R T a b F^{0}

Let c have type M

G^{0}  Assume (⟨⟨ a , c ⟩⟩ ∈ R) ∧ (⟨⟨ c , b ⟩⟩ ∈ T)
L15 : pf (⟨⟨ a , c ⟩⟩ ∈ R)  by: andEL (⟨⟨ a , c ⟩⟩ ∈ R) (⟨⟨ c , b ⟩⟩ ∈ T) G^{0}
L16 : pf (⟨⟨ a , c ⟩⟩ ∈ R ˙∪ S)  by: breln1unionIL M R S a c L15
L17 : pf (⟨⟨ c , b ⟩⟩ ∈ T)  by: andER (⟨⟨ a , c ⟩⟩ ∈ R) (⟨⟨ c , b ⟩⟩ ∈ T) G^{0}
L18 : pf (⟨⟨ a , b ⟩⟩ ∈ (R ˙∪ S) ∘ T) by: breln1compI M (R ˙∪ S) T a b c L16 L17
L19 : pf (⟨⟨ a , b ⟩⟩ ∈ (R ˙∪ S) ∘ T)
by: \begin{matrix}dexE M (λc (⟨⟨ a , c ⟩⟩ ∈ R) ∧ (⟨⟨ c , b ⟩⟩ ∈ T)) L14 \\ (⟨⟨ a , b ⟩⟩ ∈ (R ˙∪ S) ∘ T) (λc λG^{0} L18) \end{matrix}
D^{1}  Assume ⟨⟨ a , b ⟩⟩ ∈ S ∘ T
L20 : pf (∃c ∈ M. (⟨⟨ a , c ⟩⟩ ∈ S) ∧ (⟨⟨ c , b ⟩⟩ ∈ T))

                                           by: breln1compE M S T a b D^{1}

Let c have type M

E^{1}  Assume (⟨⟨ a , c ⟩⟩ ∈ S) ∧ (⟨⟨ c , b ⟩⟩ ∈ T)
L21 : pf (⟨⟨ a , c ⟩⟩ ∈ S)  by: andEL (⟨⟨ a , c ⟩⟩ ∈ S) (⟨⟨ c , b ⟩⟩ ∈ T) E^{1}
L22 : pf (⟨⟨ a , c ⟩⟩ ∈ R ˙∪ S)  by: breln1unionIR M R S a c L21
L23 : pf (⟨⟨ c , b ⟩⟩ ∈ T)  by: andER (⟨⟨ a , c ⟩⟩ ∈ S) (⟨⟨ c , b ⟩⟩ ∈ T) E^{1}
L24 : pf (⟨⟨ a , b ⟩⟩ ∈ (R ˙∪ S) ∘ T) by: breln1compI M (R ˙∪ S) T a b c L22 L23
L25 : pf (⟨⟨ a , b ⟩⟩ ∈ (R ˙∪ S) ∘ T)
by: \begin{matrix}dexE M (λc (⟨⟨ a , c ⟩⟩ ∈ S) ∧ (⟨⟨ c , b ⟩⟩ ∈ T)) L20 \\ (⟨⟨ a , b ⟩⟩ ∈ (R ˙∪ S) ∘ T) (λc λE^{1} L24) \end{matrix}
L26 : pf (⟨⟨ a , b ⟩⟩ ∈ (R ˙∪ S) ∘ T)
by: \begin{matrix}orE (⟨⟨ a , b ⟩⟩ ∈ R ∘ T) (⟨⟨ a , b ⟩⟩ ∈ S ∘ T) L13 \\ (⟨⟨ a , b ⟩⟩ ∈ (R ˙∪ S) ∘ T) (λF^{0} L19) (λD^{1} L25) \end{matrix}
L27 : pf ((R ∘ T) ˙∪ (S ∘ T) ⊆ (R ˙∪ S) ∘ T)
by: subbreln1 M ((R ∘ T) ˙∪ (S ∘ T)) ((R ˙∪ S) ∘ T) (λa λb λE^{0} L26)

Figure 12: woz2A, Part 2

woz2B : ΠM:set. ΠR:(breln1 M). ΠS:(breln1 M). ΠT:(breln1 M) .

pf ((R ˙∪ S) ∘ T = ((T^{−1} ∘ S^{−1})^{−1}) ˙∪ ((T^{−1} ∘ R^{−1})^{−1})) = λM λR λS λT transeq ((R ˙∪ S) ∘ T) ((T^{−1} ∘ R^{−1})^{−1} ˙∪ (T^{−1} ∘ S^{−1})^{−1}) ((T^{−1} ∘ S^{−1})^{−1} ˙∪ (T^{−1} ∘ R^{−1})^{−1}) L11 L12 using proof steps

L1 : pf ((T^{−1} ∘ S^{−1})^{−1} = ((S^{−1})^{−1} ∘ (T^{−1})^{−1}))  by: woz2W M T^{−1} S^{−1}
L2 : pf ((T^{−1} ∘ R^{−1})^{−1} = ((R^{−1})^{−1} ∘ (T^{−1})^{−1}))  by: woz2W M T^{−1} R^{−1}
L3 : pf (T = (T^{−1})^{−1})  by: woz2Ex M T
L4 : pf (S = (S^{−1})^{−1})  by: woz2Ex M S
L5 : pf (R = (R^{−1})^{−1})  by: woz2Ex M R
L6 : pf ((R ˙∪ S) ∘ T = (R ∘ T) ˙∪ (S ∘ T))  by: woz2A M R S T
L7 : pf ((R ˙∪ S) ∘ T = ((R^{−1})^{−1} ∘ T) ˙∪ (S ∘ T))

by:

eqCE (breln1 M) R (R^{−1})^{−1}
(λX (R ˙∪ S) ∘ T = (X ∘ T) ˙∪ (S ∘ T)) L5 L6
L8 : pf ((R ˙∪ S) ∘ T = ((R^{−1})^{−1} ∘ T) ˙∪ ((S^{−1})^{−1} ∘ T))

by:

eqCE (breln1 M) S (S^{−1})^{−1}
(λX (R ˙∪ S) ∘ T = ((R^{−1})^{−1} ∘ T) ˙∪ (X ∘ T)) L4 L7
L9 : pf ((R ˙∪ S) ∘ T = ((R^{−1})^{−1} ∘ (T^{−1})^{−1}) ˙∪ ((S^{−1})^{−1} ∘ (T^{−1})^{−1}))

by: eqCE (breln1 M) T (T^{−1})^{−1} (λX (R ˙∪ S) ∘ T = ((R^{−1})^{−1} ∘ X) ˙∪ ((S^{−1})^{−1} ∘ X)) L3 L8

L10 : pf ((R ˙∪ S) ∘ T = (T^{−1} ∘ R^{−1})^{−1} ˙∪ ((S^{−1})^{−1} ∘ (T^{−1})^{−1}))

by: eqCE2 (breln1 M) ((T^{−1} ∘ R^{−1})^{−1}) ((R^{−1})^{−1} ∘ (T^{−1})^{−1}) (λX (R ˙∪ S) ∘ T = X ˙∪ ((S^{−1})^{−1} ∘ (T^{−1})^{−1})) L2 L9

L11 : pf ((R ˙∪ S) ∘ T = (T^{−1} ∘ R^{−1})^{−1} ˙∪ (T^{−1} ∘ S^{−1})^{−1})

by: eqCE2 (breln1 M) (T^{−1} ∘ S^{−1})^{−1} ((S^{−1})^{−1} ∘ (T^{−1})^{−1}) (λX (R ˙∪ S) ∘ T = (T^{−1} ∘ R^{−1})^{−1} ˙∪ X) L1 L10

L12 : pf ((T^{−1} ∘ R^{−1})^{−1} ˙∪ (T^{−1} ∘ S^{−1})^{−1} = (T^{−1} ∘ S^{−1})^{−1} ˙∪ (T^{−1} ∘ R^{−1})^{−1})
by: breln1unionCommutes M (T^{−1} ∘ R^{−1})^{−1} (T^{−1} ∘ S^{−1})^{−1}

Figure 13: woz2B

6 Future Work

There are many avenues of research left for the future. We discuss several possibilities here.

6.1 Equality Reasoning

At the object level, we have equality between sets (given by eq) and equivalence between propositions (given by equiv). There is no object-level notion of equality between function types or proof types. Indeed, due to proof irrelevance, there is no need to consider equality between terms of a proof type, since any two terms are always equal if they are the same proof type. By a “proof type” here, we mean any type of the form

Πx^{1} :A^{1} ⋯ Πx^{n}:A^{n}pf M.

We have already defined a partial function Leib which in a sense corresponds to equality at arbitrary types, except those which return a proof type. We can give an alternative partial function Eq as follows:

• Eq((Πx:B.C), M, N) :=

(Πx:B.Eq(C, [x/x_{λ}^{M}]B_{λ}^{M}, [x/x_{λ}^{N}]B_{λ}^{N}))

when Eq(C, [x/x_{λ}^{M}]B_{λ}^{M}, [x/x_{λ}^{N}]B_{λ}^{N}) is defined.

• Eq(prop, M, N) := pf (M ≡ N).

• Eq(set, M, N) := (ΠP:(set → prop).pf (M = N)

• Eq(cl ϕ, M, N) := (ΠP:(set → prop).pf (π_{1}(M) = π_{1}(N)).

One can show by induction that for every non-proof type A, Eq(A, M, N) is inhabited iff Leib(A, M, N) is inhabited.

When replacing equals for equals within subterms, we need to know that if F and G are equal at type (Πx : AB) and M and N are equal at type A, then (F M) and (GN) are equal at type [M/x]B (or [N/x]B). Making sense of this can be tricky, since the types [M/x]B and [N/x]B are different, but should also be, in some sense, “the same”. The notion of “sameness” here should correspond to a form of isomorphism. That is, the existence of terms (in context) f : [M/x]B → [N/x]B and g : [N/x]B → [M/x]B such that the terms f ∘ g and g ∘ f are “equal” to the identity function at the appropriate types.

Assuming we can prove the existence of terms showing such types are isomorphic, we could define “congruence” types as follows:

• Cong^{1}((Πx:B.C), M, N) :=

(Πx:B.Πy:B.Πu:Eq(B, x, y).Cong^{1}(C, [x/x_{λ}^{M}]B_{λ}^{M}, f([y/x_{λ}^{N}]B_{λ}^{N})))

when Cong^{1}(B, x, y) and Cong^{1}(C, [x/x_{λ}^{M}]B_{λ}^{M}, [y/x_{λ}^{N}]B_{λ}^{N}) are defined and where f : [y/x]C → C is a term induced by the isomorphism of [y/x]C and C (in a context with x, y and u).

• Cong^{1}((Πx:B.C), M, N) :=

(Πx:B.Πy:B.Cong^{1}(C, [x/x_{λ}^{M}]B_{λ}^{M}, f([y/x_{λ}^{N}]B_{λ}^{N})))

when Cong^{1}(C, [x/x_{λ}^{M}]B_{λ}^{M}, f([y/x_{λ}^{N}]B_{λ}^{N})) is defined but Cong^{1}(B, x, y) is not defined (i.e., B is a proof type) and where f : [y/x]C → C is a term induced by the isomorphism of [y/x]C and C.

• Cong^{1}(prop, M, N) := pf (M ≡ N).

• Cong^{1}(set, M, N) := pf (M = N)

• Cong^{1}(cl ϕ, M, N) := pf (π_{1}(M) = π_{1}(N).

The expected results are the following:

1. For each type A with Γ ⊢ A : T ype^{i} with i ∈ {0, 1}, if Cong^{1}(A, x, x) is defined, then there is a term C_{A} such that Γ, x : A ⊢ C_{A} ↑ Cong^{1}(A, x, x).

2. For each logical constant c of type A, if Cong^{1}(A, c, c) is defined (i.e., A is not a proof type), then Cong^{1}(A, c, c) can be shown to be inhabited.

3. Cong^{1}(A, M, M) is inhabited (at least in some signature extended with new abbreviations of proof type) whenever · ⊢_{Σ} M ∼ M ↑ A and A is not a proof type.

4. If Eq(A, M, M), then Cong^{1}(A, M, M).

There are alternative (not necessarily equivalent) possible definitions of congruence types. For example, the following definition of Cong^{2}(A, B, M, N) avoids isomorphism of types by carrying two types as arguments. The idea is it is inhabited when M has type A, N has type B, A and B are isomorphic, and, up to isomorphism, M and N are equal.

• Cong^{2}((Πx:B.C), (Πy:B′.C′), M, N) :=

(Πx:B.Πy:B′.Πu:Cong^{2}(B, B′, x, y).Cong^{2}(C, C′, [x/x_{λ}^{M}]B_{λ}^{M}, f([y/x_{λ}^{N}]B_{λ}^{N})))

when Cong^{2}(B, B′, x, y) and Cong^{2}(C, C′, [x/x_{λ}^{M}]B_{λ}^{M}, [y/x_{λ}^{N}]B_{λ}^{N}) are defined.

• Cong^{2}((Πx:B.C), (Πy:B′.C′), M, N) :=

(Πx:B.Πy:B′.Cong^{2}(C, C′, [x/x_{λ}^{M}]B_{λ}^{M}, [y/x_{λ}^{N}]B_{λ}^{N}))

when Cong^{2}(C, [x/x_{λ}^{M}]B_{λ}^{M}, f([y/x_{λ}^{N}]B_{λ}^{N})) is defined but Cong^{2}(B, x, y) is not defined.

• Cong^{2}(prop, prop, M, N) := pf (M ≡ N).

• Cong^{2}(set, set, M, N) := pf (M = N)

• Cong^{2}(cl ϕ, cl ψ, M, N) := pf (π_{1}(M) = π_{1}(N).

Note that Cong^{2}(A, B, M, N) is only defined when A and B have similar structure and neither are proof types. What is the “best” definition of congruence types is questionable and left open.

One can use congruence types to replace equals by equals within terms and underneath binders. For instance, one could define judgments Γ ⊢^{E} M = N : A for whether two terms are equal up to a given set E of equations in context, then prove that if the judgment holds and A is not a proof type, then Cong^{1}(A, M, N) (or Cong^{2}(A, A, M, N)) is inhabited. At type prop, this means we can prove equivalence of M and N. If we know M and we can prove M ≡ N, then we can derive N. The details are left for future work.

6.2 Computations

One would like to use programs such as computer algebra systems to determine the truth of purely computational propositions and then build a DeTSeT proof term. This could especially be useful when working with, e.g., the natural numbers, real numbers, etc.

6.3 Inductive Definitions

One can encode inductively defined sets, relations and functions in ZFC (and so in DeTSeT). We sketch how such an encoding can be done by example.

Suppose S is intended to be the set inductively defined to contain an element nil and to be closed under a binary constructor cons. We can define a proposition ϕ(x, y) to be

∀z.z ∈ y ≡ ((z = ∅) ∨ (∃a^{1}, a^{2} ∈ x∃b^{1}, b^{2}.ϕ(a^{1}, b^{1}) ∧ ϕ(a^{2}, b^{2}) ∧ ∃v ∈ b^{1}∃w ∈ b^{2}.z = ⟨v, w⟩))

Using extensionality we know for all x there is at most one y such that ϕ(x, y) holds. Note ϕ(∅, {∅}) holds. For each finite ordinal n ∈ ω, assume ϕ(i, S_{i}) holds for i ∈ n. Then ϕ(n, S_{n}) holds where

S_{n} := {∅} ∪ {⟨v, w⟩|v, w ∈ S_{0} ∪ ⋯ ∪ S_{n−1}}

One can prove by induction on ω that for all n ∈ ω , S_{n} is the unique set such that ϕ(n, S_{n}). Using replacement, {S_{0}, S_{1}, …, S_{n}, …} is a set.^{1} We finally define S to be ⋃{S_{0}, S_{1}, …, S_{n}, …} and define nil := ∅ ∈ S and cons(v, w) := ⟨v, w⟩ ∈ S for v, w ∈ S. One can prove the usual induction principle for S using this definition.

Using similar techniques one can define recursive functions on an inductively defined domain such as S.

Direct support for specifying inductive definitions which fall back on the construction above would be useful. For example, one could specify S as

inductive S {
  nil:S.
  cons:S -> S -> S.
}

1This is an important application of the axiom of replacement.

which should define S : set, nil : S and cons : S → S → S and prove the important induction principles (hiding the definitions and proofs from the user).

6.4 Importing Libraries: MetaMath, Isabelle-HOL/ZF, HOL-light, HOL4, Mizar

One of the most important immediate concerns is the building of a large DeTSeT library by importing the libraries of existing systems.

Translating the library of MetaMath [22] should be relatively easy since MetaMath is fully formal and is based on ZFC. Note that MetaMath includes a construction of the real numbers. One should also be able to translate the Isabelle-ZF library in a fairly direct manner.

Mizar [2] has a very large library, but does not use a formal notion of a proof object. The Mizar checker reads text files (Mizar articles) and accepts or rejects these files based on criteria native to the code of Mizar. One could imagine writing an interpreter for Mizar articles which generates corresponding DeTSeT abbreviations. Mizar is based on an extension of ZFC (Tarski-Grothendieck set theory, which assumes every set is a member of a universe modelling ZFC). This extension will likely only prevent small parts of the Mizar library from being directly translated into DeTSeT.

Finally, using the encoding of simply typed λ-calculus in DeTSeT, a translation from Isabelle-HOL and the various members of the HOL family (HOL-light and HOL4) should be possible. There has already been work building proof terms for these libraries which allows the libraries of one system to be imported into the others (see for example [25, 21]).

6.5 Modules

We have described here how to encode mathematical information in a single, large signature of abbreviations. One would like to have a module system which allows several people to independently develop parts of the overall signature without concern about interference from other people developing a different part of the signature.

6.6 Encoding Texts

The library should be further extended by encoding mathematics from textbooks. Of particular interest are portions of Number Theory [14], Real Analysis [11, 4], Algebra [17], Topology [24], and Category Theory [19].

6.7 Natural Input and Output

Much work could be done with respect to input and output of DeTSeT terms and types. As an example, one could consider the input specification language PAM which is used in the system Scunak [8, 7]. Scunak was also able to interpret a LaTeX proof from a textbook as a specification language [9]. Optimally, one would like to be able to scan a mathematical text and obtain a corresponding signature of abbreviations (concepts and proofs). Certainly there must be interesting intermediate stages which could be studied at the moment. One possibility would be to allow proofs to be specified in scripts or articles similar to those used by Mizar [2].

In terms of output, the hope is that one could indicate which parts of a signature one wishes to output and a system could use this to write an article or even a book. The output representation could be either a typesetting language like LaTeX, a markup language like OmDoc [18] which could be used by ActiveMath [23], or a document language like PLATO [36, 20] which could be used to mediate between systems and editors.

6.8 Unification and Matching

One can define an erasure from the dependent types of DeTSeT to simple types. Using this erasure and by Currying away the product types corresponding to class types, one can easily adapt Huet’s algorithm for higher-order pre-unification [16] to DeTSeT. However, it is probably worthwhile to develop algorithms for unification and matching directly for DeTSeT.

6.9 Proof Search

We need methods for finding proofs or filling gaps in proofs. This boils down to the following problem: Given a valid signature Σ and a valid context Γ and a type such that Γ ⊢_{Σ} A : T ype^{i} (for i ∈ {0, 1, 2}), find a term M such that Γ ⊢_{Σ} M ∼ M ↑ A.

A special case would involve creating an efficient algorithm for answering the question of whether there exists a “one-step” M such that Γ ⊢_{Σ} M ∼ M ↑ A. One would need to be precise about what “one-step” means. One easy possibility can be seen by considering imitations and projections from Huet’s pre-unification algorithm [16]. Each imitation or projection partially instantiating a variable of a proof type can be considered as essentially “one-step” in partially filling a proof. A “one-step” completion of a proof (in a context Γ) could be an imitation or a projection where any newly introduced existential variables can be filled using variables from the context Γ. More than likely, however, one would also like to consider certain equality steps as “one-step” even if these do not correspond simply to an imitation or projection.

The idea of what “one-step” means is related to the issue of granularity (as studied in [31]) which is being studied in the tutoring context as part of the DiaLog project [5, 6]. This also relates to checking textbook proofs [9]. A step filling a gap in a proof would be at the appropriate level of granularity for a given student (or reader) if the type corresponding to the gap could be filled in “one-step” where “one-step” is defined relative to the student (reader) model. The head of an imitation step could in principle be any logical constant or abbreviation from Σ, but could also be restricted to a subset of constants and abbreviations. Thus, such a student (reader) model could be defined, at least in part, by giving a subset of abbreviations from Σ that the student (reader) is expected to “know.”

6.10 Compact Representation

In the formulation of DeTSeT given here, terms which correspond to proof terms are βnormal, even though by proof irrelevance it is not necessary to compute β-normal forms to check if two proof terms are equal. (Any two proof terms of the same type are equal, regardless of their normal forms.) We could avoid this by distinguishing in the syntax of terms between proof terms and non-proof terms. This should make some proof terms smaller since we could share subproofs within a term more easily. (At the moment one can only share subproofs by making abbreviations.) One could also form more compact representation by allowing implicit arguments (as in Twelf [27]) or by extending the term structure to include admissible rules (such as replacing equals for equals). In any case, one must prove that the new term representation can be mapped to the original representation in a type preserving way.

6.11 Theory and Semantics

We have given an algorithmic formulation of DeTSeT. In the future, a theoretical formulation should be given. In such a formulation, the λ on terms should probably carry the type so that each term has at most one type. One could hopefully prove that the algorithmic formulation and theoretical formulation are equivalent (in an appropriate sense).

One should be able to define a semantics and prove a soundness and (hopefully) completeness results relating the theoretical formulation of the type theory with the given semantics. Such a semantics could be set theoretic (using ideas from Henkin models), category theoretic (using, for example, either slice categories or fibrations) or perhaps by using pers over models of simple type theory.

6.12 Relationship to first-order ZFC

The motivation for DeTSeT was to give a usable formulation of ZFC. The fact that DeTSeT is at least as expressive and proof-theoretically strong seems obvious from the formulation given here. We conjecture that DeTSeT is actually equivalent to ZFC in the following senses:

• There is a translation taking each M such that · ⊢_{Σ} M ∼ M ↑ prop to a first-order proposition M′.

• For every M such that · ⊢_{Σ} M ∼ M ↑ prop, there is a term P such that · ⊢_{Σ} P ∼ P ↑ pf M iff M′ is provable in ZFC.

• For every proposition N in the language of first-order set theory there is a DeTSeT term M such that · ⊢_{Σ} M ∼ M ↑ prop and such that N ≡ M′ is provable in ZFC.

This would also imply ZFC and DeTSeT have the same consistency strength.

6.13 Choice

The formulation of the axiom of choice is a bit awkward. An easier formulation would involve a choice operator (similar to those commonly used in HOL). However, this would seem to increase the proof strength of the theory beyond ZFC. The problem is that one could use the choice operator within the definition of a set, which does not seem to be possible in ZFC. The status of choice operators in DeTSeT (or extensions of DeTSeT) and the relation to ZFC should be clarified.

7 Conclusion

We have described DeTSeT: a form of ZFC set theory encoded in a dependent type theory with proof irrelevance. DeTSeT has all the power of first-order ZFC and so can be used as a foundation for mathematics. Unlike first-order ZFC, one has the ability to directly construct sets such as

{x ∈ A|ϕ(x)}

as formal terms, even when the property ϕ only makes sense for elements of A. In DeTSeT, sets (and classes) can be treated as types. Also, one can form functional relations using an “object-level” λ-abstraction operator. Thus, DeTSeT combines the advantage of having a single universe of all sets (as in first-order set theory) with the expressive power of logical systems based on typed λ-calculi. We hope to demonstrate the power and naturality of DeTSeT in the future by building a large library of formal mathematics as a DeTSeT signature.

References

[1] Serge Autexier and Armin Fiedler. Textbook proofs meet formal logic - the problem of underspecification and granularity. In Michael Kohlhase, editor, MKM, volume 3863 of Lecture Notes in Computer Science, pages 96–110. Springer, 2005.

[2] Grzegorz Bancerek and Piotr Rudnicki. A Compendium of Continuous Lattices in MIZAR. J. Autom. Reason., 29(3-4):189–224, 2002.

[3] Henk Barendregt. Lambda calculi with types. In S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, pages 117–309. Clarendon Press, 1992.

[4] R.G. Bartle and D.R. Sherbert. Introduction to Real Analysis. John Wiley & Sons, New York, 1982.

[5] Christoph Benzmüller, Armin Fiedler, Malte Gabsdil, Helmut Horacek, Ivana Kruijff-Korbayová, Manfred Pinkal, Jörg Siekmann, Dimitra Tsovaltzi, Bao Quoc Vo, and Magdalena Wolska. A wizard of oz experiment for tutorial dialogues in mathematics. In Proceedings of AI in Education (AIED 2003) Workshop on Advanced Technologies for Mathematics Education, Sydney, Australia, 2003.

[6] Christoph Benzmüller, Helmut Horacek, Henri Lesourd, Ivana Kruijff-Korbayova, Marvin Schiller, and Magdalena Wolska. A corpus of tutorial dialogs on theorem proving; the influence of the presentation of the study-material. In Proceedings of International Conference on Language Resources and Evaluation (LREC 2006), Genova, Italy, 2006. ELDA. To appear.

[7] Chad E. Brown. Combining Type Theory and Untyped Set Theory. In Furbach and Shankar [13], pages 205–219.

[8] Chad E. Brown. Encoding functional relations in Scunak. In LFMTP’2006, September 2006.

[9] Chad E. Brown. Verifying and Invalidating Textbook Proofs using Scunak. In Mathematical Knowledge Management, MKM 2006, pages 110–123, Wokingham, England, 2006.

[10] N .G. de Bruijn. A survey of the project AUTOMATH. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 579–606. Academic Press, 1980.

[11] J. Dieudonne. Foundations of Modern Analysis, volume 1. Academic Press, New York, 1960.

[12] Conal M. Elliot. Extensions and Applications of Higher-order Unification. PhD thesis, Carnegie Mellon University, 1990.

[13] Ulrich Furbach and Natarajan Shankar, editors. Automated Reasoning, Third International Joint Conference, IJCAR 2006, volume 4130 of Lecture Notes in Artificial Intelligence, Seattle, Washington, 2006. Springer-Verlag.

[14] Godfrey H. Hardy and E. M. Wright. An introduction to the theory of numbers. Oxford University Press, 5th edition, 1979.

[15] John Harrison. HOL light: A tutorial introduction. In Mandayam Srivas and Albert Camilleri, editors, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD’96), volume 1166 of Lecture Notes in Computer Science, pages 265–269. Springer-Verlag, 1996.

[16] Gérard P. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.

[17] Thomas W. Hungerford. Algebra. Springer-Verlag New York, Inc., 1974.

[18] Michael Kohlhase. Omdoc: Towards an internet standard for the administration, distribution, and teaching of mathematical knowledge. In John A. Campbell and Eugenio Roanes-Lozano, editors, Artificial Intelligence and Symbolic Computation: International Conference AISC 2000, volume 1930 of Lecture Notes in Artificial Intelligence, pages 32–52. Springer-Verlag, 2001.

[19] Saunders MacLane. Categories for the Working Mathematician. Springer-Verlag, second edition, 1998.

[20] Christoph Benzmüller Marc Wagner, Serge Autexier. Plato: A mediator between texteditors and proof assistance systems. In Christoph Benzmüller Serge Autexier, editor, 7th Workshop on User Interfaces for Theorem Provers (UITP’06), ENTCS. Elsevier, august 2006.

[21] Sean McLaughlin. An Interpretation of Isabelle/HOL in HOL Light. In Furbach and Shankar [13], pages 192–204.

[22] Norman Megill. Metamath Home Page. http://au.metamath.org/index.html.

[23] Erica Melis. ActiveMath Home Page. http://www.activemath.org/.

[24] James R. Munkres. Topology: A First Course. Prentice-Hall, 1975.

[25] Steven Obua and Sebastian Skalberg. Importing HOL into Isabelle/HOL. In Furbach and Shankar [13], pages 298–302.

[26] Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer Verlag, 1994.

[27] Frank Pfenning and Carsten Schürmann. System Description: Twelf–A Meta-Logical Framework for Deductive Systems. In Harald Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, pages 202–206, Trento, Italy, 1999. Springer-Verlag.

[28] The QED manifesto. In Alan Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, volume 814 of Lecture Notes in Artificial Intelligence, pages 238–251, Nancy, France, 1994. Springer-Verlag.

[29] Jason Reed. Proof irrelevance and strict definitions in a logical framework. Technical Report 02-153, School of Computer Science, Carnegie Mellon University, 2002.

[30] Herman Rubin and Jean E. Rubin. Equivalents of the Axiom of Choice, II. North-Holland, 1985.

[31] Marvin Schiller. Mechanizing Proof Step Evaluation for Mathematics Tutoring - the Case of Granularity. Master’s thesis, Universität des Saarlandes, 2005.

[32] Jörg Siekmann, Christoph Benzmüller, Vladimir Brezhnev, Lassaad Cheikhrouhou, Armin Fiedler, Andreas Franke, Helmut Horacek, Michael Kohlhase, Andreas Meier, Erica Melis, Markus Moschner, Immanuel Normann, Martin Pollet, Volker Sorge, Carsten Ullrich, Claus-Peter Wirth, and Jürgen Zimmer. Proof development with Ωmega. In Andrei Voronkov, editor, Proceedings of the 18th International Conference on Automated Deduction, volume 2392 of Lecture Notes in Artificial Intelligence, pages 144–149, Copenhagen, Denmark, 2002. Springer-Verlag.

[33] Jörg Siekmann, Christoph Benzmüller, Armin Fiedler, Andreas Meier, Immanuel Normann, and Martin Pollet. Proof development in OMEGA: The irrationality of square root of 2. In Fairouz Kamareddine, editor, Thirty Five Years of Automating Mathematics, Kluwer Applied Logic series (28), pages 271–314. Kluwer Academic Publishers, 2003. ISBN 1-4020-1656-5.

[34] D.T. van Daalen. Verzamelingstheorie, de axioma’s van Zermelo-Fraenkel. Technical report, Department of Mathematics, Eindhoven University of Technology, September 1970. Internal Report, Dutch.

[35] Jean van Heijenoort. From Frege to Gödel. A Source Book in Mathematical Logic 1879–1931. Harvard University Press, Cambridge, Massachusetts, 1967.

[36] Marc Wagner. Mediation between text-editors and proof assistance systems. Diploma thesis, Saarland University, Saarbrücken, Germany, 2006.

[37] Freek Wiedijk. Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics. Journal of Applied Logic, 2005. to appear.

[38] Ernst Zermelo. Untersuchungen über die Grundlagen der Mengenlehre I. Mathematische Annalen, 65:261–281, 1908. English translation, “Investigations in the foundations of set theory” in [35], pages 199–215.

Index

∈, in, 9 =, eq, 9 ¬, not, 9 ⊃, imp, 9 ≡, equiv, 9 ∧, and, 9 ∨, or, 9 ∀, all, 9 ∃, ex, 9 ∅, emptyset, 11 P, powerset, 11 ⋃, setunion, 11 ω, omega, 11 ∀ ∈, dall, 21 ∃ ∈, dex, 21 ⊥, false, 22 ⊤, true, 23 ⊆, subset, 26 ∪, binunion, 26 ∩, binintersect, 26 ⟨⟨·, ·⟩⟩, kpair, 27 ×, cartprod, 27 ˆ∩, binintersectT, 29 ˆ∪, binunionT, 29 K̂, complementT, 31 P̂, powersetT, 29 R^{−1}, breln1inv, 36 ∘, breln1comp, 37 ˙∪, breln1union, 37

all, 9 allE, 10 allI, 10 and, 9 andEL, 23 andEquiv, 10 andER, 23 andI, 23 ap2, 27

beta2, 27 binintersect, 26 binintersectEL, 26 binintersectER, 26 binintersectI, 26 binintersectT, 29 binintersectT_lem, 29 binintersectTEL, 31 binintersectTELcontra, 31 binintersectTER, 31 binintersectTERcontra, 32 binintersectTI, 31 binintersectTSub1, 32 binintersectTSub2, 32 binunion, 26 binunionE, 26 binunionEcases, 26 binunionIL, 26 binunionIR, 26 binunionLsub, 26 binunionRsub, 26 binunionT, 29 binunionT_lem, 29 binunionTE, 33 binunionTE1, 33 binunionTEcontra, 33 binunionTIL, 32 binunionTILcontra, 32 binunionTIR, 32 binunionTIRcontra, 33 binunionTSub1, 33 binunionTSub2, 33 boxeq, 24 boxequiv, 25 breln, 27 breln1, 36 breln1all1, 36 breln1comp, 37 breln1compE, 37 breln1compI, 37 breln1compprop, 37 breln1compset, 36 breln1inv, 36 breln1invE, 36 breln1invI, 36 breln1invprop, 36 breln1invset, 36 breln1union, 37 breln1unionCommutes, 37 breln1unionE, 37 breln1unionEcases, 37 breln1unionI, 37 breln1unionIL, 37 breln1unionIR, 37 breln1unionprop, 37 bs114d, 30

cartprod, 27 cartprodfst, 27 cartprodfstpairEq, 27 cartprodpair, 27 cartprodpairin, 27 cartprodpairsurjEq, 27 cartprodsnd, 27 cartprodsndpairEq, 27 complementImpComplementIntersect, 32 complementInPowersetComplementIntersect,

32 complementSubsetComplementIntersect, 32 complementT, 31 complementT_lem, 31 complementTcontraSubset, 32 complementTE, 31 complementTE1, 31 complementTI, 31 complementTI1, 31 complementTnotintersectT, 32 contradiction, 22 contrapositive1, 22 contrapositive2, 22 contrapositive3, 22 contrapositive4, 22 contraSubsetComplement, 32 contrasubsetT, 32 contrasubsetT1, 32 contrasubsetT2, 32 contrasubsetT3, 32

dall, 21 dallE, 24 dallI, 24 dand, 21 dandEL, 24 dandER, 24 dandI, 24 demorgan1, 33 demorgan2, 33 demorgan2a1, 33 demorgan2a2, 33 descr, 12 dex, 21 dexE, 24 dexI, 24 dimp, 21 dimpE, 24 dimpI, 24 dnegE, 22 dnegI, 22 doubleComplementE1, 32 doubleComplementEq, 32 doubleComplementI1, 32 doubleComplementSub1, 32 doubleComplementSub2, 32 dpsetconstr, 27 dsetconstr, 13 dsetconstrEL, 13 dsetconstrER, 19, 20 dsetconstrERa, 13 dsetconstrI, 13

emptyset, 11 emptysetAx, 11 emptysetE, 22 eq, 9 eqbreln1, 36 eqCE, 25 eqCE2, 25 eqE, 10 eqE2, 24 eqI, 23 eqinunit, 24 equiv, 9 equivE, 23 equivEimp1, 10 equivEimp2, 10 equivI, 23 equivI1, 10 equivI2, 10 eta2, 28 ex, 9 excludedmiddle, 24 exE, 23 exEquiv, 11 exI, 23 exu, 9 exuEquiv, 11

false, 22 falseE, 22 foundationAx, 12 funcext2, 27 funcSet, 27

if, 28 iffalse, 28 iftrue, 28 iftrueorfalse, 28 imp, 9 impE, 10 impI, 10 in, 9 inComplementUnionImpInComplement1, 33 inComplementUnionImpNotIn1, 33 inIntersectImpInIntersectUnions, 33 inIntersectImpInUnion, 33 inIntersectImpInUnion2, 33 intersectInPowersetIntersectUnions, 33 iskpair, 27

kpair, 27 kpairiskpair, 27

lam2, 27

not, 9 notallE, 25 notandE, 25 notdallE, 25 notdexE, 25 notE, 10 notexE, 25 notI, 22 notimpE, 24 notimpE1, 25 notimpE2, 25 notorE, 25 notorE1, 25 notorE2, 25

omega, 11 omega0Ax, 12 omegaIndAx, 12 omegaSAx, 12 or, 9 orE, 23 orEquiv, 10 orIDemorgan, 23 orIL, 23 orIR, 23

powerset, 11 powersetAx, 11 powersetE, 23 powersetI, 23 powersetI1, 26 powersetsubset, 26 powersetT, 29 powersetT_lem, 29 powersetTE, 31 powersetTE1, 31 powersetTI, 31 powersetTI1, 31 prop2set, 21 prop2setE, 21

reflequiv, 25 replAx, 12

setadjoin, 11 setadjoinAx, 11 setadjoinE, 23 setadjoinIL, 23 setadjoinIR, 23 setext, 23 setextAx, 11 setextsub, 26 setextT, 31 setminus, 27 setminusT, 31 setminusT_lem, 31 setunion, 11 setunionAx, 11 setunionE, 23 setunionI, 23 subbreln1, 36 subset, 26 subset2powerset, 26 subsetE, 26 subsetI1, 26 subsetI2, 26 subsetTI, 31 symeq, 24 symequiv, 25 symtrans1eq, 24 symtrans1equiv, 25 symtrans2eq, 24

transeq, 24 transequiv, 25 trivialImpI, 24 true, 23 trueI, 23

uniqinunit, 24

vacuousImpI, 24

wellorderingAx, 12 woz13rule0, 33 woz13rule1, 33 woz13rule2, 34 woz13rule3, 34 woz13rule4, 34 woz1_1, 34 woz1_2, 34 woz1_3, 35 woz1_4, 35 woz1_5, 35 woz2A, 40 woz2B, 42 woz2Ex, 38 woz2W, 39

xmcases, 10