You are currently browsing the tag archive for the ‘propositional logic’ tag.

In our last installment in this series on Stone duality, we introduced the notion of Heyting algebra, which captures the basic relationships between the logical connectives “and”, “or”, and “implies”. Our discussion disclosed a fundamental relationship between distributive laws and the algebra of implication, which we put to work to discover the structure of the “internal Heyting algebra logic” of a topology.

I’d like to pause and reflect on the general technique we used to establish this relationship; like the Yoneda principle and the Principle of Duality, it comes up with striking frequency, and so it will be useful for us to give it a name. As it turns out, this particular proof technique is analogous to the way adjoints are used in linear algebra. Such analogies go all the way back to work of C. S. Peirce, who like Boole was a great pioneer in the discovery of relationships between algebra and logic. At a deeper level, similar analogies were later rediscovered in category theory, and are connected with some of the most potent ideas category theory has to offer.

Our proof that meets distribute over sups in the presence of an implication operator is an example of this technique. Here is another example of similar flavor.

Theorem: In a Heyting algebra $X$, the operator $p \Rightarrow -: X \to X$ preserves any infs which happen to exist in $X$, for any element $p \in X$. [In particular, this operator is a morphism of meet-semilattices, i.e., $(p \Rightarrow (q \wedge r)) = ((p \Rightarrow q) \wedge (p \Rightarrow r))$, and $(p \Rightarrow 1) = 1$.]

Proof: Suppose that $S \subseteq X$ has an inf, which here will be denoted $\bigwedge_{s \in S} s$. Then for all $a \in X$, we have

$a \leq p \Rightarrow (\bigwedge_{s \in S} s)$ if and only if

$a \wedge p \leq \bigwedge_{s \in S} s$ if and only if

(for all $s \in S$, $a \wedge p \leq s$) if and only if

for all $s \in S$, $a \leq p \Rightarrow s$.

By the defining property of inf, these logical equivalences show that $p \Rightarrow (\bigwedge_{s \in S} s)$ is indeed the inf of the subset $\{p \Rightarrow s: s \in S\}$, or in other words that $p \Rightarrow (\bigwedge_{s \in S} s) = \bigwedge_{s \in S} p \Rightarrow s$, as desired. $\Box \,$

In summary, what we did in this proof is “slide” the operator $p \Rightarrow -$ on the right of the inequality over to the operator $- \wedge p$ on the left, then invoke the defining property of infs, and then slide back to $p \Rightarrow -$ on the right. This sliding trick is analogous to how adjoint mappings work in linear algebra.

In fact, everything we have done so far with posets can be translated in terms of matrix algebra, provided that our matrix entries, instead of being real or complex numbers, are truth values $0, 1$ ($1$ for “true”, $0 \mbox{ for}$ “false”). These truth values are added and multiplied in the way familiar from truth tables, with join playing the role of addition and meet playing the role of multiplication. In fact the lattice $\mathbf{2} = \{0, 1\}$ is a very simple distributive lattice, and so most of the familiar arithmetic properties of addition and multiplication (associativity, commutativity, distributivity) do carry over, which is all we need to carry out the most basic aspects of matrix algebra. However, observe that $1$ has no additive inverse (for here $1 + 1 = 1 \vee 1 = 1$) — the type of structure we are dealing with is often called a “rig” (like a ring, but without assuming negatives). On the other hand, this lattice is, conveniently, a sup-lattice, thinking of sups as arbitrary sums, whether finitary or infinitary.

Peirce recognized that a relation can be classified by a truth-valued matrix. Take for example a binary relation on a set $X$, i.e., a subset $R \subseteq X \times X$. We can imagine each point $(x, y) \in X \times X$ as a pixel in the plane, and highlight $R$ by lighting up just those pixels which belong to $R$. This is the same as giving an $(X \times X)$-matrix $R(\cdot, \cdot)$, with rows indexed by elements $y$ and columns by elements $x$, where the $(y, x)$-entry $R(y, x)$ is $1$ (on) if $(x, y)$ is in $R$, and $0 \mbox{ (off)}$ if not. In a similar way, any relation $R \subseteq X \times Y$ is classified by a $(Y \times X)$-matrix whose entries are truth values.

As an example, the identity matrix has a $1$ at the $(x, y)$-entry if and only if $x = y$. Thus the identity matrix classifies the equality relation.

A poset is a set $X$ equipped with a binary relation $R$ satisfying the reflexive, transitive, and antisymmetry properties. Let us translate these into matrix algebra terms. First reflexivity: it says that $x = y$ implies $(x, y) \in R$. In matrix algebra terms, it says $Id(y, x) \leq R(y, x)$, which we abbreviate in the customary way:

