What Tarski-Lindenbaum algebra is associated with Angell's four-valued logic?

55 Views Asked by At

This talk by Hitoshi Omori on connexive logic, at around 11:50 shows the truth table for a four-valued logic created by Richard Angell to support a proof system called PA1. (I think. I'm guessing the proof system is PA1 based on the contents of this article https://plato.stanford.edu/entries/logic-connexive/).

This logic appears to have a Lindenbaum-Tarski algebra. Which algebraic structure is it? I'm having trouble identifying it because it's very un-latticelike.


First a word on notation, for the truth values I will use $T, F, N, 2$ where $2$ is both true and false. I'm doing this because I find lowercase $t$ and $f$ visually similar in some fonts and I want to use both $B$ and $b$ for other purposes.

For convenience, here is the truth table for this logic. I'm only taking the symbols from the top row at 11:50. The other connectives are additions from FDE.

    ¬      ∧  T 2 N F     → T 2 N F
T | F      T| T 2 N F     T| T F N F
2 | N      2| 2 T F N     2| F T F N
N | 2      N| N F N F     N| T F T F
F | T      F| F N F N     F| F T F T

So, the first thing to notice is the nice checkerboard pattern. This comes from the fact that $T2NF$ is alternating when we consider just the falsity conditions and $A@B$ is non-false exactly when $A$ and $B$ have the same falsity, where $@$ is $\to$ or $\land$.

Here are the truth and falsity conditions for all the connectives.

$A \to B$ is true iff ($A$ is not true or $B$ is true) and (A is false iff B is false).

$A \to B$ is false iff it is not the case that $A$ is false iff $B$ is false.

$A \land B$ is true iff $A$ is true and $B$ is true.

$A \land B$ is false iff it is not the case that $A$ is false iff $B$ is false.

$\lnot A$ is true iff $A$ is not false.

$\lnot A$ is false iff $A$ is not true.

Let's fix a set of propositional variables $\mathcal{V}$ in the background so we're just talking about one algebraic structure.

I'm also going to just assume that the consequence relation $\Gamma \vdash \varphi$ for Angell's logic is classical. I don't think I need this assumption to talk about $\equiv$ though. Also, my designated truth values are $T$ and $2$. A truth value is designated if and only if it is true (not necessarily true simpliciter).

So, $\vdash \varphi \to \psi$ and $\vdash \psi \to \varphi$ (i.e. $\varphi \equiv \psi$) both hold iff $\varphi$ and $\psi$ have the same truth values for all valuations. We get this because the truth conditions of $\to$ take into account both the truth and falsity conditions of both arguments.

Based on that fact, and the fact that we have a matrix semantics for this logic, I think $\equiv$ is a congruence for this logic.

In a certain sense, I think this fact is enough to give me an algebraic structure $\mathcal{A}$, the Lindenbaum-Tarski algebra associated with this logic.

I'm not sure which structure this is, though. It doesn't satisfy $a \land a \approx a$ so it's not a lattice, but it does satisfy some other properties. (I might be able to make it friendlier by introducing a new connective $a \& b =\!=_\text{def} a \land (b \land b)$, which ignores the falsity of the right argument).

I don't think these properties are complete and they don't collectively pin down $\mathcal{A}$.

$$ a \land a \land a \approx a $$ $$ a \approx \lnot \lnot a $$ $$ a \to \lnot a \approx F $$ $$ a \to a \approx T $$ $$ a \land b \approx b \land a $$ $$ a \land (b \land c) \approx (a \land b) \land c $$ $$ a \land \lnot a \approx F $$

I'm sort of stuck as to where to go from here. How do I figure out what kind of algebraic structure I have?