Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

November 9, 2012

Freedom From Logic

Posted by Mike Shulman

One of the most interesting things being discussed at IAS this year is the idea of developing a language for informal homotopy type theory. What does that mean? Well, traditional mathematics is usually written in natural language (with some additional helpful symbols), but in a way that all mathematicians can nevertheless recognize as “sufficiently rigorous” — and it’s generally understood that anyone willing to undertake the tedium could fully formalize it in a formal system like material set theory, structural set theory, or extensional type theory. By analogy, therefore, we would like an “informal” way to write mathematics in natural language which we can all agree could be fully formalized in homotopy type theory, by anyone willing to undertake the tedium.

Peter Aczel was the initial advocate of such a thing here, and I think it’s a great idea. Given that computer proof assistants are not really yet sufficiently automated to make formalization of nontrivial arguments palatable to the average mathematician — a situation which I think it will probably take a few decades to overcome, at least — in order for homotopy type theory to make real headway as a foundation for mathematics in the near future, we need a way to do it without computers.

It’s worth noting that the relationship between formal and informal being envisioned here is, to a large extent, backwards from the historical situation for traditional foundations. Traditionally, mathematicians developed our conventions and standards of rigor in natural language by a long, slow process of centuries, and only in the last hundred years or so did people start to write down formal systems in which such reasoning could be codified. By contrast, now we are starting with a formal system — homotopy type theory — and trying to design conventions and standards for a corresponding informal language. The situation isn’t quite as clear-cut as that — in particular, in the 20th century formal systems did also conversely influence the conventions of informal mathematics — but nevertheless I think that this proposal is, by and large, something that’s never been done before.

Another point that I think is very important is that informal HoTT is intended to be read by people who are already familiar with the conventions. Obviously, we don’t want to depart unnecessarily from the language of classical mathematics, but writing informal HoTT is not intended to be the same as writing about HoTT for newcomers to the field, just as we don’t write mathematics in research papers in the same way that we write undergraduate textbooks.

There are a lot of interesting aspects to informal HoTT, and I’ll probably be blogging about them more in the future. However, one of the trickiest and most contentious aspects (unsurprisingly) is the treatment of logic and propositions. Recall that one of the insights of type theory is the propositions as types paradigm, according to which

  • Propositions (in the logician’s sense of “assertions which we might attempt to prove”) are identified with particular types, and
  • Proofs of a proposition are identified with terms belonging to such a type.

This has all sorts of nice consequences. The common type forming operations, like cartesian product, disjoint union, function types, dependent products, etc. correspond precisely to the usual logical connectives and quantifiers, like “and”, “or”, “implies”, and “for all”. Proofs are endowed with constructive/computational content, which means that sometimes you can automatically extract an algorithm from a proof. It makes for a pleasing parsimony of foundational notions: type theory is all we need, rather than a set of axioms (like set theory) formulated within an external “logic”. And so on.

The slippery question is, which types are the propositions? I wrote about a couple of potential choices back in January: we could allow all types to be propositions, or we could allow only the (1)(-1)-truncated types (sometimes called “h-propositions”). This matters because when writing informal type theory, we want to be able to use traditional mathematical phrases like “there exists an x:Ax:A such that P(x)P(x)”, but it seems that the formal meaning of such a phrase must depend on which types we allow to be propositions. If all types can be propositions, then “there exists an x:Ax:A such that P(x)P(x)” can indicate the type x:AP(x)\sum_{x:A} P(x), but if only (-1)-types can be propositions, then the same phrase (assuming that it is to be a proposition) must denote instead the (-1)-truncation of x:AP(x)\sum_{x:A} P(x) (the bracket type).

In January, I argued strongly for the latter choice (propositions must be (-1)-types). But over the past few weeks, conversations with Bob Harper, Dan Licata, Peter Aczel, and others have brought me around to a different point of view (which nevertheless may not be the same as their point of view…). Consider the following points:

  • When doing verified programming, frequently one does want to “prove a theorem” about a program one has written, and then extract computational content from that proof. This is not possible if when one is “proving a theorem” one must always be truncating types. (I don’t personally understand the details of this, so I’m taking their word for it. But even if this were not true, or if you’re a pure mathematician who doesn’t care beans about the needs of computer programmers, I still think the other arguments I’m about to present carry weight.)

  • Many of the arguments for h-propositions, when regarded at a formal level, imply only that (-1)-truncated types are important. A priori, they don’t force us to regard such types as the “propositions”; they only force us to talk about them, in some way.

  • As I mentioned in my January post, arguably one of the insights of homotopy type theory is that there’s nothing special about (-1)-truncation. (-1)-truncated types are only the first rung on an infinite ladder. At the time, I used this to argue that they shouldn’t be treated specially the way that they are in set theory, where “logic” is an external structure — but insisting that only they should be regarded as the “propositions” is also a form of special treatment.

  • Even more generally, truncation levels themselves are not even necessarily that special: they are just particular “higher (idempotent, monadic) modalities”, i.e. stable factorization systems. (I wrote up a brief summary of such modalities from a type-theoretic perspective here.) Arguably, any such modality gives us an equally good “logic”. This includes other useful examples like codiscreteness in a cohesive topos, the double-negation modality for classical logic, and the “local” modalities of subtoposes. It seems likely to me that it would even allow us to handle the logic of strong-subobjects in an (,1)(\infty,1)-quasitopos, which in January I thought that only logic-enriched-type-theory could handle.

  • Finally, in everyday mathematics, not all the “propositions” we prove are naturally (-1)-truncated! Once my eyes were opened to this, I started to see it everywhere. Most classical mathematicians are deeply programmed to think of proofs as containing no content, in the sense that once you prove a theorem it doesn’t matter what the proof was (a type theorist calls this “proof irrelevance”). But actually, in doing ordinary mathematics it happens to me all the time that I end up writing “by the proof of Lemma 9.3”, because what matters is not just the statement of Lemma 9.3 but the particular proof of it that I gave.

    This is especially common for statements such as “ABA\cong B”. In practice, (1) to prove that two things are isomorphic, almost without exception we construct a particular isomorphism, and (2) very often in order to use the fact that two things are isomorphic, we need a particular isomorphism, and it often matters what that isomorphism is. In other words, when we “prove” a statement of the form ABA\cong B, almost always we are not constructing a term in some (-1)-type (which would have to be the (-1)-truncation of the type of isomorphisms from AA to BB), but rather constructing a term in the type of isomorphisms from AA to BB. Therefore, why not allow “ABA\cong B” to denote the type of isomorphisms?