(Reflexivity) $Id \leq R$.

Now let’s look at transitivity. It says

($\exists_y (x, y) \in R$ and $(y, z) \in R$) implies $(x, z) \in R$.

The “and” here refers to the meet or multiplication in the rig of truth values $\mathbf{2}$, and the existential quantifier can be thought of as a (possibly infinitary) join or sum indexed over elements $y$. Thus, for each pair $(x, z)$, the hypothesis of the implication has truth value

$\sum_y R(z, y) \cdot R(y, x)$

which is just the $(z, x)$-entry of the square of the matrix $R$. Therefore, transitivity can be very succinctly expressed in matrix algebra terms as the condition

(Transitivity) $R^2 \leq R$.

• Remark: More generally, given a relation $R \subseteq X \times Y$ from $X$ to $Y$, and another relation $S \subseteq Y \times Z$ from $Y$ to $Z$, the relational composite $S \circ R \subseteq X \times Z$ is defined to be the set of pairs $(x, z)$ for which there exists $y$ with $(x, y) \in R$ and $(y, z) \in S$. But this just means that its classifying matrix is the ordinary matrix product $S \cdot R$!

Let’s now look at the antisymmetry condition: ($(x, y) \in R$ and $(y, x) \in R$) implies $x = y$. The clause $(y, x) \in R$ is the flip of $(x, y) \in R$; at the matrix level, this flip corresponds to taking the transpose. Thus antisymmetry can be expressed in matrix terms as

(Antisymmetry) $R \wedge R^\top \leq Id$

where $R^\top$ denotes the transpose of $R$, and the matrix meet $\wedge$ means we take the meet at each entry.

• Remark: From the matrix algebra perspective, the antisymmetry axiom is less well motivated than the reflexivity and transitivity axioms. There’s a moral hiding beneath that story: from the category-theoretic perspective, the antisymmetry axiom is relatively insignificant. That is, if we view a poset as a category, then the antisymmetry condition is tantamount to the condition that isomorphic objects are equal (in the parlance, one says the category is “skeletal”) — this extra condition makes no essential difference, because isomorphic objects are essentially the same anyway. So: if we were to simply drop the antisymmetry axiom but keep the reflexivity and transitivity axioms (leading to what are called preordered sets, as opposed to partially ordered sets), then the theory of preordered sets develops exactly as the theory of partially ordered sets, except that in places where we conclude “$x$ is equal to $y$” in the theory of posets, we would generally conclude “$x$ is isomorphic to $y$” in the theory of preordered sets.

Preordered sets do occur in nature. For example, the set of sentences $p, q, ...$ in a theory is preordered by the entailment relation $p \vdash q$ ($q$ is derivable from $p$ in the theory). (The way one gets a poset out of this is to pass to a quotient set, by identifying sentences which are logically equivalent in the theory.)

Exercises:

1. (For those who know some topology) Suppose $X$ is a topological space. Given $x, y \in X$, define $x \leq y$ if $x$ belongs to the closure of $y$; show this is a preorder. Show this preorder is a poset precisely when $X$ is a $T_0$-space.
2. If $X$ carries a group structure, define $x \leq y$ for elements $x, y \in X$ if $x = y^n$ for some integer $n$; show this is a preorder. When is it a poset?

Since posets or preorders are fundamental to everything we’re doing, I’m going to reserve a special pairing notation for their classifying matrices: define

$\langle x, y \rangle = 1$ if and only if $x \leq y$.

Many of the concepts we have developed so far for posets can be succinctly expressed in terms of the pairing.

Example: The Yoneda principle (together with its dual) is simply the statement that if $X$ is a poset, then $x = y$ if and only if $\langle -, x \rangle = \langle -, y \rangle$ (as functionals valued in $\mathbf{2}$) if and only if $\langle x, - \rangle = \langle y, - \rangle$.

Example: A mapping from a poset $(X, \langle, \rangle_X)$ to a poset $(Y, \langle, \rangle_Y)$ is a function $f: X \to Y$ such that $\langle x, y \rangle_X \leq \langle f(x), f(y) \rangle_Y$.

Example: If $X$ is a poset, its dual or opposite $X^{op}$ has the same elements but the opposite order, i.e., $\langle x, y \rangle_X = \langle y, x \rangle_{X^{op}}$. The principle of duality says that the opposite of a poset is a poset. This can be (re)proved by invoking formal properties of matrix transpose, e.g., if $R^2 \leq R$, then $(R^\top)^2 = (R^2)^\top \leq R^\top$.

