Foundationless Types: the Very Idea

Recently, I submitted a paper on foundationless types. This suggested that it might be useful for others and fun for me to present the basic idea of foundationless types.

The foundational idea of (simple) type theories, that is, the standard well-founded sort, is the following (recursive) specification of type symbols.

  1. 0 is a type symbol (i is also sometimes used).
  2. If t1, …, tn are type symbols, then (t1, …, tn) is a type symbol.
  3. Nothing else is a type symbol.

Simple types also have a matching requirement, according to which type symbols of a predicate must ‘match’ those of terms it relates: in general, if we have a formula

Rs(xt1, …, xtn),

then the simple type s of the predicate Rs must be (t1, …, tn).

The effect of this specification of type symbols plus the matching requirement is that some terms, like x0, can only occur in subject-position and never in predicate position. For example, y(0)(x0) is well-formed, but x0(y(0)) is an ungrammatical string: it violates the matching requirement. Just like there is a least natural number, there is a lowest type, 0, such that terms of that type cannot be predicates.

However, we can give a different (recursive) specification of type symbols such that there is no least type, just as there is no least integer. One upshot of this is that certain claims about cardinality of various types can be proven. For instance, in type systems that have a lowest type, we can usually only prove that the lowest type is non-empty. In a type system without a lowest type, we can prove that every type has at least 2 elements (we can actually prove more, as I argue in forthcoming work: this is just an illustration).

For some more detail, you might check out:

One caveat: the above authors, like many others, study type theories in which, in a type symbol like (t1, …, tn), it is always the case that t1=…=tn, so that a type symbol is always homogeneous. That requirement is not imposed in type theories that allow for heterogeneous types of terms, that is, type symbols (t1, …, tn) such that ti≠tj for some distinct i and j.

Finally, note that the foundationless types can also be recursively specified. First, note that Z can be recursively specified. Then we have the following (recursive) specification:

  1. For any integer z in Z, z is a type symbol.
  2. If z1, …, zn are type symbols (n≥2), then (z1, …, zn) is a type symbol.
  3. Nothing else is a type symbol.

A recursive specification of the type symbols z in Z can be had as follows:

  1. 0, 0′, and ′0 are type symbols.
  2. If z′ is a (“positive”) type symbol, then so is z′′.
  3. If ′z is a (“negative”) type symbol, then so is ′′z.
  4. If z1, …, zn are type symbols (n≥2), then (z1, …, zn) is a type symbol.
  5. Nothing else is a type symbol.

One can informally represent 0′ by 1, 0′′ by 2, and so on, and ′0 by -1, ′′0 by -2, and so on. The presentation is thus cleaner if we take integers z in Z to stand for type symbols without losing the recursive specification.

There you have it: a brief, er, foundation, for foundationless types!

Professional News: Going to U. Alberta!

In happy news, I will be starting a postdoctoral position with the University of Alberta philosophy department this September 1st! There, I will develop a digital humanities research project in the history of logic and computing. Here is a short description:

This digital humanities project consists of novel computational research in history of philosophy. This project uses computer proof-assistants, which are programs that function like human tutors helping students with a logic problem: they can provide hints, check consistency, and suggest tactics. Using computer proof-assistants, I will model different extant interpretations of Principia Mathematica. These computer-assisted models will allow for mapping Principia under each competing interpretation, facilitating a side-by-side comparison of the text under different
readings. This Killam Fellowship project also serves as a prototype applying computer proof-assistants to other significant works in history of philosophy.

“Killam Fellowship” refers to the position title, Izaak Walton Killam Memorial Postdoctoral Fellowship, which is so-named because it is dedicated to the memory of Izaak and Dorothy Killam.

I am grateful to the Killam Trusts for this award. Having honeymooned in Alberta, my wife and I are excited to return there for our next northern adventure.

Tracing the symbol for disjunction

There was an interesting Twitter thread launched by Richard Zach’s remark:

Here we also get a curious sub-question: when did Russell switch from taking “⊃” as primitive (as he does in 1901—see Collected Papers Vol. 3, Chapter 11, page 381) to taking “∨” and “∼” as primitive (as he does in Principia)?

The short story is that the earliest use of “∨” for disjunction is early 1903 in Russell’s manuscript “Classes” (see the picture below) and the switch to taking “∨” and “∼” as primitive rather than “⊃” occurred around 21 August 1906. The longer story, most of which comes from Gregory Moore’s introductions in The Collected Papers of Bertrand Russell, Volume 3, is retold below.

Russell’s 1901 works are already deeply influenced by Peano, particularly in their choice of symbolism. However, even there, Russell shows some independent choices of notation. For example, in “The Logic of Relations,” Russell has already introduced the use of dot “.” for conjunction. This is in addition to his and Peano’s shared use of the same symbol as a scope marker. But as Dirk Schlimm pointed out to Richard Zach, Peano does not use “.” for conjunction. Still, in 1901 and 1902, Russell is working from (that is, working his way out of) the standpoint of treating certain logical symbols as having a dual use, namely, for symbolizing relations between classes and between propositions.