This last point reminds me of Bishop’s comment that the axiom of choice is most often used to extract elements from equivalence classes into which they should never have been put in the first place. If what we have actually constructed is a particular term belonging to some informative type (one that isn’t (-1)-truncated), why force ourselves to say less by asserting only that the (-1)-truncation of that type is inhabited, simply because we want to “prove a theorem” and we dogmatically require that “theorems” must be (-1)-types?

Just as intuitionistic logic is more expressive than classical logic because it doesn’t force us to assume the law of excluded middle (but allows us to assume it as an additional hypothesis like any other hypothesis), type theory is allowing us to see a further distinction which was invisible to the classical mind: we aren’t forced to (-1)-truncate all theorems (but we are allowed to, if we so desire, by simply applying the truncation operator).

(There is another point that seems important too: namely, in homotopy type theory, even the “irrelevant” types — that is, (-1)-types — can be, in a sense, relevant. For instance, the type isEquiv(f)isEquiv(f) which asserts that ff is an equivalence is a (-1)-type, so that any two inhabitants of it are equivalent. However, in proving isEquiv(f)isEquiv(f) we must supply, among other things, an inverse to ff, while from an inhabitant of isEquiv(f)isEquiv(f) we may extract an inverse of ff, and unless we did something stupid, the inverse we get out is the one we put in — not just equivalent to it, but literally definitionally the same as it. Sometimes this can be really important, especially when implementing things in a proof assistant, because definitional equality controls type-checking — not to speak of computational behavior and efficiency. The other day we had a very interesting discussion about which of the many types equivalent to isEquivisEquiv should be used in the HoTT Coq library as “the” definition of equivalence; we eventually settled on “adjoint equivalences” because they specify the most additional data in an easily-extractable form.)

With all the above in mind, I think what I would really like to do is to make a clean break by expunging the notion of “proposition” from the language. In other words, there are only types. Some types are (-1)-truncated. Some types are nn-truncated. Some types belong to other modalities. Sometimes we can construct a term in a given type as it stands. Other times we can only construct a term in some truncation of it, or in its reflection into some other modality. (For instance, this is quite a common occurrence for the “classical logic” modality.)

Realistically, of course, the word “proposition” is not going to go away. For one thing, it’s a very convenient word to use to describe (-1)-types. But I still believe this way of thinking—freeing ourselves from our percieved need to distinguish between what I called the “two activities” of mathematics, namely “constructing” and “proving”—is the way of the future.

We do still have to choose how to interpret informal statements like “there exists an x:Ax:A such that P(x)P(x)” as types. I think the point that “(-1)-types are not special” argues strongly that (1) such a phrase should, by itself, be interpreted as x:AP(x)\sum_{x:A} P(x), but also that (2) there must be an easy and concise way to indicate when we want it to be interpreted in some other modality. And the obvious idea for (2) is to use adverbs, which are a part of speech frequently used to denote modalities (consider the most traditional modalities such as “necessarily” and “possibly”). For instance, we can say “there codiscretely exists …” or “there classically exists …” to indicate application of the \sharp modality or the double-negation modality.

We would, of course, have to choose a particular adverb to indicate the (-1)-truncation modality. One possibility would be “irrelevantly” (referring to “proof irrelevance”), but (aside from being five syllables) that has the quite undesirable implication of “not related to the rest of what I’m saying”. The best adverb I’ve thought of so far is “purely”, as used in classical statements like “this is a pure existence proof, not a construction”. Thus, for instance, we would have the different forms of the axiom of choice:

  1. “If for every x:Ax:A, there exists a y:By:B such that P(x,y)P(x,y), then there exists a function f:ABf:A\to B such that for all x:Ax:A we have P(x,f(x))P(x,f(x))” — this one is provable.

  2. “If for every x:Ax:A, there purely exists a y:By:B such that P(x,y)P(x,y), then there exists a function f:ABf:A\to B such that for all x:Ax:A we have P(x,f(x))P(x,f(x))” — this one is a strong axiom.

But I’m open to other suggestions. It would also be nice to have an adverb that could be parametrized by a number to denote nn-truncation. I guess we could say “nn-purely” for this, though with the unfortunate convention that the unadorned “purely” would imply n=1n=-1. On the other hand, thinking semantically, one might also consider “locally”, since (-1)-truncated truth descends along effective epimorphisms. However, this intuition is questionable from a foundational point of view, and probably the adverb “locally” should be reserved for lex modalities, i.e. subtoposes.

Posted at November 9, 2012 3:19 PM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2573

70 Comments & 1 Trackback

Re: Freedom From Logic

How about “non-constructively”?

Posted by: Patrick Schultz on November 10, 2012 4:34 AM | Permalink | Reply to this

Re: Freedom From Logic

“Non-constructively” could suggest the double-negation operator. How about “there logically exists”?

Posted by: Colin McQuillan on November 10, 2012 12:06 PM | Permalink | Reply to this

Re: Freedom From Logic

Yes, I think Colin is right: ‘non-constuctively’ is ambiguous (and five syllables). On the other hand, arguably everything we’re doing is logic. The restriction of the word ‘logic’ to refer to (-1)-types is another part of the position I’ve argued strongly for in the past that now I am changing my mind about: for one thing, the propositions-as-types people don’t want to give up the word ‘logic’ for their versions either.

Posted by: Mike Shulman on November 10, 2012 2:50 PM | Permalink | Reply to this

Re: Freedom From Logic

What can I say? I like!

Other (long) adverbs for existence you might like to consider: mysteriously, expressing our wonder above our ignorance; obscurely, expressing the hiddenness of any terms in the type one is considering; merely, similar to your “purely”, though with slightly different connotations as to the dirrection of perfection; resonantly, in case one ever feels like specializing to quantum logics; …

Posted by: Jesse C. McKeown on November 10, 2012 4:57 AM | Permalink | Reply to this

Re: Freedom From Logic

