Within this sequence of posts I will outline a procedure for logical counterfactuals based on something similar to proof length. In this post I present a reimagining of propositional logic in which proving a theorem is taking a walk around a graph of equivalent proposititions.

Within this post, I will use Latin symbols, for specific symbols within proof strings. I will sometimes use symbols like $\forall$ to represent a function with particular properties.

I will use Greek letters to represent an arbitrary symbol, upper case for single symbols, lower case for strings.

Respecifying Propositional logic

The goal of this first section is to reformulate first order logic in a way that makes logical counterfactuals easier. Lets start with propositional logic.

We have a set of primitive propositions $p, q, r, . . .$ as well as the symbols $⊤, ⊥$ . We also have the symbols $\lor, \land$ which are technically functions from $B o o l^{2} \to B o o l$ but will be written $p \lor q$ not $\lor (p, q)$ . There is also $\neg : B o o l \to B o o l$

Consider the equivalence rules.

1. $α \equiv \neg \neg α$

2. $α \land β \equiv β \land α$

3. $(α \land β) \land γ \equiv α \land (β \land γ)$

4. $\neg α \land \neg β \equiv \neg (α \lor β)$

5. $α \land ⊤ \equiv α$

6. $\neg α \lor α \equiv ⊤$

7. $⊥ \equiv \neg ⊤$

8. $α \land (β \lor γ) \equiv (α \land β) \lor (α \land γ)$

9. $⊥ \land α \equiv ⊥$

$10. α \equiv α \land α$

Theorem

Any tautology provable in propositional logic can be created by starting at $⊤$ and repeatedly applying equivalence rules.

Proof

First consider $α ⟹ β$ to be shorthand for $\neg α \lor β$ .

Lemma

We can convert $⊤$ into any of the 3 axioms.

$α ⟹ (β ⟹ α)$ is a shorthand for

$\neg α \lor (\neg β \lor α) \equiv_{1}$

$\neg \neg (\neg α \lor (\neg β \lor α)) \equiv_{4}$

$\neg (\neg \neg α \land \neg (\neg β \lor α)) \equiv_{4}$

$\neg (\neg \neg α \land (\neg \neg β \land \neg α)) \equiv_{1}$

$\neg (\neg \neg α \land (β \land \neg α)) \equiv_{2}$

$\neg (\neg \neg α \land (\neg α \land β)) \equiv_{3}$

$\neg ((\neg \neg α \land \neg α) \land β) \equiv_{4}$

$\neg (\neg (\neg α \lor α) \land β) \equiv_{6}$

$\neg (\neg ⊤ \land β) \equiv_{7}$

$\neg (⊥ \land β) \equiv_{9}$

$\neg ⊥ \equiv_{7}$

$⊤$

Similarly

$(α ⟹ (β ⟹ γ)) ⟹ ((α ⟹ β) ⟹ (α ⟹ γ))$

$(\neg α ⟹ \neg β) ⟹ (β ⟹ α)$

(if these can't be proved, add that they $\equiv ⊤$ as axioms)

End Lemma

Whenever you have $α \land (α ⟹ β)$ , that is equiv to

$α \land (\neg α \lor β) \equiv_{8}$

$(α \land \neg α) \lor (α \land β) \equiv_{1}$

$(\neg \neg α \land \neg α) \lor (α \land β) \equiv_{4}$

$\neg (\neg α \lor α) \lor (α \land β) \equiv_{6}$

$\neg ⊤ \lor (α \land β) \equiv_{1}$

$\neg \neg (\neg ⊤ \lor (α \land β)) \equiv_{4}$

$\neg (\neg \neg ⊤ \land \neg (α \land β)) \equiv_{1}$

$\neg (⊤ \land \neg (α \land β)) \equiv_{2}$

$\neg (\neg (α \land β) \land ⊤) \equiv_{5}$

$\neg \neg (α \land β) \equiv_{1}$

$α \land β$

This means that you can create and apply axioms. For any tautology, look at the proof of it in standard propositional logic. Call the statements in this proof $p_{1}, p_{2}, p_{3} . . .$

suppose we have already found a sequence of substitutions from $⊤$ to $p_{1} \land p_{2} . . . \land p_{i - 1}$

Whenever $p_{i}$ is a new axiom, use (5.) to get $p_{1} \land p_{2} . . . \land p_{i - 1} \land ⊤$ , then convert $⊤$ into the instance of the axiom you want. (substitute alpha and beta with arbitrary props in above proof schema)

Using substitution rules (2.) and (3.) you can rearrange the terms representing lines in the proof and ignore their bracketing.

Whenever $p_{i}$ is produced by modus ponus from the previous $p_{j}$ and $p_{k} = p_{j} ⟹ p_{i}$ then duplicate $p_{k}$ with rule (10.), move one copy next to $p_{j}$ and use the previous procedure to turn $p_{j} \land (p_{j} ⟹ p_{i})$ into $p_{j} \land p_{i}$ . Then move $p_{i}$ to end.

Once you reach the end of the proof, duplicate the result and unwind all the working back to $⊤$ , which can be removed by rule (5.)

Corollary

${p, q, r} ⊢ s$ then $p \land q \land r \equiv p \land q \land r \land s$

Because $p \land q \land r ⟹ s$ is a tautology and can be applied to get $s$ .

Corollary

Any contradiction is reachable from $⊥$

The negation of any contradiction $k$ is a tautology.

$⊥ \equiv \neg ⊤ \equiv \neg \neg k \equiv k$

Intuitive overview perspective 1

An illustration of rule 4. $\neg α \land \neg β \equiv \neg (α \lor β)$ in action.

We can consider a proposition to be a tree with a root. The nodes are labeled with symbols. The axiomatic equivalences become local modifications to the tree structure, which are also capable of duplicating and merging identical subtrees by (10.). Arbitrary subtrees can be created or deleted by (5.).

We can merge nodes with identical subtrees into a single node. This produces a directed acyclic graph, as shown above. Under this interpretation, all we have to do is test node identity.

Intuitive overview perspective 2

Consider each possible expression to be a single node within an infinite graph.

Each axiomatic equivalence above describes an infinite set of edges. To get a single edge, substitute the generic $α, β . . .$ with a particular expression. For example, if you take (2. $α \land β \equiv β \land α$ ) and substitute $α := p \lor q$ and $β := \neg q$ . We find a link between the node $(p \lor q) \land \neg q$ and $\neg q \land (p \lor q)$ .

Here is a connected subsection of the graph. Note that, unlike the previous graph, this one is cyclic and edges are not directed.

All statements that are provably equivalent in propositional logic will be within the same connected component of the graph. All statements that can't be proved equivalent are in different components, with no path between them.

Finding a mathematical proof becomes an exercise in navigating an infinite maze.

In the next Post

We will see how to extend the equivalence based proof system to an arbitrary first order theory. We will see what the connectedness does then. We might even get on to infinite dimensional vector spaces and why any of this relates to logical counterfactual.