This dual usage was made possible partly by Russell’s logic of propositions around this time: on that theory, propositions stand in relations of implication, disjunction, conjunction, and so on, just as classes would stand in relations of subset and membership. This conception of propositional logic is very different from the modern one in which symbols like “∧,” “∨,” and “¬” connect well-formed formulas to form a new formula. Rather, on Russell’s view (and probably Peano’s also), such symbols connect propositions as terms to make a formula.

As Gregory Moore notes (ibid., Chapter 15, page 439), in his spring 1902 “On Likeness” (which was not published until Collected Papers Vol. 3), Russell departs further from Peano’s notation. Russell now distinguishes between “⊃” for the relations of propositional implication and relation inclusion and “⊂” for class inclusion. Similarly, he introduces “∼” for propositional negation rather than using “–” for this and for a class’ complement.

Here, however, his usage of “∧” and “∨” is the reverse of our modern usage: Russell introduces the new notation “∧” and “∨” for class intersection and class union, whereas he uses the old notation “∩” for propositional conjunction and relation intersection, and he used “∪” for propositional disjunction and relational union. This use of “∧” and “∨” can be seen in *1·1 below, and this use of “∪” can be seen in *2·1 below.

CPBRVol3OnLikenessPage440

Collected Papers Vol. 3, Chapter 15, page 440: Russell’s 1902 “On Likeness”

As Moore says, this usage gets reversed in Russell’s early 1903 “Classes” (Collected Papers Vol. 4, Chapter 1a), so that “∨” now symbolizes disjunction and “∪” symbolizes class union. This persists from Principles through Principia, and seems to be origin of our modern usage.

CPBRVol4GeneralTheoryOfClassesPage9

Collected Papers Vol. 4, Chapter 1a, page 9: the introduction of “∨” for disjunction in *12·58 of Russell’s 1903 “Classes”

All of this is a post-Peano influence with Russell’s considered modifications. There is a second wave of influence post-Frege’s deeper influence on Russell in early 1903. A deeper chronology is given by Moore in Collected Papers Vol. 3, Introduction, §V (that’s section five and not section or!).

Finally, as Moore again notes (Collected Papers Vol. 5, Introduction, §VII), in 1905 Russell switched to taking “∼” as primitive when he came to the conclusion, for philosophical reasons, that negation could not be defined. In 1906 Russell took “∨” as primitive because “two primitive propositions are made superfluous,” as he says in a 21 August 1906 letter to Louis Couturat (ibid., page xlv).

As a side remark, in the 1902 paper, Russell also introduces “≡” for propositional equivalence (it had previously been used for identity of individuals) rather than using “=” for both propositional equivalence and class identity. Against the backdrop of Russell’s propositional logic on which propositions can be terms of relations, there may be a curious anticipation of propositional equality in modern type theories treating propositions-as-types.

As another side remark, it appears Peano never changed his notation in response to Russell’s innovations. Curiously, a cursory look at Peano’s 1913 review of Principia in the Formulario is largely just Peano showing how the theorems of Principia could be symbolized in his preferred notation. This might be seen as a refusal to “get with the times” of modernized notation that avoids dual uses of symbols. But Peano’s concern was more with the abbreviation and crisp communication of mathematical knowledge.

Frege mockingly criticized Peano’s notation choices as making “the convenience of the typesetter” the “summum bonum” in his 1897 “On Mr. Peano’s Conceptual Notation and My Own.” However, in Peano’s defense, we see now a renewed concern with conveniently crisp presentations of appropriately abbreviated mathematics in modern proof-assistant libraries. In addition, the context in Peano’s works was supposed to clarify which dual use was meant (or else reading it on either use was not illicit and allowed for a briefer presentation of results), much as a modern typing context can clarify syntactic “ambiguities.”

I do not say this to defend dual uses of notation, but only to indicate that Peano’s values and goals, the ones that guided his notation choices, are deeply relevant to us today, just as avoiding syntactic ambiguities was and still is.

 

New with LibriVox: “Philosophical Essays” by Bertrand Russell

In case you want more listening opportunities during this pandemic, look no further than LibriVox, which hosts free public-domain audio books. As of April 2nd, another work that I recorded is out: Bertrand Russell’s 1910 Philosophical Essays, which includes numerous essays on pragmatism, monism, and ethics. The preface is also a treat, if only because it contains this snippet:

The death of William James, which occurred when the printing of this book was already far advanced, makes me wish to express, what in the course of controversial writings does not adequately appear, the profound respect and personal esteem which I felt for him, as did all who knew him, and my deep sense of the public and private loss occasioned by his death. For readers trained in philosophy, no such assurance was required; but for those unaccustomed to the tone of a subject in which agreement is necessarily rarer than esteem, it seemed desirable to record what to others would be a matter of course.

