Is there a (foundational) type theory with the features I'm looking for?
I have the impression that Russellian unramified typed set theory (TST) might be the (foundational) type theory you are looking for. This type theory is used in some papers by Randall Holmes, Adrian Richard David Mathias and Thomas Forster. Note that this type theory is not predicative, because it only conforms to the position of Frank P. Ramsey and Rudolf Carnap, who accepted the ban on explicit circularity, but argued against the ban on circular quantification. If I understood it correctly, Church's 1940 simple type theory based on lambda calculus is a more elegant formulation of this type theory (or at least equiconsistent). I don't know the place where TST was first described, but Mendelson's (1997, 289–293) ST type theory seems to be essentially TST + infinity.
Let me explain how TST is "un-ramified". SEP describes ramified types like this:
The types can be defined as
- $i$ is the type of individuals
- $()$ is the type of propositions
- if $A_1,\ldots,A_n$ are types then $(A_1,\ldots,A_n)$ is the type of $n$-ary relations over objects of respective types $A_1,\ldots,A_n$
For instance, the type of binary relations over individuals is $(i, i)$, the type of binary connectives is $((),())$, the type of quantifiers over individuals is $((i))$.
The unramified type theory on the other hand doesn't use any tuples at all. TST has a linear hierarchy of types: type $0$ consists of individuals otherwise undescribed. For each (meta-)natural number $n$, type $n+1$ objects are sets of type $n$ objects; sets of type $n$ have members of type $n-1$.
As noticed however first by Chwistek, and later by Ramsey, in the presence of the axiom of reducibility, there is actually no point in introducing the ramified hierarchy at all! It is much simpler to accept impredicative definitions from the start. The simple “extensional” hierarchy of individuals, classes, classes of classes, … is then enough. We get in this way the simpler systems formalised in Gödel 1931 or Church 1940 that were presented above.
The axiom schema of comprehension of TST (comprehension axioms are used by Henkin semantics for higher order logic) is "more impredicative" than its simple statement suggests:
If $\phi(x^n)$ is a formula, then the set $\{x^n \mid \phi(x^n)\}^{n+1}$ exists.
First note that $\phi(x^n)$ is allowed to contain free variables other than $x^n$, with no restriction on the type of these variables. If $\phi(x^n)$ would only contain quantification over variables of type $<n$, then we would still consider this as predicative. Quantification over variables of type $\leq n$ would already be impredicative, but in this case, there are no restriction on the type of the variables for the quantification at all. This is how the reference to the position of Frank P. Ramsey and Rudolf Carnap translates into actual axiom schemes.
The Calculus of Constructions (CoC) which forms the foundation for the proof assistant Coq pretty much directly satisfies the requested properties:
- Native support for recursively-defined sets (bonus points if there's support for definitions by transfinite recursion).
Yes, recursively-defined sets are a primitive of CoC. For example, $\mathbb{N}$ is defined in Coq as:
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
And you can also recursively define sets based on indexed constructions with arbitrarily-sized index sets. For example, for trees with countably infinite branching at each node:
Inductive omega_tree : Set :=
| leaf_node : omega_tree
| internal_node : (nat -> omega_tree) -> omega_tree.
Or we can even have this start of a model of ZFC within the system:
Inductive V : Type :=
| enumerated_set : forall (A:Type), (A -> V) -> V.
Inductive V_in : V -> V -> Prop :=
| V_in_intro : forall (A:Type) (x:A->V) (a:A), V_in (x a) (enumerated_set A x).
(But then, V_in needs to be modified somewhat in order to make the extensionality axiom hold. Still, this should give an idea of the power of the construction.)
Also, if we use the definition of ordinals below, then definitions of functions by transfinite recursion will work.
- Sets "float free" in the universe.
Yes, for a generic type A, elements a : A are treated as atomic "ur-elements" of the type, not as sets themselves.
- A big sledgehammer (like the axiom schema of separation) with which to define arbitrary subsets.
Well, in Coq, subsets of A are usually treated as identical to functions A -> Prop taking an element of A to the proposition that the element is in the subset. So, for example, you could define
Definition S : Ensemble nat := fun n:nat => (n >= 3 /\ n <= 7).
There are also sigma-types like { n:nat | n >= 3 /\ n <= 7 }.
By the way, sigma-types are just a special case of the general inductive construction:
Inductive sig (A:Type) (P:A->Prop) : Type :=
| exist : forall x:A, P x -> sig A P.
More generally, Coq allows you to define data types with invariants included using convenient notation. For example, in my development of basic topology, I have:
Record neighborhood_net_index `{TopologicalSpace X} (x0 : X) : Type := {
nni_nhd : Ensemble X;
nni_pt : X;
nni_nhd_is_nhd : neighborhood x0 nni_nhd;
nni_pt_in_nhd : In _ nni_nhd nni_pt
}.
This ends up producing much more readable proofs than the sigma-type { nhd : Ensemble X & pt : X | neighborhood x0 nhd /\ In _ nhd pt }.
- Not too much dependency on the lambda calculus; I don't want to be forced to code the natural numbers as Church numerals, for example. (To be honest, I find the lambda calculus very, very hard to use for all but the most trivial of problems).
Yes, functions can be recursively defined using natural notation, rather than the somewhat artificial constructions of lambda calculus. For example:
Fixpoint plus (n m : nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)
end.
- Uncountable sets, non-computable functions
Yes, Ensemble nat and nat -> nat are provably uncountable within the system. Also, we can for example define a proposition of which Turing machines terminate on which inputs. (The system has a distinction between Prop as the type of propositions, and bool as the set of true or false values.)
- Direct sums, Cartesian products, exponential objects
Inductive sum (A B:Type) : Type :=
| inl : A -> sum A B
| inr : B -> sum A B.
Inductive prod (A B : Type) : Type :=
| pair : A -> B -> prod A B.
As for exponential objects A -> B, they are built in to the system. In fact, Coq is a dependently typed language, so for any function P : A -> Type we can form forall x:A, P x which represents the indexed product $\prod_{x \in A} P_x$. Elements of this product are still thought of as functions which take in x : A and return an element of P x.
- As much of the power of ZFC as possible, especially a rich theory of ordinal numbers and cardinal numbers
Yes, you can for example build a model of ordinal numbers as:
Inductive ordinal : Type :=
| ordS : ordinal -> ordinal
| ord_sup : forall A:Type, (A -> ordinal) -> ordinal.
You then need to define equivalence between different representations of ordinals. From there, you can form the quotient type (assuming you add some classical axioms, see below), or you can work with the setoid on ordinal using this equivalence.
And you can also define cardinals for example as a setoid on Type with equivalence being existence of a bijection. If you add the axiom of choice to the system, you can prove a type-theoretic version of Zorn's lemma, and also prove the existence of a well-order on any type.
- A logic that is classical, or at least the ability to make it classical by adjoining a few more axioms and/or rules.
The default logic of Coq is intuitionistic. However, you can add several axioms to make it more classical - for example:
Axiom classic : forall P:Prop, P \/ ~P.
Axiom functional_extensionality : forall (A B:Type) (f g:A -> B),
(forall x:A, f x = g x) -> f = g.
Axiom prop_extensionality : forall P Q:Prop, (P <-> Q) -> P = Q.
Axiom Extensionality_Ensembles : forall (A:Type) (S T : Ensemble A),
Included _ S T -> Included _ T S -> S = T.
Axiom proof_irrelevance : forall (P : Prop) (proof1 proof2 : P),
proof1 = proof2.
Axiom choice : forall (A B:Type) (R : A -> B -> Prop),
(forall x:A, exists y:B, R x y) ->
exists f : A -> B, forall x:A, R x (f x).
Axiom definite_description : forall (A:Type) (P:A->Prop),
(exists! x:A, P x) -> { x:A | P x }.
(The last is needed in cases where a classical construction defines an object as "the unique $x \in X$ such that ..." and the proof of the existence of an object satisfying the property is not constructive.)
These axioms are consistent with the theory of CoC.
The request to have innate support for recursively defined sets seems closely related to the "Appendix to Part Zero" from Conway's "On Numbers and Games". I have the impression that it slightly misses the point where the consistency strength of a foundational system comes in, but I will have to think about it again later. The openly admitted ontological commitments seem to be identical to predicativism, but some statements and principles also hint at a "Platonic realist" conception. The ontological commitments related to the position of Frank P. Ramsey and Rudolf Carnap were easier for me to grasp.
"If $P$ is some proposition that holds for $x$ whenever it holds for all $x^L$ and $x^R$, then $P$ holds universally."
We have already remarked that this was what we intended to be understood from the last sentence of out construction: "All numbers are constructed in this way."
This is patently a "last word" construction, similar to the standard second order semantics. As more ways to construct propositions $P$ become available during further construction, this axiom will always keep the last word. And no word has been said about whether impredicative propositions will be allowed, but I guess that the intention is to not allow them.
The curiously complicated nature of these constructions tells us more about the nature of formalizations within ZF than about our system of numbers, [...]
It seems to us, however, that mathematics has now reached the stage where formalization within some particular axiomatic set theory is irrelevant, even for foundational studies. [...] This appendix is in fact a cry for a Mathematicians' Liberation Movement!
Among the permissible kinds of construction we should have:
- Objects may be created from earlier objects in any reasonably constructive fashion.
- Equality among the created objects can be any desired equivalence relation.
In particular, set theory would be such a theory, sets being constructed from earlier ones by processes corresponding to the usual axioms, and the equality relation being that of having the same members. But we could also, for instance, freely create a new object $(x,y)$ and call it the ordered pair of $x$ and $y$. [...]
Is the axiom scheme of replacement (or the equivalent axiom scheme of class comprehension) from ZF really of this nature? What about the axiom of choice from ZFC?
For those who doubt the possibility of such a programme, it might be worthwhile to note that certainly principles (i) and (ii) of our Mathematicians' Lib movement can be expressed directly in terms of the predicate calculus without any mentioning of sets (for instance), and it can be shown that any theory satisfying the corresponding restrictions can be formalized in ZF together with sufficiently many axioms of infinity.
Finally, we note that we have adopted the modern habit of identifying ZF (which properly has only sets) with the equiconsistent theory NBG (which has proper Classes as well) in this appendix and elsewhere.
What is meant by "sufficiently many axioms of infinity" here? Is he referring to large cardinal axioms? If not, why does he need more axioms of infinity than the ones already present in ZF (infinity and powerset)?