Notation note, $\left[\right]$ are for lists, $\left(\right)$ 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,

$T=[\psi ,\rho ,\Xi ,type,arity]$

Where $\psi =\{s_1,s_2,...\}$ are the theories symbols. These can be arbitrary mathematical objects.

$\Xi =\{{\Xi }_1,{\Xi }_2,...\}$ is the set of types, also arbitrary.

$type:\psi \to \Xi$ is a function.

Is also a function.

An expression $E$ in a theory is defined recursively, it consists of a pair $E=[s,v_1,v_2,\cdots ,v_n]$. Here $s\in \psi$ and $\forall 1\le i\le n:v_i$ is an expression.

Let $arity\left(s\right)=[x_1,x_2,...x_m]$

Sometimes we will write $type\left(E\right)$, what we really mean is $type\left(s\right)$, and $arity\left(E\right)=arity\left(s\right)$ We write $symbol\left(E\right)=s$ when we want to refer to just $s$ and ignore $v_1,...,v_n$

Expressions have the restriction that $m=n$ the number of elements of $\Xi$ that $s$ is mapped to is the same as the number of other expressions.

We also insist that for all $i$, $type\left(v_i\right)=x_i$

The base case happens when $arity\left(s\right)=\left[\right]$ the empty list.

All expressions are strictly finite mathematical objects. There are no self referential expressions.

Expressions can be written $s(v_1,...,v_n)$

We can define equality between expressions $e=s(v_1,...)$ and $f=t(w_1,...)$ recursively by saying $e=f$ iff $symbol\left(e\right)=symbol\left(f\right)$ and forall $i:v_i=w_i$

The distinction between expressions $e,f$ is defined recursively.

$e-f=[e,f]$ if $symbol\left(e\right)\ne symbol\left(f\right)$

$e-f=[e,f]$ if $\exists i\ne j\in N:v_i\ne w_{i}and{v}_j\ne w_j$

$e-f=None$ if $e=f$

$e-f=v_i-w_i$ if ${\exists }_{1}i:v_i\ne w_i$

These can be uniquely expressed as strings made up of $\Xi \cup \{{}^{\prime }{(}^{\prime },{}^{\prime }{,}^{\prime },{}^{\prime }{)}^{\prime }\}$

Lets define $V\left(n\right)=V\left({\Xi }_n\right)$ to be the set of all possible expressions of type ${\Xi }_n$.

A function $f:V\left(n_1\right)\times ...V\left(n_t\right)\to V\left(m\right)$ is called basic if it is constant, or it is the projection function ( so $f(e_1,...e_t)=e_k$ for fixed $k\le t$) or $f$ can be expressed as

$f(e_1,...e_t)=s(v_1,...v_n)$ where $s$ is constant and each $v_i$ is a basic function of $e_1,...e_t$.

Note you can cross as much extra junk into $f$ as you like and ignore it. If $f(e_1,e_2)$ is basic, so is $g(e_1,e_3,e_2,e_4)=f(e_1,e_2)$.

Basic functions can be said to have $type\left(f\right)={\Xi }_m$ and $arity\left(f\right)=[{\Xi }_{n_1},...{\Xi }_{n_t}]$

Basic functions can be defined in the style of $f(\alpha ,\beta )=s_1(c_1,\alpha ,s_2(\alpha ,\beta \left)\right)$

Finally, $\rho =\left\{\right[f_1,g_1],[f_2,g_2],\cdots \}$ where $f_i$ and $g_i$ are basic functions with the same domains and codomains. $type\left(v_i\right)=type\left(w_i\right)$

We write $x\left(\alpha \right)\equiv y\left(z\right(\alpha \left)\right)$ to mean that the pair of basic functions $f\left(\alpha \right)=x\left(\alpha \right)$ and $g\left(\alpha \right)=y\left(z\right(\alpha \left)\right)$ are matched in $\rho$. Ie $[f,g]\in \rho$ where $x,y,z\in \psi$

We express the concept that for expressions $e,f$ that $e-f=[p,q]$ and there exists $[f,g]\in \rho$ and expressions $v_1,...v_n$ such that $p=f(v_1,...v_n)$ and $q=g(v_1,...v_n)$ by saying

$e\equiv f$.

