If you haven't read part 1, read it here.

In this post we extend the notion of propositional graphs to cover any first order theory.

Consider some arbitrary first order theory. For example a theory of integers.

We can consider the program to deal with two basic types. $B=\{\top ,\perp \}$ and $N=\{0,1,2,...\}$. All the functions and transformation rules in the previous post apply to $B$. For example, $\top$ is of type $B$. $\wedge$ is a function from $B^2\to B$.

$3$ and $7$ are of type $N$, and $<$ is a function from $N^2\to B$. So $3<7$ is a valid Boolean that can be treated just like $p$ with respect to the propositional transformations. ie $(3<7)\wedge p\equiv p\wedge (3<7)$.

We can also add $S:N\to N$ the successor function. Here are some more equivalence rules you might want.

$S\alpha <S\beta \equiv \alpha <\beta$

$\alpha <0\equiv \perp$

$0<S\alpha \equiv \top$

$\neg (\alpha <\beta )\equiv \beta <S\alpha$

In general, there is a finite list of types. Call them $X_1,X_2,...X_n$

All functions have a fixed number of inputs, each with a fixed type, and output something of a fixed type. In our parse tree from before, this means that our edges have one of finitely many different colours, and that each symbol node has a fixed pattern of colors for its inputs and outputs. $+$ is a node of type $N$ and both its children are of type $N$. $<$ is a node of type $B$, and both its children are of type $N$. $\neg$ is of type $B$ and has one child of type $B$. Where the output type is not clear, it may be indicated by a subscript. ${<}_B(3_N,5_N)$

Before we can get to predicate logic, we will introduce a set of implicit variable symbols $V_X$ for each type $X$ in use. $V={\cup }_{x=1}^n{V}_X$ is the set of all implicit variables. An implicit variable is an abstract symbol like $\perp$ or $3$. Specific implicit variables will be represented by capital roman letters (ABC). Substitution rules can also contain references to arbitrary members of some $V_X$. Eg

$\text{Sub}({\Gamma }_N,{\delta }_N,{+}_N({\alpha }_N,{\beta }_N\left)\right)\equiv {+}_N\left(\text{Sub}\right({\Gamma }_N,{\delta }_N,{\alpha }_N),\text{Sub}({\Gamma }_N,{\delta }_N,{\beta }_N\left)\right)$

$\text{Sub}({\Gamma }_N,{\delta }_N,{\Gamma }_N)\equiv {\delta }_N$

Here $\text{Sub}$ is the substitution function, the ${\alpha }_N,{\beta }_N,{\delta }_N$ represent any expression that has a real type. The ${\Gamma }_N$ represents any single symbol from the set $V_N$.

Applying these equivalences tells us that

$\text{Sub}(X,5,+(3,X\left)\right)\equiv +\left(\text{Sub}\right(X,5,3),\text{Sub}(X,5,X\left)\right)\equiv +\left(\text{Sub}\right(X,5,3),5)$

If $3$ is a shorthand for $S\left(S\right(S\left(0\right)\left)\right)$ then the rules $\text{Sub}({\Gamma }_N,{\delta }_N,S({\alpha }_N\left)\right)\equiv S\left(\text{Sub}\right({\Gamma }_N,{\delta }_N,{\alpha }_N\left)\right)$ and $\text{Sub}({\Gamma }_N,{\delta }_N,0_N)\equiv 0_N$ allow deduction all the way to $+\left(\text{Sub}\right(X,5,3),5)\equiv 8$

A general first order theory makes use of $=$ and $\forall$ as well as $\left[/\right]$ for substitution. These do not need any special properties, and can be defined by the normal substitution rules. Technically there is a collection of $\text{Sub}$'s, one for each pair of types.

We have $4$ axioms, which can be turned into rules by making them all equivalent to $\top$.

${\forall }_B({\Gamma }_N,{=}_B,({\Gamma }_N,{\Gamma }_N\left)\right)\equiv \top$

${\forall }_B({\Gamma }_N,\forall ({\Delta }_N,⟹{}_B\left({=}_B\right({\alpha }_N,{\beta }_N),{=}_B({\varphi }_B,\text{Sub}({\Gamma }_N,{\Delta }_N,{\varphi }_B)\left)\right)\left)\right)\equiv \top$

$⟹{}_B\left({\forall }_B\right({\Gamma }_N,{\varphi }_B),\text{Sub}({\Gamma }_N,{\alpha }_N,{\varphi }_B\left)\right)\equiv \top$

