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. and . All the functions and transformation rules in the previous post apply to . For example, is of type . is a function from .
and are of type , and is a function from . So is a valid Boolean that can be treated just like with respect to the propositional transformations. ie .
We can also add the successor function. Here are some more equivalence rules you might want.
In general, there is a finite list of types. Call them
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 and both its children are of type . is a node of type , and both its children are of type . is of type and has one child of type . Where the output type is not clear, it may be indicated by a subscript.
Before we can get to predicate logic, we will introduce a set of implicit variable symbols for each type in use. is the set of all implicit variables. An implicit variable is an abstract symbol like or . Specific implicit variables will be represented by capital roman letters (ABC). Substitution rules can also contain references to arbitrary members of some . Eg
Here is the substitution function, the represent any expression that has a real type. The represents any single symbol from the set .
Applying these equivalences tells us that
If is a shorthand for then the rules and allow deduction all the way to
A general first order theory makes use of and as well as for substitution. These do not need any special properties, and can be defined by the normal substitution rules. Technically there is a collection of 's, one for each pair of types.
We have axioms, which can be turned into rules by making them all equivalent to .
And a rule that allows generalization.
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 into and then using substitutions not dependent on to turn it into .
For any set of symbols with appropriate type signatures, for any recursively enumerable equivalence relation . (With the property that )There exists a finite set of extra symbols and a finite set of substitution rules such that these equivalences hold.
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.
And the same for 1
By adding the rules
Then if then .
This means that can unambiguously express pairs of bitstrings as a single bitstring.
Arbitrary syntax trees can be encoded like
Where 010 is the unique bitstring representing "*", an arbitrary symbol.
Then add a rule that
As can be anything, it could be an encoding of what you want. Then we let and the same for one, to run to the far end of the bitstring. Then where is a null symbol for tape that doesn't store data and we can extend tape as needed. Using rules like we can run any turing machine with one symbol per state. Then finally we have a rule like . Let success commute with 0,1 so it can go up to the top. Let .
Then you can unwind all the computations, and means that you can take the bit stream that you computed to be equal, and decode it back into its symbols.
Any possible computably checkable formal proof system can be converted into an equivalence graph.
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.