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

]]>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$”?

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

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.

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

]]>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?

]]>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”.

]]>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.

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.

]]>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.

]]>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.

]]>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.

]]>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!

]]>