Crossposted from the AI Alignment Forum. May contain more technical jargon than usual.

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 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 as well as the symbols . We also have the symbols which are technically functions from but will be written not . There is also

Consider the equivalence rules.











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


First consider to be shorthand for .


We can convert into any of the 3 axioms.

is a shorthand for


(if these can't be proved, add that they as axioms)

End Lemma

Whenever you have , that is equiv to

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

suppose we have already found a sequence of substitutions from to

Whenever is a new axiom, use (5.) to get , 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 is produced by modus ponus from the previous and then duplicate with rule (10.), move one copy next to and use the previous procedure to turn into . Then move 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.)



Because is a tautology and can be applied to get .


Any contradiction is reachable from

The negation of any contradiction is a tautology.

Intuitive overview perspective 1

An illustration of rule 4. 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. ) and substitute and . We find a link between the node and .

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.


Ω 8

New Comment