Dtyjlui

Having never had much exposure to formal mathematical logic, I have decided to embark on a quest to rectify this; unfortunately having been exposed to concepts from Intuitionistic Logic through my dabbles in functional programming, I find myself running into issues understanding "how it all fits together".

I am familiar with the notion of rejecting the law of the excluded middle (LEM); from the little I know of intuitionistic logic, I understand that this is done in the sense that LEM is not treated as an axiom within whatever deductive system is being used. However, looking at the treatments of propositional calculus within pretty much any text that I can lay my hands on, I find that after a discussion of the syntax of a zeroth-order logic, the author starts to talk about "semantics", in many cases illustrating this with truth tables.

At this point I run into an issue, because clearly the semantics presented for example in Goldrei (Propositional and Predicate Calculus: A Model of Argument) mean that LEM is a tautology.

When presenting "the semantics of propositional calculus", is the author in fact presenting a specific "logic" (i.e. classical logic), or are these semantics a fundamental part of of any propositional calculus? It seems to me that the latter cannot be true (as intuitionistic propositional logic definitely exists), but I cannot find an introductory text in which the author addresses this issue.

I am likely falling into the trap of a little knowledge being a dangerous thing and it's quite possible that everything I think I know about this is wrong, but I find myself currently unable to pass beyond this point without serious doubts as to what I'm reading actually refers to.

Truth table semantics is particular to classical propositional logic. So if the author were being specific, they would have added this qualifier. (However it’s probably a good rule of thumb that if you just see “propositional calculus,” in most contexts they are referring to classical.)

While “propositional” is a descriptor that mainly refers to the language (in particular, the absence of non logical symbols other than sentence letters), as soon as we start talking about proof systems or semantics, we have a particular logic in mind: classical, intuistionistic, minimal, modal, etc.

In classical propositional logic, a semantic interpretation can be more generally provided by a Boolean algebra, which is a set $X$ with constants $top, bot$, unary operation $lnot$, and binary operations $wedge, vee$ satisfying certain axioms. The prototypical Boolean algebra is ${ T, F }$ with the obvious interpretations.

In intuitionistic propositional logic, the corresponding construction is a Heyting algebra, which is a set $X$ with constants $top, bot$, and binary operations $wedge, vee, rightarrow$ satisfying certain axioms. Given a Heyting algebra, we can then often define $lnot x := (x rightarrow bot)$; however, in a general Heyting algebra, some of the Boolean algebra axioms or derived identities such as $x vee lnot x = top$, $lnot(lnot x) = x$, and $lnot(x wedge y) = (lnot x) vee (lnot y)$ no longer hold.

An interesting example of a Heyting algebra which is not a Boolean algebra is if $X$ is the set of open subsets of $mathbb{R}$, with $top := mathbb{R}$, $bot := emptyset$, $U wedge V := U cap V$, $U vee V := U cup V$, and $U rightarrow V := operatorname{int}((mathbb{R} setminus U) cup V)$. In this Heyting algebra, for example if we set $U := mathbb{R} setminus { 0 }$, then $lnot U = (U rightarrow emptyset) = operatorname{int}({ 0 }) = emptyset$, so $U vee lnot U = mathbb{R} setminus { 0 } neq top$, and $lnot (lnot U) = mathbb{R} ne U$. (Of course, there's nothing particular special about $mathbb{R}$ in this example: the same construction will work for the open subsets of any topological space.)

In case you're not comfortable with topology or real analysis, there's also a finite example that's often used: $X := { 0, frac{1}{2}, 1 }$; $top := 1$; $bot := 0$; $x vee y := max(x,y)$; $x wedge y := min(x,y)$; and $x rightarrow y$ is given by a table. In this Heyting algebra, $lnot(frac{1}{2}) = (frac{1}{2} rightarrow 0) = 0$, so $frac{1}{2} vee lnot(frac{1}{2}) = frac{1}{2} ne top$.

What author are you reading? The author may be referring to semantics in the context of category theory and type theory, where various notions of equality in type theory have the same structural property in category theory which are various notions of semantics.