I like “merely”. In the same vein we could have “barely” or “plainly”.

Posted by: Guillaume Brunerie on November 10, 2012 5:59 PM | Permalink | Reply to this

Re: Freedom From Logic

I’ve experimented a little in notes with using “there is a such-and-such” for a specified choice, and “there exists a/some such-and-such” for the bracketed/truncated/mere version. It takes a bit of getting used to, since in traditional maths we’re so used to reading “there is…” and “there exists…” as synonyms, but it ends up reading reasonably nicely, I think.

Posted by: Peter LeFanu Lumsdaine on November 10, 2012 7:35 PM | Permalink | Reply to this

Re: Freedom From Logic

I was just about to suggest the same thing.

For me, however, a big part of this comes from the fact that I adamantly disagree with the conflation of Sigma with the existential quantifier. The strong Sigma of ITT is, fundamentally, a notion of tupling/pairing—which therefore enables one to project out both components of that pair. The weak Sigma (aka refinement types) is similar, but disallows projecting out the second component of the pair (in any computationally relevant way). And the existential quantifier, both in classical mathematics without choice and in languages such as System F, disallows projection of the first component (in any way that won’t be erased or recaptured by another existential quantifier). This restriction of not allowing existentially quantified variables to escape is requisite for reasoning by parametricity, which is crucial in programming and the related portion of proof theory. When one can project out the first component of a dependent pair, we lose most of the properties we desire from existential quantification. That Martin-Loef suggested strong Sigma corresponds to existential quantification is, IMO, a gross error which should not be perpetuated.

Thus, I think “there is” is a much better colloquialism for strong Sigma. Thus, following the idea of using adverbs to express modalities we should say: “there is locally”, “there is codiscretely”,… and for (-1)-truncation: “there is extantly”, or more casually “there exists”.

Posted by: wren ng thornton on November 10, 2012 11:58 PM | Permalink | Reply to this

Re: Freedom From Logic

Actually, I don’t even see the point about existential types. Dependent type theory differs from the type systems used in languages like Haskell and ML in that types are first-class objects, but it seems to me that if you were going to implement something like an existential type therein, it would have to be a Sigma and not some squashing thereof.

Wikipedia’s example of an existential type is X.X×(Xint)\exists X. X\times (X\to int), a datatype containing a value of same type and a function from that same type to int. If you want to be able to apply that function to that value and get out an integer, then it seems to me that this has to be a Sigma and not a (-1)-truncated Sigma, since a (-1)-truncated Sigma can only be destructed to produce something in another (-1)-type, which int is not.

Of course, the stronger type system of DTT probably means that implementing an existential type like that would lack some good metatheoretic properties, but I don’t see how you could do it at all in any other way. Unless I’m missing something?

Posted by: Mike Shulman on November 12, 2012 10:20 AM | Permalink | Reply to this

Re: Freedom From Logic

If you take the Mitchell-Plotkin definition in the presence of Sigma types (e.g. in Coq with impredicative Set).
Then existential types and Sigma types are equivalent.
This is folklore, I would need to look for a precise reference.

Posted by: Bas Spitters on November 12, 2012 3:24 PM | Permalink | Reply to this

Re: Freedom From Logic

Dear Bas,

I was under the impression that “big” sigma-types with impredicative Set were inconsistent!?

That is, if you have impredicative types, only the “weak” eliminator for existentials (over types) is consistent. Γe:α:*.AΓ,α:*,x:Ae:CΓC:*Γunpack(α,x)=eine:C \frac{\Gamma \vdash e : \exists \alpha:\ast.\;A \qquad \Gamma, \alpha:\ast, x:A \vdash e' : C \qquad \Gamma \vdash C : \ast} {\Gamma \vdash \mathrm{unpack}\;(\alpha, x) = e \;\mathrm{in}\; e' : C} Here, I use *\ast to denote the kind of types. However, I thought the projective eliminators Γe:α:*.AΓπ 1(e):* \frac{\Gamma \vdash e : \exists \alpha:\ast.\;A} {\Gamma \vdash \pi_1(e) : \ast} and Γe:α:*.AΓπ 2(e):[π 1(e)/α]A \frac{\Gamma \vdash e : \exists \alpha:\ast.\;A} {\Gamma \vdash \pi_2(e) : [\pi_1(e)/\alpha]A} led to inconsistency, by some variant of Girard’s paradox.

Posted by: Neel Krishnaswami on November 13, 2012 10:53 AM | Permalink | Reply to this

Re: Freedom From Logic

Well, I haven’t actually tried it, but I think I would find it very difficult to get used to distinguishing between those “there is” and “there exists”. And I’d be even more hesitant to ask mathematicians without prior type-theoretic experience to learn to do so. While it’s true that we’re developing a language to be read by people who know it, I think it will benefit a lot the closer we can keep it to ordinary informal language, and in ordinary English phrases like “there is” and “there exists” are also generally treated as synonyms.

