Notation note, are for lists, are for functions.
Note that many of the words and symbols I am using are made up. When this maths is better understood, someone should reinvent the notation. My notation isn't that great, but its hard to make good notation when you are still working out what you want to describe.
A theory (of my new type, not standard maths) T is formally defined to be,
Where are the theories symbols. These can be arbitrary mathematical objects.
is the set of types, also arbitrary.
is a function.
Is also a function.
An expression in a theory is defined recursively, it consists of a pair . Here and is an expression.
Sometimes we will write , what we really mean is , and We write when we want to refer to just and ignore
Expressions have the restriction that the number of elements of that is mapped to is the same as the number of other expressions.
We also insist that for all ,
The base case happens when the empty list.
All expressions are strictly finite mathematical objects. There are no self referential expressions.
Expressions can be written
We can define equality between expressions and recursively by saying iff and forall
The distinction between expressions is defined recursively.
These can be uniquely expressed as strings made up of
Lets define to be the set of all possible expressions of type .
A function is called basic if it is constant, or it is the projection function ( so for fixed ) or can be expressed as
where is constant and each is a basic function of .
Note you can cross as much extra junk into as you like and ignore it. If is basic, so is .
Basic functions can be said to have and
Basic functions can be defined in the style of
Finally, where and are basic functions with the same domains and codomains.
We write to mean that the pair of basic functions and are matched in . Ie where
We express the concept that for expressions that and there exists and expressions such that and by saying
We express that such that and and as . (previous posts use for both concepts)
Lets create a new theory, called T1, this is a very simple theory, it has only 1 constant, 2 functions and 2 substitution rules, with only a single type.
With the only constant being 0. This theory can be considered to be a weak theory of integers with only a +1 and -1 function. It has a connected component of its graph for each integer. Propositions are in the same graph if and only if they have the same . Theorems look like .
Now consider the theory T2 formed by the symbols
It turns out that this theory also has one connected component for each integer, but this time, propositions are in the same component if is the same.
When is a theory and similarly for T.
We can define the disjoint union, to be the theory
Consider a function and a function basic functions in , such that and where means .
These arity conditions mean that for any expression i n , we can define an expression in T
is the set of expressions in . Call a transjection if it meets the condition that . For each meeting the above conditions, there exists exactly one transjection.
We can now define a relation.
We say iff there exists a transjection such that in iff in . Call such transjections projections.
Say iff and .
and implies .
There exists a and projections.
The composition of basic maps is basic, by the recursive definition.
The composition of transjections is a transjection.
So is a transjection.
For all , then
Hence is a projection.
Let be the identity. The identity map is a projection.
Suppose and are theories, with and transjections.
Suppose that for all we know that .
And the same when we swap with . Call and psudoinverses.
If we also know that for all a pair of basic functions, that for all we know . Say that is axiom preserving. Again we know the same when is swapped with , IE that is axiom preserving.
Note that all these claims are potentially provable with a finite list of when the expressions contain the arbitrary constants .
All the stuff above implies that .
Consider . We know that . st there exists and some such that and (or visa versa.)
This tells us that
If then . True because is a basic function, and they preserve similarity.
Repeat this to find that .
If then , and , so so .
On the other hand, if then because the same reasoning also applies to . For any we know .
We know . But and are psudoinverses, so hence
Therefore . Symmetrically, so
Remember our theories and from earlier? The ones about a,b and f,g,h?
We can now express the concept that they are basically the same. .
We can prove this by giving basic functions for each symbol, that generates transjections, and by showing that they are psudoinverses and axiom preserving, we know they are projections and .
, , .
, , , .
For example, pick the symbol . To show that and are psudoinverses, we need to show that . We know .
To prove these transjections to be psudoinverses, do this with all symbols in .
Finally we prove that is axiom preserving. We must show that and that .
is also axiom preserving.
We have formally defined a notion of a theory, and provided a criteria for telling when two theories are trivial distortions of each other. This will allow us notions of logical provability that aren't dependent on an arbitrary choice of formalism. By looking at all equivalent theories, weighted by simplicity, we can hope for a less arbitrary system of logical counterfactuals based on something thematically similar to proof length, although kind of more continuous with graduations of partly true.