Contents

• Respecifying Propositional logic
• Theorem
• Proof
• Lemma
• End Lemma
• Corollary
• Corollary
• Intuitive overview perspective 1
• Intuitive overview perspective 2
• In the next Post 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 \top,\bot. We also have the symbols \vee,\wedge which are technically functions from Bool^2\rightarrow Bool but will be written p\vee q not \vee(p,q) . There is also \neg:Bool \rightarrow Bool Consider the equivalence rules.

1. \alpha \equiv \neg\neg\alpha
2. \alpha \wedge \beta \equiv \beta \wedge \alpha
3. (\alpha \wedge \beta) \wedge \gamma \equiv\alpha \wedge (\beta \wedge \gamma)
4. \neg \alpha \wedge \neg \beta\equiv \neg(\alpha\vee\beta)
5. \alpha \wedge \top \equiv \alpha
6. \neg\alpha\vee \alpha\equiv \top
7. \bot\equiv \neg \top
8. \alpha \wedge (\beta \vee \gamma)\equiv (\alpha \wedge \beta)\vee(\alpha \wedge \gamma)
9. \bot\wedge\alpha\equiv \bot 10.\alpha\equiv\alpha\wedge\alpha

Theorem

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

Proof

First consider \alpha \implies \beta to be shorthand for \neg \alpha \vee \beta.

Lemma

We can convert \top into any of the 3 axioms. \alpha\implies(\beta\implies\alpha) is a shorthand for \neg \alpha \vee (\neg \beta \vee \alpha)\equiv_1 \neg\neg(\neg \alpha \vee (\neg \beta \vee \alpha))\equiv_4 \neg(\neg\neg \alpha \wedge \neg(\neg \beta \vee \alpha))\equiv_4 \neg(\neg\neg \alpha \wedge (\neg\neg \beta \wedge \neg\alpha))\equiv_1 \neg(\neg\neg \alpha \wedge (\beta \wedge \neg\alpha))\equiv_2 \neg( \neg\neg\alpha \wedge (\neg\alpha \wedge\beta ))\equiv_3 \neg(( \neg\neg\alpha \wedge \neg\alpha) \wedge\beta )\equiv_4 \neg(\neg( \neg\alpha \vee \alpha) \wedge\beta )\equiv_6 \neg(\neg\top \wedge\beta )\equiv_7 \ \neg(\bot \wedge\beta )\equiv_9 \neg \bot\equiv_7 \top Similarly (\alpha\implies (\beta\implies\gamma))\implies ((\alpha\implies\beta)\implies(\alpha\implies\gamma)) (\neg\alpha\implies\neg\beta)\implies(\beta\implies\alpha) (if these can’t be proved, add that they \equiv\top as axioms)

End Lemma

Whenever you have \alpha\wedge(\alpha\implies \beta), that is equiv to \alpha\wedge(\neg\alpha\vee \beta)\equiv_8 (\alpha\wedge\neg\alpha)\vee(\alpha\wedge \beta)\equiv_1 (\neg\neg\alpha\wedge\neg\alpha)\vee(\alpha\wedge \beta)\equiv_4 \neg(\neg\alpha\vee\alpha)\vee(\alpha\wedge \beta)\equiv_6 \neg\top\vee(\alpha\wedge \beta)\equiv_1 \neg\neg(\neg\top\vee(\alpha\wedge \beta))\equiv_4 \neg(\neg\neg\top\wedge\neg(\alpha\wedge \beta))\equiv_1 \neg(\top\wedge\neg(\alpha\wedge \beta))\equiv_2 \neg(\neg(\alpha\wedge \beta)\wedge\top)\equiv_5 \neg\neg(\alpha\wedge \beta)\equiv_1 \alpha\wedge \beta 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 \top to p_1\wedge p_2 ...\wedge p_{i-1} Whenever p_i is a new axiom, use (5.) to get p_1\wedge p_2 ...\wedge p_{i-1}\wedge \top, then convert \top 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\implies 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\wedge(p_j\implies p_i) into p_j\wedge 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 \top, which can be removed by rule (5.)

Corollary

{p,q,r}\vdash s then p\wedge q\wedge r\equiv p\wedge q\wedge r\wedge s Because p\wedge q\wedge r \implies s is a tautology and can be applied to get s.

Corollary

Any contradiction is reachable from \bot The negation of any contradiction k is a tautology. \bot\equiv\neg\top\equiv\neg\neg k\equiv k

Intuitive overview perspective 1

An illustration of rule 4. \neg \alpha \wedge \neg \beta\equiv \neg(\alpha\vee\beta) 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 \alpha,\beta... with a particular expression. For example, if you take (2. \alpha \wedge \beta \equiv \beta \wedge \alpha ) and substitute \alpha := p\vee q and \beta:=\neg q. We find a link between the node (p\vee q)\wedge \neg q and \neg q\wedge(p\vee 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.