$⟹{}_B\left({\forall }_N\right({\Gamma }_N,⟹{}_B({\varphi }_B,{\psi }_B)),⟹{}_B({\forall }_N({\Gamma }_N,{\varphi }_B),{\forall }_N({\Gamma }_N,{\psi }_B)\left)\right)$

And a rule that allows generalization.

${\forall }_N({\Gamma }_N,\top )\equiv \top$

I believe that this set of substitution rules, or something like it, can produce predicate logic. I also believe that more substitution rules and symbols can be added to make any first order theory. The intuition is that you can take any proof in any first order logical theory and convert it into a series of substitution rules by anding in any axioms, and applying moduls ponens. Generalization can be done by turning $\top$ into $\forall (X,\top )$ and then using substitutions not dependent on $X$ to turn it into $\forall (X,p)$.

Theorem

For any set of symbols with appropriate type signatures, for any recursively enumerable equivalence relation $H$. (With the property that $a\equiv b⟹f\left(a\right)\equiv f\left(b\right)$ )There exists a finite set of extra symbols and a finite set of substitution rules such that these equivalences hold.

Proof Outline

Introduce the symbols 0,1,end so that binary strings can be stored 0(1(1(0(end))))

Give them some new type Y, and add a load of type converters, symbols that take in an object of type Y, and output some other type.

Introduce + for concatenation.

$+\left(0\right({\alpha }_Y),{\beta }_Y)\equiv 0(+({\alpha }_Y,{\beta }_Y\left)\right)$

And the same for 1

$+(end,{\alpha }_Y)\equiv {\alpha }_Y$

By adding the rules

$P(\alpha ,0(\beta \left)\right)\equiv 0\left(P\right(0\left(\alpha \right),\beta \left)\right)$

$P(\alpha ,1(\beta \left)\right)\equiv 0\left(P\right(1\left(\alpha \right),\beta \left)\right)$

$P(\alpha ,end)\equiv 1\left(\alpha \right)$

Then if $|\alpha |=n$ then $P(end,\alpha )\equiv 0^{n}1reverse\left(\alpha \right)$.

This means that $J(\alpha ,\beta )\equiv +\left(P\right(end,\alpha ),P(end,\beta \left)\right)$ can unambiguously express pairs of bitstrings as a single bitstring.

Arbitrary syntax trees can be encoded like $\ast \left(Con{v}_N\right({\alpha }_Y),Con{v}_N({\beta }_Y\left)\right)\equiv Con{v}_N\left(J\right(010end,J({\alpha }_Y,{\beta }_Y)\left)\right)$

Where 010 is the unique bitstring representing "*", an arbitrary symbol.

Then add a rule that

$Con{v}_N\left({\alpha }_Y\right)\equiv righ{t}_N\left(TM1\right(left\left(J\right({\alpha }_Y,{\beta }_Y\left)\right)\left)\right)$

As ${\beta }_Y$ can be anything, it could be an encoding of what you want. Then we let $left\left(0\right(\alpha \left)\right)\equiv 0\left(left\right(\alpha \left)\right)$ and the same for one, to run $left$ to the far end of the bitstring. Then $left\left(end\right)\equiv n\left(left\right(end\left)\right)$ where $n$ is a null symbol for tape that doesn't store data and we can extend tape as needed. Using rules like $TM1\left(n\right(\alpha \left)\right)\equiv 1\left(TM3\right(\alpha \left)\right)$ we can run any turing machine with one symbol per state. Then finally we have a rule like $TM4\left(0\right(\alpha \left)\right)\equiv success\left(TM4\right(0\left(\alpha \right)\left)\right)$. Let success commute with 0,1 so it can go up to the top. Let $right\left(success\right(\alpha \left)\right)\equiv right\left(success\right(n\left(\alpha \right)\left)\right)$.

Then you can unwind all the computations, and $righ{t}_N\left(success\right(TM1\left(left\right(J({\alpha }_Y,{\beta }_Y)\left)\right)\left)\right)\equiv Con{v}_N\left({\beta }_y\right)$ means that you can take the bit stream that you computed to be equal, and decode it back into its symbols.

Lemma

Any possible computably checkable formal proof system can be converted into an equivalence graph.

Post Ending.

Next time we will see when different proof systems are provably the same. I know the formatting is rough and the explanations aren't always as clear as could be. Tell me about any unusually opaque parts. If these ideas turn out to be important, someone will need to rework this. I know the axioms used are not the simplest possible, and proofs are not fully formalized.