Notes on Logic

[mikeshulman]

The Notes to Chapter 3 could use some love. I think it would be nice to include a bit of mention of different ways that type theories can treat logic (e.g. logic on top of type theory, logic-enriched type theory, as well as PAT and PAST). Also a bit of history of intuitionistic and constructive logic, perhaps, and of AC and unique choice? Maybe mention how unique choice fails in LETT and Coq.

[awodey]

I'll get started on this and others can add on.

[spitters]

I have added some more refs.

On Fri, Apr 26, 2013 at 11:16 PM, Steve Awodey notifications@github.comwrote:

I'll get started on this and others can add on.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/179#issuecomment-17100475 .

[awodey]

in the Notes there is now a paragraph that begins "The adverb “purely” as used to refer to untruncated logic is a reference to the use of monadic modalities to model effects in programming languages. ..." This is news to me! Then there is a bunch of stuff about monads and Haskell and programming languages. I don't think this really belongs here -- at least not as an explanation of the use of "purely" vs. "merely", which I thought was strictly a logical matter.

[spitters]

I believe the suggestion to use "purely" may have been Bob's. The explanation seems nice, where do you propose to put it?

On Tue, Apr 30, 2013 at 4:13 PM, Steve Awodey notifications@github.comwrote:

in the Notes there is now a paragraph that begins "The adverb “purely” as used to refer to untruncated logic is a reference to the use of monadic modalities to model effects in programming languages. ..." This is news to me! Then there is a bunch of stuff about monads and Haskell and programming languages. I don't think this really belongs here -- at least not as an explanation\ of the use of "purely" vs. "merely", which I thought was strictly a logical matter.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/179#issuecomment-17229431 .

[dlicata335]

I don't recall who suggested the word (it wasn't me, so probably Bob?), but I believe that "purely" was adopted because it is used in programming languages to refer to the absence of a monad, just as it is used here.

[mikeshulman]

I believe the history is that I suggested "purely" to mean what we are now calling "merely", but Dan, Bob, and Noam objected because of this, see their comments at: http://golem.ph.utexas.edu/category/2012/11/freedom_from_logic.html . It seemed natural then to use "purely" with the opposite meaning, once we settled on "merely" for the propositional truncation.

[mikeshulman]

Perhaps this paragraph would fit better in the notes to chapter 7, after having discussed general modalities in 7.7?

[awodey]

Who wrote it? It just seems a lot more detailed and technical than the issue warrants. It's just "no truncation" -- why drag in all the PL stuff?

Sent from my iPhone

On Apr 30, 2013, at 12:55 PM, Mike Shulman notifications@github.com wrote:

Perhaps this paragraph would fit better in the notes to chapter 7, after having discussed general modalities in 7.7?

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

[RobertHarper]

sometimes i think our biggest problems are with the choice of words for things! everything has a meaning to someone, and we all have attachments to words from our own experience, so it's hard to find consensus.

we seem to have settled on "merely" for the weaker form of truth (esp existence), but there doesn't seem to be much need for "purely" (or a synonym) in the development, is there? if it were me i'd say something like "truly exists" (as opposed to "merely exists"), but that most surely would not be popular, so i'm not proposing it.

bob

On Apr 30, 2013, at 12:54 PM, Mike Shulman wrote:

I believe the history is that I suggested "purely" to mean what we are now calling "merely", but Dan, Bob, and Noam objected because of this, see their comments at: http://golem.ph.utexas.edu/category/2012/11/freedom_from_logic.html . It seemed natural then to use "purely" with the opposite meaning, once we settled on "merely" for the propositional truncation.

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

[RobertHarper]

check the git log. i find it implausible that i made a comparison with haskell, but maybe i did when i was drunk or something.

bob

On Apr 30, 2013, at 1:08 PM, Steve Awodey wrote:

Who wrote it? It just seems a lot more detailed and technical than the issue warrants. It's just "no truncation" -- why drag in all the PL stuff?

Sent from my iPhone

On Apr 30, 2013, at 12:55 PM, Mike Shulman notifications@github.com wrote:

