Compatibility with classical mathematics

[mikeshulman]

Should we try to modify the introduction to make it more obvious that HoTT is compatible with classical mathematics? (Cf. discussion on the mailing list.)

Here is one proposal: d151e50b

[JasonGross]

For the record, the thread is here, and this question is brought up on Jan 10.

[marcbezem]

I really think the more positive sentence I proposed is better than the current 296. Here it comes:

"On the other hand, this notion of “or” is so strong that one must be careful in formulating the law of excluded middle. The formulation "for all \emph{propositions} A, either A or not A" is perfectly consistent with the univalence axiom. (In HoTT, not all types are considered to be propositions)."

In the next sentence, it would be good to stress:

"For if we assume ``for all \emph{types} $A$ ... "

The reason is simple: first things first. Though it is informative that something is inconsistent, it is much more important that classical logic IS consistent with univalence. That should come first, even if the notion of "proposition" is not completely clear yet. That's fine for an introduction.

It is far from optimal to explain a new concept by counterexamples.

Marc

[mikeshulman]

@marcbezem, the problem with your sentence is that it doesn't fit the flow of the section. The idea of stratification of types into sets, propositions, etc. is not introduced until several paragraphs later.

[marcbezem]

That's true, but you don't need the stratification, only "(In HoTT, not all types are considered to be propositions)." One could even have that sentence second, without (), after my first sentence. The message would be: HoTT is richer than MLTT, not all types are considered to be propositions, and LEM for propositions is OK. Then, in the next para, the warning not to overstretch LEM (which has probably never been meant to be stretched that far).

[mikeshulman]

But that sentence isn't even true. We do sometimes use PAT.

[RobertHarper]

And we do sometimes use PAT with full-on LEM --- this was the subject of Chet Murthy's PhD thesis which established the connection between continuations and classical logic.

Part of the "public relations" problem is that different people mean different things by "proposition". Andrej's note today stresses a more classical perspective in which they are sub-singletons, and points out that we can certainly augment these with LEM and get classical logic as usually practiced. But a "strict constructivist" (pardon the pun, may only be meaningful to americans on this list) would insist that propositions are arbitrary types, and that the fully general form of LEM postulating decidability of all types is, at times, provable, at other times appropriate as an assumption, but is not to be postulated generally. In particular, what is currently being described as the "wrong" meaning of disjunction is, on that view, the only correct meaning of disjunction.

I am not taking sides here, just observing that this seems to be reasons people get confused and we have a hard time agreeing on how best to explain the situation to outsiders. It doesn't help that, historically, "constructivism" has been interpreted as being somehow opposed to classicism in mathematics, starting with Hilbert's misplaced opposition ("taking away boxing gloves" and all that). So many bring a skeptical or negative attitude towards the word. And Martin has pointed out that, unfortunately, the same applies to "synthetic". Sigh.

Bob

On Jan 13, 2014, at 16:33, Mike Shulman notifications@github.com wrote:

But that sentence isn't even true. We do sometimes use PAT.

— Reply to this email directly or view it on GitHub.

[mikeshulman]