We express that $\exists e_1,e_2,...,e_n$ such that $\forall i<n:e_i\equiv e_{i+1}$ and $e_1=e$ and $e_n=f$ as $e\sim f$. (previous posts use $\equiv$ 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.

$a\left(b\right(\alpha \left)\right)\equiv \alpha$

$b\left(a\right(\alpha \left)\right)\equiv \alpha$

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 $count\left(a\right)-count\left(b\right)$. Theorems look like $a\left(a\right(a\left(b\right(b\left(0\right)\left)\right)\left)\right)\sim b\left(a\right(a\left(0\right)\left)\right)$.

Now consider the theory T2 formed by the symbols $f,g,h$

$f\left(f\right(f\left(g\right(g\left(\alpha \right)\left)\right))\equiv \alpha$

$f\left(\alpha \right)\equiv h\left(g\right(\alpha \left)\right)$

$f\left(h\right(\alpha \left)\right)\equiv h\left(f\right(\alpha \left)\right)$

$g\left(h\right(\alpha \left)\right)\equiv h\left(g\right(\alpha \left)\right)$

It turns out that this theory also has one connected component for each integer, but this time, propositions are in the same component if $2\times count\left(f\right)-3\times count\left(g\right)+5\times count\left(h\right)$ is the same.

When $S=({\psi }_S,{\rho }_S,{\Xi }_S,typ{e}_S,arit{y}_S)$ is a theory and similarly for T.

We can define the disjoint union, $S\bigsqcup T$ to be the theory $({\psi }_S\bigsqcup {\psi }_T,{\rho }_S\bigsqcup {\rho }_T,{\Xi }_S\bigsqcup {\Xi }_t,typ{e}_S\bigsqcup typ{e}_T,arit{y}_S\bigsqcup arit{y}_T)$

Consider a function $f:{\Xi }_S\to {\Xi }_T$ and a function $Q:{\psi }_S\to$basic functions in $T$, such that $type\left(Q\right(s_i\left)\right)=f\left(type\right(s_i\left)\right)$ and where$arity\left(s_i\right)=[X_1,...X_n]$ means $arity\left(Q\right(s_i\left)\right)=\left[f\right(Q\left(s_1\right)),...f(Q\left(s_n\right)\left)\right]$.

These arity conditions mean that for any expression $e=s(v_1,...v_n)$ i n $S$, we can define an expression in T

$V_T$ is the set of expressions in $T$. Call $Q^{\ast }:V_S\to V_T$ a transjection if it meets the condition that $Q^{\ast }\left(e\right)=Q\left(s\right)\left(Q^{\ast }\right(v_1),...Q^{\ast }(v_n\left)\right)$. For each $Q$ meeting the above conditions, there exists exactly one transjection.

We can now define a relation.

We say $S\lesssim T$ iff there exists $Q^{\ast }:V_S\to V_T$ a transjection such that $e\sim f$ in $S$ iff $Q^{\ast }\left(e\right)\sim Q^{\ast }\left(f\right)$ in $T$. Call such transjections projections.

Say $S\approx T$ iff $S\lesssim T$ and $T\lesssim S$.

Theorem

$S\lesssim T$ and $T\lesssim U$ implies $S\lesssim U$.

Proof

There exists a $Q:V_S\to V_T$ and $R:V_T\to V_U$ projections.

The composition of basic maps is basic, by the recursive definition.

The composition of transjections is a transjection.

So $R\circ Q$ is a transjection.

For all $e,f\in V_S$, then $e\sim f⟺Q\left(e\right)\sim Q\left(f\right)⟺R\left(Q\right(e\left)\right)\sim R\left(Q\right(f\left)\right)$

Hence $R\circ Q$ is a projection.

Lemma

$S\lesssim S$

Let $Q$ be the identity. The identity map is a projection.

Theorem

Suppose $S$ and $T$ are theories, with $Q:V_S\to V_T$ and $R:V_T\to V_S$ transjections.

Suppose that for all $e=s(v_1,...,v_n)\in V_S$ we know that $R\left(Q\right(e\left)\right)\sim e$.

And the same when we swap $S$ with $T$. Call $Q$ and $R$ psudoinverses.

If we also know that for all $\left[f\right(v_1,...v_n),g(v_1,...v_n\left)\right]\in {\rho }_S$ a pair of basic functions, that for all $v_1,...v_n$ we know $Q\left(f\right(v_1,...\left)\right)\sim Q\left(g\right(v_1,...\left)\right)$ . Say that $Q$ is axiom preserving. Again we know the same when $S$ is swapped with $T$, IE that $R$ is axiom preserving.

Note that all these claims are potentially provable with a finite list of $a\sim b\sim c...$ when the expressions contain the arbitrary constants $v_1,...v_n$.

All the stuff above implies that $S\approx T$.

Proof

Consider $e\equiv f\in V_S$. We know that $e-f=[a,b]$. st there exists $[f,g]\in {\rho }_S$ and some $v_1,...$ such that $f(v_1,...)=a$ and $g(v_1,...)=b$ (or visa versa.)

This tells us that $Q\left(a\right)\sim Q\left(b\right)$

If $\forall i:Q\left(v_i\right)\sim Q\left(w_i\right)$ then $Q\left(s\right(v_1,...v_n\left)\right)\sim Q\left(s\right(w_1,...w_n\left)\right)$. True because $Q\left(s\right)$ is a basic function, and they preserve similarity.

Repeat this to find that $Q\left(e\right)\sim Q\left(f\right)$.

If $e\sim f$ then $e=e_1$, $f=e_n$ and $e_i\equiv e_{i+1}$, so $Q\left(e_i\right)\sim Q\left(e_{i+1}\right)$ so $Q\left(e\right)\sim Q\left(f\right)$.

On the other hand, if $Q\left(e\right)\sim Q\left(f\right)$ then $R\left(Q\right(e\left)\right)\sim R\left(Q\right(f\left)\right)$ because the same reasoning also applies to $R$. For any $e^{\prime },f^{\prime }\in V_T$ we know $e^{\prime }\sim f^{\prime }⟹R\left(e^{\prime }\right)\sim R\left(f^{\prime }\right)$.

We know $Q\left(e\right),Q\left(f\right)\in V_T$. But $S$ and $T$ are psudoinverses, so $e\sim R\left(Q\right(e\left)\right)\sim R\left(Q\right(f\left)\right)\sim f$ hence $e\sim f⟺Q\left(e\right)\sim Q\left(f\right)$

Therefore $S\lesssim T$. Symmetrically, $T\lesssim S$ so $S\approx T$

Remember our theories $T1$ and $T2$ from earlier? The ones about a,b and f,g,h?

We can now express the concept that they are basically the same. $T1\approx T2$.

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 $T1\approx T2$.

$Q:T1\to T2$

$Q\left(0\right)=0$ , $Q\left(a\right(\alpha \left)\right)=f\left(f\right(g\left(Q\right(\alpha \left)\right)\left)\right)$ , $Q\left(b\right(\alpha \left)\right)=f\left(g\right(Q\left(\alpha \right)\left)\right)$.

$R:T2\to T1$

$R\left(f\right(\alpha \left)\right)=a\left(a\right(R\left(\alpha \right)\left)\right)$ , $R\left(g\right(\alpha \left)\right)=b\left(b\right(b\left(R\right(\alpha \left)\right)\left)\right)$ , $R\left(h\right(\alpha \left)\right)=a\left(a\right(a\left(a\right(a\left(R\right(\alpha \left)\right)\left)\right)\left)\right)$ , $R\left(0\right)=0$ .

For example, pick the symbol $a$. To show that $Q$ and $R$ are psudoinverses, we need to show that $R\left(Q\right(a\left(\alpha \right)\left)\right)\sim a\left(\alpha \right)$. We know $R\left(Q\right(a\left(\alpha \right)\left)\right)=R\left(f\right(f\left(g\right(Q\left(\alpha \right)\left)\right)\left)\right)=a\left(a\right(a\left(a\right(b\left(b\right(b\left(R\right(Q\left(\alpha \right)\left)\right)\left)\right)\left)\right)\left)\right)\sim a\left(a\right(a\left(a\right(b\left(b\right(b\left(\alpha \right)\left)\right)\left)\right)\left)\right)\sim a\left(\alpha \right)$.

To prove these transjections to be psudoinverses, do this with all symbols in ${\psi }_S\bigsqcup {\psi }_T$.

Finally we prove that $Q$ is axiom preserving. We must show that $Q\left(a\right(b\left(\alpha \right)\left)\right)\sim Q\left(\alpha \right)$ and that $Q\left(b\right(a\left(\alpha \right)\left)\right)\sim Q\left(\alpha \right)$ . $Q\left(a\right(b\left(\alpha \right)\left)\right)=f\left(f\right(g\left(f\right(g\left(Q\right(\alpha \left)\right)\left)\right)\left)\right)\equiv f\left(f\right(g\left(h\right(g\left(g\right(Q\left(\alpha \right)\left)\right)\left)\right)\left)\right)\equiv f\left(f\right(h\left(g\right(g\left(g\right(Q\left(\alpha \right)\left)\right)\left)\right)\left)\right)\equiv f\left(f\right(f\left(g\right(g\left(Q\right(\alpha \left)\right)\left)\right)\left)\right)\equiv Q\left(\alpha \right)$

Likewise $Q\left(a\right(b\left(\alpha \right)\left)\right)\sim Q\left(\alpha \right)$ .

$R$ is also axiom preserving.

So $T1\approx T2$.

Conclusion

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.