Perhaps this paragraph would fit better in the notes to chapter 7, after having discussed general modalities in 7.7?

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

[mikeshulman]

I wrote this paragraph. Certainly, "purely" is not used as much as "merely", but there are places where we want to emphasize that something exists untruncatedly. But I seem to have been the only one using it in this way, and I'm not especially attached to it, so we can get rid of it entirely if that's what everyone wants.

[RobertHarper]

personally, i don't mind either way.

bob

On Apr 30, 2013, at 1:26 PM, Mike Shulman wrote:

I wrote this paragraph. Certainly, "purely" is not used as much as "merely", but there are places where we want to emphasize that something exists untruncatedly. But I seem to have been the only one using it in this way, and I'm not especially attached to it, so we can get rid of it entirely if that's what everyone wants.

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

[awodey]

it's ok to have the word just to mean "not merely", but I wouldn't attach so much baggage to it.

On Apr 30, 2013, at 1:26 PM, Mike Shulman notifications@github.com wrote:

I wrote this paragraph. Certainly, "purely" is not used as much as "merely", but there are places where we want to emphasize that something exists untruncatedly. But I seem to have been the only one using it in this way, and I'm not especially attached to it, so we can get rid of it entirely if that's what everyone wants.

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

[mikeshulman]

This is the Notes section, not the main text, so I don't see any harm in explaining where the terminology comes from. On the other hand, there's a valid point that if a bit of terminology is used infrequently enough, then the reader will never remember what it means, so there's not much point to introducing it in the first place.

On Tue, Apr 30, 2013 at 12:28 PM, Steve Awodey notifications@github.comwrote:

it's ok to have the word just to mean "not merely", but I wouldn't attach so much baggage to it.

On Apr 30, 2013, at 1:26 PM, Mike Shulman notifications@github.com wrote:

I wrote this paragraph. Certainly, "purely" is not used as much as "merely", but there are places where we want to emphasize that something exists untruncatedly. But I seem to have been the only one using it in this way, and I'm not especially attached to it, so we can get rid of it entirely if that's what everyone wants.

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

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/179#issuecomment-17241651 .

[awodey]

On Apr 30, 2013, at 1:30 PM, Mike Shulman notifications@github.com wrote:

This is the Notes section, not the main text, so I don't see any harm in explaining where the terminology comes from.

fair enough

On the other hand, there's a valid point that if a bit of terminology is used infrequently enough, then the reader will never remember what it means, so there's not much point to introducing it in the first place.

I haven't checked to see how much it's used.

[mikeshulman]

Grep told me there are only a couple of uses anywhere (and rather more uses of the word "purely" in the ordinary English sense).

On Tue, Apr 30, 2013 at 12:33 PM, Steve Awodey notifications@github.comwrote:

On Apr 30, 2013, at 1:30 PM, Mike Shulman notifications@github.com wrote:

This is the Notes section, not the main text, so I don't see any harm in explaining where the terminology comes from.

fair enough

On the other hand, there's a valid point that if a bit of terminology is used infrequently enough, then the reader will never remember what it means, so there's not much point to introducing it in the first place.

I haven't checked to see how much it's used.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/179#issuecomment-17241925 .

[andrejbauer]

I think I used it a couple of times in the section of reals, and it came in really handy. I had to say something like "we might be tempted to require pure existence in the definition of X, but this would create problem Y". Without purely, I would have to write down the pure version of X, which seems like a lot of overhead for something I don't want to use. I am against getting rid of "purely". If we do, we will still have to agree how to say "not merely", and we will end up reinventing "purely", no?

Also, the stuff about monads and Haskell, while probably not strictly necessary, isn't doing any harm and will help some people understand what is going on. We've agree a long time ago that the main text is about informal mathematics (not logic, meta-theory, syntax, computational properties, CS or PL --- however important they actually are), but we can be a bit more relaxed in the notes, I think.

I am relabeling the issue as needs-talk.

[mikeshulman]

Have a look at 6f47319 and see what you think.

[dlicata335]

looks good to me

[awodey]

fine with me.

[mikeshulman]

I'm happy with this now, but anyone who wants to add more should feel free.