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