Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeMay 2nd 2017
• (edited May 2nd 2017)

I have a request to the logic experts:

The entry classical logic is a bit thin. I would like to be able to point to it so that readers who don’t already know about it all, get away with a decent idea of what is meant. Might somebody have the energy to add a few lines?

Of course I could add a few lines myself, but I imagine it would be more efficient if some expert here did it from scratch, instead of having to improve on what I would come up with.

Especially it would be nice if the following keywords were at least mentioned and maybe briefly commented on in the entry:

Also for instance the keyword constructive anything is presently missing from the entry.

Thanks!

• CommentRowNumber2.
• CommentAuthorTodd_Trimble
• CommentTimeMay 2nd 2017

It’s not a bad start, but the bit about linear logic having distributivity looks a little off since one side of the distributivity equation involves a repetition of variables. I suppose some fancier form of distributivity involving the modal operator $!$ might be asserted, but anyway something needs fixing there.

This I find a fairly tricky article to just start editing right away; it would require thought and planning.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeMay 2nd 2017
• (edited May 2nd 2017)

I should clarify that I am not after a decent technical discussion that would do justice to the topic of classical logic (though that would of course be nice to have, too). Rather I am after providing a decent Idea of the subject to readers who are not yet experts in logic. I bet that a reader who already knows that “lattice” is a concept in logic is in little need of looking up what is meant by “classical logic”.

So I went ahead and gave the entry an informal Idea section. Please feel invited to edit.

• CommentRowNumber4.
• CommentAuthorTodd_Trimble
• CommentTimeMay 2nd 2017

It looks like we were editing at the same time, then. (How does that happen?) I tried my hand at it as well. I think it’s fairly non-technical, but others should judge that.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeMay 2nd 2017

Thanks for adding material, Todd! I suppose the edit block times out after a while. I have pasted my Idea-section back in now. Please check it out to see if it is okay.

• CommentRowNumber6.
• CommentAuthorMike Shulman
• CommentTimeMay 2nd 2017

In linear logic the multiplicative conjunction $\otimes$ distributes over the additive disjunction $\oplus$. The additivity of $\oplus$ is what allows the duplication of variables. Altogether the structure is not, so far as I know, a distributive lattice: the additive conjunction $\&$ and disjunction $\oplus$ do form a lattice structure, but as far as I know they do not distribute (I think getting them to distribute is one of the points of bunched implication), while the multiplicative conjunction is a quantale structure rather than a lattice one.

• CommentRowNumber7.
• CommentAuthorMike Shulman
• CommentTimeMay 3rd 2017

I corrected the statement about linear logic (by waffling), and added a bit here and there. Overall the introduction looks good. Is it really quite correct to identify classical logic with Aristotelian logic, though? I’m sure Aristotle believed in LEM, but my impression was that his logic was otherwise not as powerful as modern propositional/predicate logic, and it’s the latter that we usually mean by “classical logic”.

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeMay 3rd 2017
• (edited May 3rd 2017)

Is it really quite correct to identify classical logic with Aristotelian logic, though?

Right, it should not point to “Aristotlean logic”, just to “Aristotle”, I have changed it. I suppose he is credited for stating excluded middle?

• CommentRowNumber9.
• CommentAuthorDavid_Corfield
• CommentTimeMay 3rd 2017

“Of any one subject, one thing must be either asserted or denied” (Aristotle, Metaphysics 1011b24)

• CommentRowNumber10.
• CommentAuthorTodd_Trimble
• CommentTimeMay 3rd 2017
• (edited May 3rd 2017)

I already made a slight amendment at proof by contradiction about this without announcing it before now, but since it comes up at classical logic as well: I’m not very keen on stating the principle of excluded middle as saying every proposition is either true or false. This seems subject to misunderstanding: you wouldn’t say the continuum hypothesis is either true or false, unless you meant something that refers to individual models. But PEM has an internal and elementary formulation that doesn’t depend on models and semantics and completeness, and which might as well be stated up front: for any proposition $P$, we have $\top = P \vee \neg P$. (Sophisticated readers will probably understand that the statement was actually meant to be interpreted ’internally’, but such understandings are probably not common to those readers who need to read the Idea section.)

I went ahead and made the amendment at classical logic as well. I might touch up principle of excluded middle as well, although it has some sophisticated discussion about internal/external in the Idea section (one which might make some readers nervous because of its sophistication).

BTW: it seems to me that the way most nLab Idea sections are written, symbolism is eschewed. But I’ve never seen any sort of policy about that made explicit.

• CommentRowNumber11.
• CommentAuthorUrs
• CommentTimeMay 3rd 2017
• (edited May 3rd 2017)

David, thanks! I have added pointer to Aristotle’s Metaphysics at excluded middle and also from “classical logic”.

• CommentRowNumber12.
• CommentAuthorMike Shulman
• CommentTimeMay 3rd 2017

Todd, I think I see your point, but why the “$\top=$”? Can’t we just say “for any $P$, we have $P\vee\neg P$”?

• CommentRowNumber13.
• CommentAuthorTodd_Trimble
• CommentTimeMay 3rd 2017

I was thinking algebraically (i.e., in a Boolean algebra), but yes I’d be happy with that as well.