Enjoy this new recording! And if Russell works and my voice are still not wearisome to you, then there are 55 hours of free philosophy audio books for listening at your leisure and pleasure. Enjoy those, too!

Constructive and Destructive Philosophy: Russell’s conception of philosophy and the “analytic”/”synthetic” locution

Eric Schliesser (University of Amsterdam), in an interesting review of books by Dennett and Godfrey Smith, suggests a contrast between synthetic philosophy and analytic philosophy (pages 1-2):

By ‘synthetic philosophy’ I mean a style of philosophy that brings together insights, knowledge, and arguments from the special sciences with the aim to offer a coherent account of complex systems and connect these to a wider culture or other philosophical projects (or both). […] So, one useful way to conceive of synthetic philosophy is to discern in it the construction of a scientific image that may influence the development of the special sciences, philosophy, public policy, or the manifest image.

It is notoriously difficult to define analytic philosophy. But I intend here to evoke the contrast with the kind of decomposition favored by Russell and those influenced by him. […] The key move is to represent a topic in terms of an argument with plausible premises and an unpalatable conclusion, which, in turn, can be re-conceived as a (say) trilemma. The point of the enterprise—the condition of possibility of progress—then is to find ways to give up one of the plausible seeming premises or to find ways to make the conclusion seem less unpalatable.

I will not define Russell’s conception of philosophy here, as that would take too much time and it went through substantial changes over his 97 years of life. (His death-day is 2nd February, by the by.) The narrow point of this post is that Russell’s conception of philosophy is not “analytic” in this sense. The upshot is a suggestion of a different way of talking about two sorts of philosophical activity.

It is true that Russell jokingly suggests in The Philosophy of Logical Atomism, “…the point of philosophy is to start with something so simple as to not seem worth stating, and to end with something so paradoxical that no one will believe it.” But Russell clearly makes space for the synthetic activity described above, and holds it out as a crucial part of philosophical activity. As Russell says in Problems (and elsewhere):

Philosophy, like all other studies, aims primarily at knowledge. The knowledge it aims at is the kind of knowledge which gives unity and system to the body of the sciences, and the kind which results from a critical examination of the grounds of our convictions, prejudices, and beliefs.

This sounds a lot like synthetic philosophy as Schliesser characterizes it. So, Russell is not an analytic philosopher as Schliesser characterizes it.

Nonetheless, Russell is at times an unapologetic believer in abstract objects like universals. So, he is clearly not a naturalist philosopher in the modern ontological sense. But thus he is not a synthetic philosopher as Schliesser characterizes it. This is because, on Schliesser’s view, synthetic philosophy “shares kinship with what was once known as ‘natural philosophy’ or (later) ‘philosophy of nature'” (page 4).

But Russell was of course aggressive leery (rightly, I think) of “speculative”, “systematic”, and “natural” philosophical approaches in the spirit of Bergson (as Russell understood Bergson). This makes me reluctant to unduly wed synthetic philosophy in Schliesser’s sense to systematic or naturalistic approaches precisely because this way of conceptualizing philosophical methodologies (carving up the space) leaves folks like Russell in neither class of philosophers.

Characteristic of problematic philosophical activity, in Russell’s view, is the attempt to establish necessary metaphysical truths about the entire universe. Russell is deeply suspicious of any and all attempts to arrive at a priori justifiable metaphysical principles, arguing, “It would seem that knowledge concerning the universe as a whole is not to be obtained by metaphysics…” Russell concludes:

Thus we are left to the piecemeal investigation of the world, and are unable to know the characters of those parts of the universe that are remote from our experience. This result, disappointing as it is to those whose hopes have been raised by the systems of philosophers, is in harmony with the inductive and scientific temper of our age, and is borne out by the whole examination of human knowledge which has occupied our previous chapters.

The relation between philosophy of nature in this allegedly problematic sense and synthetic philosophy in Schliesser’s sense is an interesting question. But I would like to suggest that a more apt word choice than “analytic”/”synthetic” for describing the different kinds of activities Schliesser has in mind: on the one hand, we have destructive philosophy, which aims chiefly at refutation of some claim or claims; on the other we have constructive philosophy, which aims chiefly at, as Schliesser nicely puts it (page 4), “the generation (and stabilization) of the scientific image out of disparate, esoteric special sciences…being a vehicle for the dynamic interaction and co-evolution of the manifest and scientific images.”

There is room for both sorts of activity making useful contributions (this post is an example): they can be mutually supporting philosophical activities. So, this way of talking about these two sorts of activities (rather than about “analytic”/”synthetic” philosophical schools) allows more clearly for the manifest truth that philosophers often engage in both activities throughout their career—as Russell certainly did.