Also, using a special phrase to distinguish between a type and its (-1)-truncation goes against the whole point of “(-1)-types are not special”. The (-1)-truncation is just another modality, so it should be indicated in natural language the same way that other modalities are. (Sorry, Wren, I’m not convinced by “there is extantly” – ugh! (-: )

Wren, your second paragraph is about where I was two months ago. But all the reasons I cited above have since convinced me that this is a better way to go. In particular, while technically speaking in classical mathematics the existential does not allow a first projection, in practice one very frequently uses it this way, perhaps appealing to the axiom of choice. How much better to be specific about which type one is using! Your argument about the importance of parametricity only invokes my second bullet point: (-1)-truncated types are important. Nothing along those lines mandates that we refer to the (-1)-truncated Sigma by “there exists”. Finally, I’m not saying that language should be used this way in all of mathematics — only in informal homotopy type theory (which I separately believe will eventually become the standard in most of mathematics, but that’s a separate issue).

Posted by: Mike Shulman on November 11, 2012 12:31 AM | Permalink | Reply to this

Re: Freedom From Logic

In particular, the word “is” is such a multipurpose word, that I think it is dangerous to introduce a term of art involving only it and another extremely multipurpose word such as “there”. I imagine myself making lots of mistakes if we adopted a convention distinguishing between “there is” and “there exists”.

Posted by: Mike Shulman on November 11, 2012 12:43 AM | Permalink | Reply to this

Re: Freedom From Logic

The problem does not only occur for the existential quantifier, but also for instance for disjunction and equality. It would be better to have a solution that could work in all cases.

Posted by: Guillaume Brunerie on November 11, 2012 2:02 PM | Permalink | Reply to this

Re: Freedom From Logic

An excellent point! We can say “A merely or B”, but a distinction like “there is/there exists” doesn’t lend itself so immediately to other connectives.

Posted by: Mike Shulman on November 11, 2012 10:19 PM | Permalink | Reply to this

Re: Freedom From Logic

I could live with “merely”, but I prefer “purely”, partly because it is a less common word in ordinary English, and therefore more obviously a term of art when you come across it in mathematical writing. “Barely” and “plainly” have the wrong connotations to me.

Posted by: Mike Shulman on November 11, 2012 12:22 AM | Permalink | Reply to this

Re: Freedom From Logic

When talking to myself I usually use the word “bracket” as an adverb. For instance “there bracket exists x:Ax:A such that P(x)P(x)” or “the type of all types which are bracket equal to \mathbb{Z}”.

That’s probably not grammatically correct but it does not sound so bad and is (I think?) understandable to anyone having heard about bracket types.

Posted by: Guillaume Brunerie on November 10, 2012 5:02 AM | Permalink | Reply to this

Re: Freedom From Logic

Yes, it’s certainly not grammatical with the usual word ‘bracket’. I’m also generally against naming mathematical concepts after their notations — I think it’s much better to find a name that actually describes their meaning. (One of the worst examples of this is the ‘bar construction’, which is named after a notation that nobody ever uses any more!)

Posted by: Mike Shulman on November 10, 2012 2:54 PM | Permalink | Reply to this

Re: Freedom From Logic

The last point in your list captures something that is currently broken in the informal language we use to express mathematics. I’m currently writing a paper where one of the statements I want to make is “Our Radford isomorphism blah, is the same as the one constructed in ENO’s paper.” But their statement (Thm 3.3) is “There is a natural blah” and the actual construction is in the proof. So the statement I’ll end up having to make is “Our proof of this theorem constructs the same blah as ENO’s proof of the same theorem.” But the actual statement I want is “Our proof and their proof can be directly translated into each other in the following way” which is perhaps one level higher in the hierarchy that you’re discussing.

Surely there’s some better way to deal with this construction/proposition problem in ordinary (non-HTT) informal mathematical language? Does anyone have a better way to state theorems like “We construct a blah.”

Posted by: Noah Snyder on November 10, 2012 10:48 AM | Permalink | Reply to this

Re: Freedom From Logic

Hope the mention of Radford will not disappear in your final choice.

Posted by: jim_stasheff on November 10, 2012 1:33 PM | Permalink | Reply to this

Re: Freedom From Logic

We’ll definitely call this is “the Radford isomorphism” no matter how this particular proposition is phrased. (In fact, we call the image of the Dirac belt bordism in any fully dualizable 3-category “the Radford iso.”)

Posted by: Noah Snyder on November 10, 2012 2:19 PM | Permalink | Reply to this

Re: Freedom From Logic

Hope the mention of Radford will not disappear in your final choice.

Posted by: jim_stasheff on November 10, 2012 1:33 PM | Permalink | Reply to this

Re: Freedom From Logic

One answer is to call it a ‘Definition’ rather than a theorem.

Posted by: Mike Shulman on November 10, 2012 2:55 PM | Permalink | Reply to this

Re: Freedom From Logic

Then where do you put the argument? From a typesetting point of view, definitions are typeset to be short things. For a proposition you follow it with a proof. But definition/proof is pretty far from common usage. I guess one common solution is Definition/Theorem, which can be followed by a proof.

Posted by: Noah Snyder on November 10, 2012 3:01 PM | Permalink | Reply to this

Re: Freedom From Logic

Well, you need to make some change to common usage. Definition/proof seems perfectly reasonable to me. I think there are lots of mathematical papers that would be improved by the freedom to write definition/proof: how many times does a ‘definition’ still require a proof that it defines the kind of thing you claimed?

Posted by: Mike Shulman on November 10, 2012 3:07 PM | Permalink | Reply to this

Re: Freedom From Logic

Noah wrote: Does anyone have a better way to state theorems like “We construct a blah.”?

What I think of the standard way of doing this is to first have a subsection constructing X. Then you have a theorem saying “X is a blah”.

This is like how it’s not so good to say X×YX\times Y is isomorphic to Y×XY\times X — it’s much better to first construct the map (which in this case isn’t too hard) and then assert that that map is an isomorphism. This is because people usually want to know what the isomorphism actually is, and they don’t want to have to comb through your proof to find that out.

I tend to think of a theorem of the form “We construct a blah” as more of an advertisement. In my opinion, it’s good to put things like that in an introduction or an abstract but better to leave them out of the body of the paper. For me the purpose of the Proof/QED delimiters is to tell the reader that if they’re willing to accept the truth of the theorem but skip what’s between the Proof and the QED, then the rest of the paper will still make perfect sense.

Posted by: James Borger on November 11, 2012 3:28 AM | Permalink | Reply to this

Re: Freedom From Logic

Instead of replacing “there exists”, why not appropriate some other phraseology? For example, the propositions-as-types version of the axiom of choice could be stated like this: if, for all xx in XX, we have an element y(x)y (x) of type Y(x)Y(x), then we have a function yy of type X x:XY(x)X \to \sum_{x : X} Y(x) such that y(x)y (x) is in Y(x)Y (x) for all xx in XX.

Of course, it is precisely this kind of phrasing that makes the axiom of choice sound obviously true. Contrast the obviously false version: if, for all xx in XX, someone has an element of Y(x)Y (x), then someone has a function yy such that y(x)y (x) is in Y(x)Y (x) for all xx in XX. (After all, no-one said all the “someones” are the same person!)

Posted by: Zhen Lin on November 10, 2012 12:22 PM | Permalink | Reply to this

Re: Freedom From Logic

Yes, that’s another possibility we discussed. But neither group wants to give up ‘there exists’, so who has the right to step in and dictate which side gets to keep it (not to speak of enforcing it)? Plus, I think all the other reasons I cited above make the case that there’s no good reason to keep ‘there exists’ tied to (-1)-types.

Posted by: Mike Shulman on November 10, 2012 3:00 PM | Permalink | Reply to this

Re: Freedom From Logic

I just realized that there is another perfectly good name for (-1)-types: subsingletons. So if we really wanted to get rid of the word ‘proposition’ entirely, maybe we could.

Posted by: Mike Shulman on November 10, 2012 3:02 PM | Permalink | Reply to this

Re: Freedom From Logic

I’m reminded of a wonderful diatribe by James Dolan at the IMA workshop in Minneapolis against the idea of mathematics being merely about proving propositions. I wish I had it taped. The essence, though, was to argue that establishing mere truth values was a wretched impoverishment.

Posted by: David Corfield on November 10, 2012 4:33 PM | Permalink | Reply to this

Re: Freedom From Logic

You are not the first person to propose developing informal mathematical language and notation from the formal kind. Nor am I, but I would like to take this opportunity to plug Section 1.6 of my book, which relates proof boxes to mathematical idiom.

In particular, I have an explanation of the idiom “there exists”, in which the witness becomes available, in contrast to the quantifier, in which it is a bound variable. Personally, I prefer to read the quantifier as “for some”, matching “for all”.

Charles Wells has also written “A Handbook of Mathematical Discourse”. I see from my Web search for this that other people have discussed the subject too.

I like your proposal to use adverbs as modalities for mathematical statements. However, I think you will need to experiment with this in informal settings such as seminars before you commit yourself in writing or on line to the use of particular words.

I have never much liked the name “proof irrelevance”. Proofs are not irrelevant, though they may be anonymous. So, “there exists anomymously” or “for some anonymous” might work better in the idioms you propose.

For the benefit of people who have not heard about Homotopy Type Theory, your discussion would benefit from some explanation of type levels and especially of how you assign numbers such as -1 to them.

Posted by: Paul Taylor on November 10, 2012 11:20 PM | Permalink | Reply to this

Re: Freedom From Logic

You are not the first person to propose developing informal mathematical language and notation from the formal kind.

Okay, good to know. (Note that, as I said, I was not the proposer of this project: Peter Aczel was. I’m merely blogging about it.)

I think you will need to experiment with this in informal settings such as seminars

…and blogs. (-: Of course, it’s obvious that we need to experiment before making a decision. That’s the whole point of the project.

For the benefit of people who have not heard about Homotopy Type Theory, your discussion would benefit from some explanation of type levels and especially of how you assign numbers such as -1 to them.

I did link to the nLab page on homotopy type theory, which hidden further down somewhere has a link to truncated object. But probably a better place to start is my introductory sequence of blog posts, in the second of which I discussed nn-types. Unfortunately, I don’t have space to review the whole theory in every new post….

Posted by: Mike Shulman on November 11, 2012 12:36 AM | Permalink | Reply to this

Re: Freedom From Logic

I like the meaning of ‘anonymously’. However, I think it’s a few too many syllables for everyday use. Namelessly? Unknown-ly? Obscurely? Ineffably? Secretly? Covertly?

Or we could play off the fact that (-1)-types are subsingletons: singly, singularly.

Posted by: Mike Shulman on November 12, 2012 12:13 AM | Permalink | Reply to this

Re: Freedom From Logic

I’m not crazy about “purely,” because “pure” has a pretty common meaning in programming languages/type theory already: the absence of computational effects. And because effects are often represented as monads, and bracketing also forms a monad, these two meanings are at odds here. I like “merely”.

Posted by: Dan Licata on November 11, 2012 3:28 AM | Permalink | Reply to this

Re: Freedom From Logic

Oh, darn, I forgot all about that meaning of “pure”. Yes, you’re right, we can’t use it as a monadic modality when “pure” also means without effects. (Although that suggests that we could instead use “purely” when we want to emphasize the lack of a modality, or rather the identity modality.)

I’m still not crazy about “merely” — it sounds a little too dismissive for my taste. It’s better than anything else we’ve thought of yet, but we’ve only just barely started looking….

Posted by: Mike Shulman on November 11, 2012 10:22 PM | Permalink | Reply to this

Re: Freedom From Logic

I like what you wrote! But some comments:

  • On informal type theory: I don’t think this is a new idea – the idea of going from a formal system to an informal system is at least as old as McCarthy’s LISP, and in type theory this is played out everyday in languages like Haskell and Agda (which have theoretical foundations and strive to be sound, but sometimes step outside what is formally justified when this is helpful for Getting Things Done), and even to some extent in languages like ML and Coq (which are more conservative, but still have some unformalized aspects). The point is that “implemented in software” \ne formal.
  • On terminology: I’m with Dan Licata about “purely”: it rings backwards to me, since in the terminology of computational effects saying that a term tt of a certain type τ\tau is “pure” is precisely saying that you don’t need to perform any translation on τ\tau to understand the computational content of tt.
  • On the meaning of quantifiers in mathematical language: I think this is a fascinating question, which is really part of the larger question of explicating the computational content of natural language. In fact, type theory has proven helpful in understanding quantifiers in natural language, as has the theory of continuations and side effects.
Posted by: Noam Zeilberger on November 11, 2012 6:54 PM | Permalink | Reply to this

Re: Freedom From Logic

Thanks! I already conceded to Paul that this may not be the first time for going from formal to informal. However, I disagree that programming languages are at all similar. Any programming language is, by definition, a formal system, even if the complete description of that system exists only in the form of the source code of its compiler.

Posted by: Mike Shulman on November 11, 2012 10:23 PM | Permalink | Reply to this

Re: Freedom From Logic

That is not my definition of “programming language”. The meaning of any real programming language is tied inextricably to its use, just as the meaning of any natural language is. And while it can be very useful to have formal definitions of idealized programming languages—just as it can be useful in linguistics to try to give a formal grammar/semantics for toy fragments of natural language—it is important not to lose sight of the bigger picture.

Take the examples of ML and Haskell. There is a formal definition of Standard ML, and this is very useful for posing and answering questions about the language, but certainly it does not provide a framework for discussing all issues one cares about when programming in ML (for example, questions about the time-space efficiency of execution, or about interaction with external libraries written in different languages). And on the other hand, while it is sometimes a source of confusion and ambiguity that Haskell does not have a comparable formal definition, these problems are not resolved by referring to the source code of a compiler – for one, because there are multiple different compilers for Haskell!

Posted by: Noam Zeilberger on November 11, 2012 11:02 PM | Permalink | Reply to this

Re: Freedom From Logic

But the meaning of a programming language is still determined by what happens when you run it on a computer. Maybe that meaning encompasses different things depending on what compiler or architecture you use, or how much memory you have, or whatever. But all of that information is completely determined by the code once it is written.

By contrast, the meaning of informal mathematics lies only in the heads of mathematicians, and in a tacit understanding that it could be formalized in some formal system. Actually doing such a formalization is, as Assia emphasized in her talk here at IAS on Friday, extremely nontrivial, requiring human thought and creativity, and the correction of many local errors.

Posted by: Mike Shulman on November 12, 2012 12:04 AM | Permalink | Reply to this

Re: Freedom From Logic

Again, the complete description of “what happens when you run it on a computer” is not the way people reason about programs in languages like Haskell and Agda because: 1. even if you fixed a compiler/machine, it still wouldn’t be well-defined (e.g., the program might communicate with programs running on other machines/written in different languages, and in the limit you would have to know the complete state of the universe and the laws of physics), 2. it is much easier to reason informally in terms of an idealized model (e.g., modelling types in Haskell as domains or even as sets, though the latter is known to be in general unsound) and a simple calculus (e.g., the βη equations), and very often this is good enough—in cases where it isn’t, either you you go back and revise the model or you to take a break from formal reasoning.

My point is that this latter activity—the way people actually reason inside a typed programming language—is informal type theory. The fact that there may exist a compiler/operating system/hardware that lets the programmer physically run her program and observe some result is simply a (very nice) bonus.

Actually, my views here are pretty close to what Dan Piponi wrote in “What Category do Haskell Types and Functions Live In?”: “So the question to ask isn’t ‘what category does Haskell live in?’ but ‘what class of category corresponds to the internal language in which I wrote this bit of code?’.”

Posted by: Noam Zeilberger on November 12, 2012 1:13 AM | Permalink | Reply to this

Re: Freedom From Logic

That sounds to me like reasoning in ordinary informal mathematics about an idealized model of a programming language.

Posted by: Mike Shulman on November 12, 2012 10:35 AM | Permalink | Reply to this

Re: Freedom From Logic

Certainly there could be a mix of reasoning that is machine-checked and reasoning that is human-checked (in Haskell and ML a lot more of the latter goes on than in Agda and Coq). But surely we can agree that there is a spectrum of formality, and the mere fact that a particular piece of software running on a particular machine lends its authority to a fragment of text does not in itself make the latter a formal proof, any more so than the fact that an argument is conveyed by one human to another in English makes it informal.

Posted by: Noam Zeilberger on November 12, 2012 10:55 PM | Permalink | Reply to this

Re: Freedom From Logic

Indeed, I would not disagree with that. But I still stand behind my last comment.

Posted by: Mike Shulman on November 13, 2012 6:38 PM | Permalink | Reply to this

Re: Freedom From Logic

While there is precedent for using “pure existence” to mean something rather less than pure existence, as a Computer Scientist I have to agree with Dan and Noam that it would be a bad idea to use “purely exists” for the non-constructive form.

Why not “cannot fail to exist”? The implied double-negation is in fact a “squashing” modality—indeed, it was the first form of squashing we consider in NuPRL way back in the early 80’s. (Subsequently squashing was defined to mean quotient by the full relation, which makes good sense in the context of HIT’s.)

I must disagree with Wren’s contention about the existential quantifier. I would rather say that conventional logic does not have a proper existential quantifier, precisely because it is impossible to speak of the witness given by a proof. We’ve managed to muddle through to some degree, but now that we have reached a more sophisticated understanding of concepts such as the squashing modality, I think we may change our perspective about this longstanding issue.

Posted by: Bob Harper on November 12, 2012 1:03 AM | Permalink | Reply to this

Re: Freedom From Logic

Another suggestion: “there must exist”? It conveys the sense of not having provided the witness, but asserting that there must be one.

Posted by: Bob Harper on November 12, 2012 2:13 AM | Permalink | Reply to this

Re: Freedom From Logic

Thanks for your thoughts, Bob! I think the problem with ‘there cannot fail to exist’ is that squashing is different from double negation. Double negation puts you into a classical-like logic, while squashing is still intuitionistic.

‘There must exist’ sounds intuitively to me like a stronger statement than ‘there exists’. And how would you pronounce a squashed ‘or’?

Posted by: Mike Shulman on November 12, 2012 10:29 AM | Permalink | Reply to this

Re: Freedom From Logic

I was thinking of “it must be around here somewhere,” which implies that you haven’t actually found it but are sure it is there.

For disjunction one might say “there must exists either an A or a B”, with explicit reference to the proof object. After all, as soon as you case analyze you name the proof object for each case. Formally, A+B is Exists d:2 s.t. d=0 implies A and d=1 implies B. Adding the “must” weakens it to classical disjunction.

Posted by: Bob Harper on November 12, 2012 12:19 PM | Permalink | Reply to this

Re: Freedom From Logic

First: I’ve been thinking about such adverbs for a while now, and came to the conclusion that the precise adverb you choose matters little, compared to your power to enforce it (when enough people use it, it becomes a second nature, and the original meaning disappears in the background).

I kind of like “must”, it resonates well with how intuitionistic logic works. It makes the disjunction quite a mouthful, which is displeasing, but I tend to believe that there is not an adverb which combines properly with “or” (it’s not a verb after all). There may be more comfortable choices however.

Another adverb can be “choicelessly” to reflects that truncation robs us from picking a choice (using the principle of choice, or whatever). “There choicelessly exists”, “Choicelessly A or B”… Well, it doesn’t mean the same as in plain English, but considering it’s a non-standard neologism to start with…

Also, let me mention that V. Pratt likes to read the double negation as “surely”. That’s pretty neat. It’s a better adverb than “classically” at least.

Posted by: Arnaud Spiwack on November 12, 2012 1:49 PM | Permalink | Reply to this

Re: Freedom From Logic

the precise adverb you choose matters little, compared to your power to enforce it

But, your ability to convince other people to use it may depend greatly on the precise adverb you choose. Since mathematics is not about power and enforcement, but rather consensus and discussion. (-:

Posted by: Mike Shulman on November 12, 2012 2:33 PM | Permalink | Reply to this

Re: Freedom From Logic

Well, by power of enforcement, I meant “a number of people ready to repeat it in front of many audiences”. People won’t choose to use a word because it conveys elegantly an intuition of the object it refers to, but because they’ve heard it first and can’t get it out of their head.

Posted by: Arnaud Spiwack on November 12, 2012 2:51 PM | Permalink | Reply to this

Re: Freedom From Logic

I disagree. There is an effect of “first past the post” when naming concepts, but to be “sticky” (for people to be “unable to get it out of their head”), a name should also be a good one. And even if it were true that whatever word we choose will stick, we should still want to choose a good word!

Posted by: Mike Shulman on November 12, 2012 2:56 PM | Permalink | Reply to this

Re: Freedom From Logic

I was thinking of “it must be around here somewhere,” which implies that you haven’t actually found it but are sure it is there.

Sure, but I was just saying how it sounds to me. I have the same problem with “surely” — in ordinary English, both are emphasis words which make a sentence stronger, not weaker.

as soon as you case analyze you name the proof object for each case.

Not in informal mathematics!

Adding the “must” weakens it to classical disjunction.

Where by “classical” you mean “intuitionistic”? (-:

Posted by: Mike Shulman on November 12, 2012 2:31 PM | Permalink | Reply to this

Re: Freedom From Logic

Surely you must be joking!

Maybe if you imagine them pronounced with an upper-class British accent, they may sound closer to what was intended.

Here is another adverb though: “evidently”. “There evidently exists”, “evidently A or B”.

Posted by: Arnaud Spiwack on November 12, 2012 2:56 PM | Permalink | Reply to this

Re: Freedom From Logic

I think would be a poor decision to choose mathematical terminology that only sounds correct when pronounced in an upper-class British accent.

“Evidently” is also an emphasis word, and is also commonly used in informal mathematics in the same way as “clearly” or “it is easy to show that” or “it is left to the reader to show that”. No word of that sort should be hijacked for a precise meaning.

Posted by: Mike Shulman on November 12, 2012 3:01 PM | Permalink | Reply to this

Re: Freedom From Logic

The British accent thing was a joke, of course.

Posted by: Arnaud Spiwack on November 12, 2012 3:23 PM | Permalink | Reply to this

Re: Freedom From Logic

There surely exists?

Posted by: John Beattie on November 12, 2012 5:41 PM | Permalink | Reply to this

Re: Freedom From Logic

“is extant”?

Posted by: Bob Harper on November 13, 2012 3:06 AM | Permalink | Reply to this

Re: Freedom From Logic

‘There must exist’ sounds intuitively to me like a stronger statement than ‘there exists’.

Perhaps “ought (to)” would better match Bob’s idea then? Saying “there ought to exist an X such that…” seems to capture the idea of things existing without having recourse to an explicit witness. But then perhaps the deontic modality would be better used for, oh, deontics. Also, it’s not clear how to extend it to disjunction and the like.

Posted by: wren ng thornton on November 14, 2012 6:48 AM | Permalink | Reply to this

Re: Freedom From Logic

A few more suggestions (most of which will probably be deemed unacceptable by some, just tossing ideas around):

intuitionistically
constructively
sceptically
materially
simply
ordinarily
provably
absolutely
mainly
chiefly
pretty much
coarsely
theoretically
in principle
propositionally
indistinguishably

Posted by: Arnaud Spiwack on November 13, 2012 9:21 AM | Permalink | Reply to this

Re: Freedom From Logic

How about keeping the exists x : A for the squashed case and using “we have x : A and P x”, “we have t : A with P t” or “we have t : A and pt : P t”. To me, exists clearly indicates that we care about existence and not actual content, so I’m perfectly willing to give it up to truncated versions of the sigma type. I think it’s gonna be hard to find an adverb that weakens the exists in the squashed version without feeling weird because it’s all this is about, existence. And similarly for the Sigma type, existence is not the central point, the identity of the object is.
I’d add that “we have (a specific) t : A and pt : P t” can be used both to introduces a name for the witness or give the witness and “proof”/second component directly. It should work well with the Definition of first component and Proof/Definition of the second component workflow too.

For or you would get “we have a : A or b : B”, i.e. case analysis in binding position, and explicit reference to the witnesses in term position “we have t : A or B”/”we have A or t : B”. Leaving the injection implicit in most cases thanks to context, you could also write “we have t : A or B”.

My 2 cents…

Posted by: Matthieu Sozeau on November 13, 2012 11:28 PM | Permalink | Reply to this

Re: Freedom From Logic

Some questions:

Is there something modal about adding ‘natural’ or ‘canonical’ to isomorphism?

Thinking of the operator – ‘It is locally the case that…’, how should I think of it applied to a type in general? Something like taking the interior?

Does this work on higher modalities make contact with category theoretic semantics for first-order modal logic, e.g., sheaves and ionads?

Posted by: David Corfield on November 19, 2012 9:35 AM | Permalink | Reply to this

Re: Freedom From Logic

Is there something modal about adding ‘natural’ or ‘canonical’ to isomorphism?

Good question. It does seem intuitively sort of “modal”, but it’s an odd sort of modality in that it can only be applied to a particular sort of type (namely, types of families of isomorphisms). I can’t think offhand of any way of expressing it in a way that looks formally modal.

Thinking of the operator – ‘It is locally the case that…’, how should I think of it applied to a type in general?… Does this work on higher modalities make contact with category theoretic semantics for first-order modal logic, e.g., sheaves and ionads?

What I was thinking of when I wrote “locally” as a modality was very close to the latter situation: you have a left-exact reflective subcategory (i.e. a “subtopos of sheaves”) and “locally” refers to applying the reflection. This sort of modality is only the “monadic” sort, however; I don’t know how to express the “comonadic” sort internally in this way (the problem is that they don’t usually seem to be stable under pullback).

Posted by: Mike Shulman on November 19, 2012 3:33 PM | Permalink | Reply to this

Re: Freedom From Logic

Perhaps this business of thinking about adverbs (or other auxiliary words) would be easier if we stepped out of the context of mathematics for a moment.

Imagine that you’re in a meeting of your entire department. Just moments before, a government agent knocked on your office door and showed you convincing proof that secret documents of national importance are being leaked from your department to enemy agents. Now you sit faced with your colleagues. You are sure that the number of traitors in the room is non-zero. And yet, as you look around the room at each person, you can’t bring yourself to believe that he or she is a traitor. So how do you express to yourself the thought “There is a traitor in this room”, or “One of these people here is a traitor”, or “We have a traitor amongst us” without the connotation that you believe of any particular person that they are the traitor? Is there an adverb, adjective, or other turn of phrase that succinctly conveys this sense of (known) existence without (known) exemplar?

Posted by: Stuart on November 23, 2012 9:17 AM | Permalink | Reply to this

Known existence without known exemplar

The word for that is anonymous(ly), as I said before.

Please don’t use must or evident(ly) because they suggest the (traditional) modal operators.

When I said earlier that there had been previous accounts of the mathematical vernacular, I was trying to give some encouragement to this discussion, not to have a priority dispute.

Posted by: Paul Taylor on November 27, 2012 9:00 AM | Permalink | Reply to this

Re: Freedom From Logic

If I’m understanding this at all correctly (and it is entirely possible that I am not), then “erasably” may be the proper terminology here. My intuition is to relate (-1)-truncated types to phase distinctions in dependently typed language technology. My reference on this would be McKinna and Brady’s “Phase Distinctions in the Compilation of EPIGRAM”: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.131.7913

I think that even more than (-1)-truncated types may be erasable at times, is one is sufficiently clever. So perhaps “trivially erasably” or “simply erasably” would be more correct.

Or rather than adverbs we could move to adjectives, so “there erasably exists” becomes “there exists an erasable” or “there exists a trivially erasable”.

Posted by: Gershom B on December 2, 2012 9:25 PM | Permalink | Reply to this

Re: Freedom From Logic

One problem with a lot of these suggestions (like irrelevant, anonymous, ond erasable) is that inhabitants of (-1)-truncated types aren’t exactly the same as proof-irrelevant types in traditional type theory. In fact, we can and must sometimes make use of their actual inhabitants: it’s just that the result of such use is independent — propositionally — of what that inhabitant was.

For instance, the type asserting that a function ff is an equivalence is (-1)-truncated, but an inhabitant of it contains the data of the inverse of ff, and very frequently we need to extract from it that actual inverse, which is a function going in the other direction. Up to homotopy, what we do with that inverse doesn’t depend on what it was, but it’s vitally important that we have it. Moreover, sometimes we even care about that inverse more than propositionally: if we supplied a specific inverse when we proved that ff was an equivalence, then we may want to get out that specific function from the inhabitant of ‘ff is an equivalence’, including its computational behavior.

Technically, that means that inhabitants of (-1)-truncated types cannot be put into Coq’s sort ‘Prop’, nor can they even be declared with ‘Qed’ rather than ‘Defined’ (at least not always). So all the words which evoke the traditional notion of proof irrelevance are at best a little misleading.

At the last informal type theory meeting here at IAS, there seemed to be broad support for the idea of calling (-1)-truncated types mere propositions, evoking the adverb ‘merely’ which seemed to be gaining ground for (-1)-truncation, and also acknowledging that all types may be called ‘propositions’.

Posted by: Mike Shulman on December 3, 2012 3:14 PM | Permalink | Reply to this

Re: Freedom From Logic

We can and must sometimes make use of their actual inhabitants: it’s just that the result of such use is independent — propositionally — of what that inhabitant was.

This is why the word should be anonymous and not irrelevant,

Posted by: Paul Taylor on December 9, 2012 10:36 PM | Permalink | Reply to this

Re: Freedom From Logic

We can and must sometimes make use of their actual inhabitants: it’s just that the result of such use is independent — propositionally — of what that inhabitant was.

This is why the word should be anonymous and not irrelevant,

Posted by: Paul Taylor on December 9, 2012 10:40 PM | Permalink | Reply to this

Re: Freedom From Logic

How about ‘non-informatively’ or ‘uninformatively’ (lots of syllables, I know)? It was used in section 4.1 in this article on implementing reals in Coq.

On a lighter side, what about ‘NTW-exists’ (or variants), where NTW stands for None-The-Wiser?

Posted by: David Roberts on December 4, 2012 4:45 AM | Permalink | Reply to this

Re: Freedom From Logic

I think that has the same problem mentioned in my comment above.

Posted by: Mike Shulman on December 4, 2012 7:38 AM | Permalink | Reply to this

Re: Freedom From Logic

I recently found an old essay by de Bruijn, which I think is very much in the spirit of these discussions:

The Mathematical Vernacular, A Language for Mathematics with Typed Sets by N.G. de Bruijn

De Bruijn writes that “the idea to develop MV [Mathematical Vernacular] arose from the wish to have an intermediate stage between ordinary mathematical presentation on the one hand, and fully coded presentation in Automath-like systems on the other hand.” His goals are slightly more ambitious in that he is trying to formalize a fragment of mathematical vernacular using type-theoretical ideas (though he doesn’t try to do machine verification, saying “it may require quite some amount of artificial intelligence”). But I think that ultimately he was aiming for a sort of fixed point between formal and informal language:

Many people like to think that what really matters in mathematics is a formal system (usually embodying predicate calculus and Zermelo-Fraenkel set theory), and that everything else is loose informal talk about that system. Yet the current formal systems do not adequately describe how people actually think, and, moreover, do not quite match the goals we have in mathematical education. Therefore it is attractive to try to put a substantial part of the mathematical vernacular into the formal system. One can even try to discard the formal system altogether, making the vernacular so precise that its linguistic rules are sufficiently sound as a basis for mathematics.

Posted by: Noam Zeilberger on January 29, 2013 11:33 PM | Permalink | Reply to this
Read the post The King of France
Weblog: The n-Category Café
Excerpt: Bringing dependent type theory to philosophy
Tracked: February 1, 2013 3:52 PM

Post a New Comment