Well, the "we" who uses PAT with LEM is not the "we" of the book, since it is inconsistent with UA. (-:

[vladimirias]

There is only one formulation of LEM in the UF: isaprop P -> coprod P ( P -> empty ).

Anything else is not a formulation of LEM in UF. Since the book is about UF and not about general spread of ideas in the Type Theory I think we should make this very clear.

V.

On Jan 13, 2014, at 4:44 PM, Robert Harper wrote:

And we do sometimes use PAT with full-on LEM --- this was the subject of Chet Murthy's PhD thesis which established the connection between continuations and classical logic.

Part of the "public relations" problem is that different people mean different things by "proposition". Andrej's note today stresses a more classical perspective in which they are sub-singletons, and points out that we can certainly augment these with LEM and get classical logic as usually practiced. But a "strict constructivist" (pardon the pun, may only be meaningful to americans on this list) would insist that propositions are arbitrary types, and that the fully general form of LEM postulating decidability of all types is, at times, provable, at other times appropriate as an assumption, but is not to be postulated generally. In particular, what is currently being described as the "wrong" meaning of disjunction is, on that view, the only correct meaning of disjunction.

I am not taking sides here, just observing that this seems to be reasons people get confused and we have a hard time agreeing on how best to explain the situation to outsiders. It doesn't help that, historically, "constructivism" has been interpreted as being somehow opposed to classicism in mathematics, starting with Hilbert's misplaced opposition ("taking away boxing gloves" and all that). So many bring a skeptical or negative attitude towards the word. And Martin has pointed out that, unfortunately, the same applies to "synthetic". Sigh.

Bob

On Jan 13, 2014, at 16:33, Mike Shulman notifications@github.com wrote:

But that sentence isn't even true. We do sometimes use PAT.

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub.

[awodey]

I agree — and I think Mike’s proposed revision does this.

On Jan 13, 2014, at 6:22 PM, Vladimir Voevodsky notifications@github.com wrote:

There is only one formulation of LEM in the UF: isaprop P -> coprod P ( P -> empty ).

Anything else is not a formulation of LEM in UF. Since the book is about UF and not about general spread of ideas in the Type Theory I think we should make this very clear.

V.

On Jan 13, 2014, at 4:44 PM, Robert Harper wrote:

And we do sometimes use PAT with full-on LEM --- this was the subject of Chet Murthy's PhD thesis which established the connection between continuations and classical logic.

Part of the "public relations" problem is that different people mean different things by "proposition". Andrej's note today stresses a more classical perspective in which they are sub-singletons, and points out that we can certainly augment these with LEM and get classical logic as usually practiced. But a "strict constructivist" (pardon the pun, may only be meaningful to americans on this list) would insist that propositions are arbitrary types, and that the fully general form of LEM postulating decidability of all types is, at times, provable, at other times appropriate as an assumption, but is not to be postulated generally. In particular, what is currently being described as the "wrong" meaning of disjunction is, on that view, the only correct meaning of disjunction.

I am not taking sides here, just observing that this seems to be reasons people get confused and we have a hard time agreeing on how best to explain the situation to outsiders. It doesn't help that, historically, "constructivism" has been interpreted as being somehow opposed to classicism in mathematics, starting with Hilbert's misplaced opposition ("taking away boxing gloves" and all that). So many bring a skeptical or negative attitude towards the word. And Martin has pointed out that, unfortunately, the same applies to "synthetic". Sigh.

Bob

On Jan 13, 2014, at 16:33, Mike Shulman notifications@github.com wrote:

But that sentence isn't even true. We do sometimes use PAT.

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub.

[marcbezem]

@mikeshulman, and all others, of course. Sorry for being unclear. When I wrote "LEM (which has probably never been meant to be stretched that far)" I expressed my opinion, not a fact, and it was certainly not a proposal for a sentence for the book. What I mean is that, when one stretches LEM beyond propositions, one postulates an interesting type-theoretic axiom, but I would personally not see it as a logical axiom. (Imo the only logical LEM is LEM_{-1}, so I agree with Vladimir. One could even argue that the higher LEM's are misnomers in HoTT.)

My point on exposition is the following. If B comes after A in the correct mathematical flow, but happens to be much more important than A, then it can be better to mention B before A, after a minimal preparation necessary for the appreciation B. This is exactly the freedom one has in an introduction, and we should use that freedom here. Mike's revision, although an improvement, does not do this, imo.

[vladimirias]

On Jan 13, 2014, at 4:32 PM, Marc Bezem notifications@github.com wrote:

That's true, but you don't need the stratification, only "(In HoTT, not all types are considered to be propositions)." One could even have that sentence second, without (), after my first sentence. The message would be: HoTT is richer than MLTT, not all types are considered to be propositions, and LEM for propositions is OK. Then, in the next para, the warning not to overstretch LEM (which has probably never been meant to be stretched that far).

— Reply to this email directly or view it on GitHub.

BTW in the intro to the book you do explain the UF approach to sets before you discuss constructivity. If you have started by saying that ``here is how we define propositions in the UF and here is how we implement intuitionistic and classical logics on the UF-propositions" and then discussed discussed how to define sets in the UF and how to implement basic set theory(ies) of UF-sets may be things would get clearer.

V.

[mikeshulman]

I have been trying to avoid radical restructuring of the intro, because we spent a lot of time last year trying to make it acceptable to all the authors and I don't want to go into that all again. But maybe I'll try moving things around a tiny bit, so we can see what it would look like.

[mikeshulman]

Okay, here is another possibility: 45772e28

[mikeshulman]

I'm going to consider this closed by #616.