By far the most significant concept that can be expressed in terms of these pairings that of adjoint mappings:

Definition: Let $X, Y$ be posets [or preorders], and $f: X \to Y$, $g: Y \to X$ be poset mappings. We say $(f, g)$ is an adjoint pair (with $f$ the left adjoint of $g$, and $g$ the right adjoint of $f$) if

$\langle f(x), y \rangle_Y = \langle x, g(y) \rangle_X$

or, in other words, if $f(x) \leq y$ if and only if $x \leq g(y)$. We write $f \dashv g$. Notice that the concept of left adjoint is dual to the concept of right adjoint (N.B.: they are not the same, because clearly the pairing $\langle x, y \rangle$ is not generally symmetric in $x$ and $y$).

Here are some examples which illustrate the ubiquity of this concept:

1. Let $X$ be a poset. Let $X \times X$ be the poset where $(x, y) \leq (x', y')$ iff ($x \leq x'$ and $y \leq y'$). There is an obvious poset mapping $\delta: X \to X \times X$, the diagonal mapping, which takes $x$ to $(x, x)$. Then a meet operation $\wedge: X \times X \to X$ is precisely a right adjoint to the diagonal mapping. Indeed, it says that $(a, a) \leq (x, y)$ if and only if $a \leq x \wedge y$.
2. Dually, a join operation $\vee: X \times X \to X$ is precisely a left adjoint to the diagonal mapping $\delta: X \to X \times X$.
3. More generally, for any set $S$, there is a diagonal map $\Delta: X \to X^S$ which maps $x \in X$ to the $S$-tuple $(\ldots, x, x, x, \ldots)$. Its right adjoint $X^S \to X$, if one exists, sends an $S$-tuple $(x_s)_{s \in S}$ to the inf of the set $\{x_s: s \in S\}$. Its left adjoint would send the tuple to the sup of that set.
4. If $X$ is a Heyting algebra, then for each $x \in X$, the conjunction operator $x \wedge -: X \to X$ is left adjoint to the implication operator $x \Rightarrow -: X \to X$.
5. If $X$ is a sup-lattice, then the operator $\sup: PX \to X$ which sends a subset $S \subseteq X$ to $\sup(S) \in X$ is left adjoint to the Dedekind embedding $i: X \to PX$. Indeed, we have $\sup(S) \leq a$ if and only if (for all $s \in S, s \leq a$) if and only if $S \subseteq \{x \in X: x \leq a\} = i(a)$.

As items 1, 2, and 4 indicate, the rules for how the propositional connectives $\wedge, \vee, \Rightarrow$ operate are governed by adjoint pairs. This gives some evidence for Lawvere’s great insight that all rules of inference in logic are expressed by interlocking pairs of adjoint mappings.

Proposition: If $f \dashv g$ and $f' \dashv g'$ where $g: X \to Y$ and $g': Y \to Z$ are composable mappings, then $f \circ f' \dashv g' \circ g$.

Proof: $\langle f f' z, x \rangle_X = \langle f' z, g x \rangle_Y = \langle z, g' g x \rangle_Z$. Notice that the statement is analogous to the usual rule $(A B)^\dagger = B^\dagger A^\dagger$, where $A^\dagger$ refers to taking an adjoint with respect to given inner product forms.

We can use this proposition to give slick proofs of some results we’ve seen. For example, to prove that Heyting algebras are distributive lattices, i.e., that $p \wedge (x \vee y) = (p \wedge x) \vee (p \wedge y)$, just take left adjoints on both sides of the tautology $\delta \circ g = (g \times g) \circ \delta$, where $g = p \Rightarrow -$ is right adjoint to $p \wedge -$. The left adjoint of the left side of the tautology is (by the proposition) $p \wedge -$ applied to $\vee$. The left adjoint of the right side is $\vee$ applied to $(p \wedge -) \times (p \wedge -)$. The conclusion follows.

Much more generally, we have the

Theorem: Right adjoints $g: X \to Y$ preserve any infs which exist in $X$. Dually, left adjoints $f: Y \to X$ preserve any sups which exist in $Y$.

Proof: $\langle y, g(\bigwedge_{s \in S} x_s) \rangle_Y = \langle f(y), \bigwedge_{s \in S} x_s \rangle_X = \bigwedge_{s \in S} \langle f(y), x_s \rangle_X$ where the last inf is interpreted in the inf-lattice $\mathbf{2}$. This equals $\bigwedge_{s \in S} \langle y, g(x_s) \rangle_Y$. This completes the proof of the first statement (why?). The second follows from duality.

Exercise: If $X$ is a Heyting algebra, then there is a poset mapping $- \Rightarrow c: X^{op} \to X$ for any element $c$. Describe the left adjoint of this mapping. Conclude that this mapping takes infs in $X^{op}$ (i.e., sups in $X$) to the corresponding infs in $X$.

Let’s see if we can build this from ground up. We first define a statement (or sometimes, a proposition) to be a meaningful assertion that is either true or false. Well, meaningful means we should be able to say for sure if a statement is true or false. So, something like “Hello, there!” is not counted as a statement but “the sun is made of butter” is. The latter is evidently false but the former is neither true nor false. Now, it can get quite cumbersome after a while if we keep using statements such as “the sun is made of butter” every time we need to use them. Thus, it is useful to have variables, or to be precise, propositional variables, to denote all statements. We usually prefer to use $p, q, r$ and so on for such variables.

Now, all of this would be rather boring if we had just symbols such as $p, q, r$ etc. to denote statements. Thus, a statement like “Archimedes was a philosopher” is not that interesting in itself. In fact, all the statements (in our formal system) would be “isolated” ones in the sense that we wouldn’t be able to logically “connect” one statement to another. We want to be able to express sentences like “$x = -2$ and $y=2$“, “$(x = -2)$ implies $(x^2 = 4)$” and so on. So, we add something called logical connectives (also called operator symbols) to the picture. There are four basic ones: $\wedge$ (conjunction), $\vee$ (disjunction), $\rightarrow$ (material implication), which are all of arity 2 and $\neg$ (negation) which is of arity 1. Using these logical connectives, we can now form compound statements such as $p \wedge q$ (i.e. $p$ and $q$), $p \vee q$ (i.e. $p$ or $q$), $\neg p$ (i.e. $\mbox{not} (p)$), and $p \rightarrow q$ (i.e. $p$ implies $q$.) Note that each of $\wedge, \vee$ and $\rightarrow$ requires two propositional variables in order for it to make any sense; this is expressed by saying their arity is 2. On the other hand, $\neg$ has arity 1 since it is applied to exactly one propositional variable.

We also introduce another logical operator called logical equivalence ($\equiv$,) which has arity 2. It is really convenient to have logical equivalence on hand, as we shall see later. We say $p \equiv q$ if and only if “$(p \rightarrow q) \mbox{ and } (q \rightarrow p)$“. What this basically means is, if $p$ is true then so is $q$ and if $q$ is true then so is $p$. Another equivalent way of saying this is, if $p$ is true then so is $q$ and if $p$ is false then so is $q$.

Before we proceed further, we make a few observations. First, if $p$ and $q$ are propositional variables, then by definition each of those is either true or false. Formally speaking, the truth value of $p$ or $q$ is either true or false. This is equally true of the compound statements $p \wedge q,\, p \vee q,\, p \rightarrow q$ and $\neg p$. Of course, the truth values of these four compound statements depend on $p$ and $q$. We will delve into this in the next post.

Second, we don’t really need all the four basic operators. Two of those, viz. $\rightarrow$ and $\neg$ suffice for all logical purposes. This means all statements involving $\wedge$ and/or $\vee$ can be “converted” to ones that involve only $\rightarrow$ and $\neg$. However, we can also choose the “minimal” set $\{ \wedge, \,\neg \}$, instead, for the purpose for which we chose the minimal set $\{ \rightarrow, \neg \}$. In fact, there are lots of other possible combinations of operators that can serve our purpose equally well. Which minimal set of operators we choose depends sometimes on personal taste and at other times on practical considerations. So, for example, while designing circuits in the field of computer hardware, the minimal operator set that is used is $\{ \downarrow \}$. In fact, all that’s really needed is this particular operator set. Here $p \downarrow q \equiv \neg (p \wedge q)$.

So, what have we got so far? Well, we have a formal notion of a statement (or proposition.) We have access to propositional variables ($p, \, q, \, r$, etc.) that may be used to denote statements. We know how to create the negation of a given statement using the $\neg$ logical connective. We also know how to “connect” any two statements using conjunction, disjunction and material implication that are symbolically represented by the logical connectives $\wedge, \, \vee$ and $\rightarrow$, respectively. And, lastly, given any two statements $p$ and $q$, we have defined what it means for the two to be logically equivalent (which is symbolically represented by $\equiv$) to each other. Indeed, $p \equiv q$ if and only if ($p \rightarrow q \mbox{ and } q \to p$).

We shall see in the later posts that the above “small” formal system (for propositional calculus) we have built thus far is, in fact, quite powerful. We can, indeed, already employ quite a bit of it in “ordinary” mathematics. But, more on this, later!

• 340,184 hits