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,
T=[ψ,ρ,Ξ,type,arity]
Where ψ={s1,s2,...} are the theories symbols. These can be arbitrary mathematical objects.
Ξ={Ξ1,Ξ2,...} is the set of types, also arbitrary.
type:ψ→Ξ is a function.
arity:ψ→∪∞i=0Ξ×Ξ×⋯×Ξi
Is also a function.
An expression E in a theory is defined recursively, it consists of a pair E=[s,v1,v2,⋯,vn]. Here s∈ψ and ∀1≤i≤n:vi is an expression.
Let arity(s)=[x1,x2,...xm]
Sometimes we will write type(E), what we really mean is type(s), and arity(E)=arity(s) We write symbol(E)=s when we want to refer to just s and ignore v1,...,vn
Expressions have the restriction that m=n the number of elements of Ξ that s is mapped to is the same as the number of other expressions.
We also insist that for all i, type(vi)=xi
The base case happens when arity(s)=[] the empty list.
All expressions are strictly finite mathematical objects. There are no self referential expressions.
Expressions can be written s(v1,...,vn)
We can define equality between expressions e=s(v1,...) and f=t(w1,...) recursively by saying e=f iff symbol(e)=symbol(f) and forall i:vi=wi
The distinction between expressions e,f is defined recursively.
e−f=[e,f] if symbol(e)≠symbol(f)
e−f=[e,f] if ∃i≠j∈N:vi≠wiandvj≠wj
e−f=None if e=f
e−f=vi−wi if ∃1i:vi≠wi
These can be uniquely expressed as strings made up of Ξ∪{′(′,′,′,′)′}
Lets define V(n)=V(Ξn) to be the set of all possible expressions of type Ξn.
A function f:V(n1)×...V(nt)→V(m) is called basic if it is constant, or it is the projection function ( so f(e1,...et)=ek for fixed k≤t) or f can be expressed as
f(e1,...et)=s(v1,...vn) where s is constant and each vi is a basic function of e1,...et.
Note you can cross as much extra junk into f as you like and ignore it. If f(e1,e2) is basic, so is g(e1,e3,e2,e4)=f(e1,e2).
Basic functions can be said to have type(f)=Ξm and arity(f)=[Ξn1,...Ξnt]
Basic functions can be defined in the style of f(α,β)=s1(c1,α,s2(α,β))
Finally, ρ={[f1,g1],[f2,g2],⋯} where fi and gi are basic functions with the same domains and codomains. type(vi)=type(wi)
We write x(α)≡y(z(α)) to mean that the pair of basic functions f(α)=x(α) and g(α)=y(z(α)) are matched in ρ. Ie [f,g]∈ρ where x,y,z∈ψ
We express the concept that for expressions e,f that e−f=[p,q] and there exists [f,g]∈ρ and expressions v1,...vn such that p=f(v1,...vn) and q=g(v1,...vn) by saying
e≡f.
We express that ∃e1,e2,...,en such that ∀i<n:ei≡ei+1 and e1=e and en=f as e∼f. (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.
a(b(α))≡α
b(a(α))≡α
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(a)−count(b). Theorems look like a(a(a(b(b(0)))))∼b(a(a(0))).
Now consider the theory T2 formed by the symbols f,g,h
f(f(f(g(g(α))))≡α
f(α)≡h(g(α))
f(h(α))≡h(f(α))
g(h(α))≡h(g(α))
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×count(f)−3×count(g)+5×count(h) is the same.
When S=(ψS,ρS,ΞS,typeS,arityS) is a theory and similarly for T.
We can define the disjoint union, S⊔T to be the theory (ψS⊔ψT,ρS⊔ρT,ΞS⊔Ξt,typeS⊔typeT,arityS⊔arityT)
Consider a function f:ΞS→ΞT and a function Q:ψS→basic functions in T, such that type(Q(si))=f(type(si)) and wherearity(si)=[X1,...Xn] means arity(Q(si))=[f(Q(s1)),...f(Q(sn))].
These arity conditions mean that for any expression e=s(v1,...vn) i n S, we can define an expression in T
VT is the set of expressions in T. Call Q∗:VS→VT a transjection if it meets the condition that Q∗(e)=Q(s)(Q∗(v1),...Q∗(vn)). For each Q meeting the above conditions, there exists exactly one transjection.
We can now define a relation.
We say S≲T iff there exists Q∗:VS→VT a transjection such that e∼f in S iff Q∗(e)∼Q∗(f) in T. Call such transjections projections.
Say S≈T iff S≲T and T≲S.
Theorem
S≲T and T≲U implies S≲U.
Proof
There exists a Q:VS→VT and R:VT→VU projections.
The composition of basic maps is basic, by the recursive definition.
The composition of transjections is a transjection.
So R∘Q is a transjection.
For all e,f∈VS, then e∼f⟺Q(e)∼Q(f)⟺R(Q(e))∼R(Q(f))
Hence R∘Q is a projection.
Lemma
S≲S
Let Q be the identity. The identity map is a projection.
Theorem
Suppose S and T are theories, with Q:VS→VT and R:VT→VS transjections.
Suppose that for all e=s(v1,...,vn)∈VS we know that R(Q(e))∼e.
And the same when we swap S with T. Call Q and R psudoinverses.
If we also know that for all [f(v1,...vn),g(v1,...vn)]∈ρS a pair of basic functions, that for all v1,...vn we know Q(f(v1,...))∼Q(g(v1,...)) . 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∼b∼c... when the expressions contain the arbitrary constants v1,...vn.
All the stuff above implies that S≈T.
Proof
Consider e≡f∈VS. We know that e−f=[a,b]. st there exists [f,g]∈ρS and some v1,... such that f(v1,...)=a and g(v1,...)=b (or visa versa.)
This tells us that Q(a)∼Q(b)
If ∀i:Q(vi)∼Q(wi) then Q(s(v1,...vn))∼Q(s(w1,...wn)). True because Q(s) is a basic function, and they preserve similarity.
Repeat this to find that Q(e)∼Q(f).
If e∼f then e=e1, f=en and ei≡ei+1, so Q(ei)∼Q(ei+1) so Q(e)∼Q(f).
On the other hand, if Q(e)∼Q(f) then R(Q(e))∼R(Q(f)) because the same reasoning also applies to R. For any e′,f′∈VT we know e′∼f′⟹R(e′)∼R(f′).
We know Q(e),Q(f)∈VT. But S and T are psudoinverses, so e∼R(Q(e))∼R(Q(f))∼f hence e∼f⟺Q(e)∼Q(f)
Therefore S≲T. Symmetrically, T≲S so S≈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≈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≈T2.
For example, pick the symbol a. To show that Q and R are psudoinverses, we need to show that R(Q(a(α)))∼a(α). We know R(Q(a(α)))=R(f(f(g(Q(α)))))=a(a(a(a(b(b(b(R(Q(α)))))))))∼a(a(a(a(b(b(b(α)))))))∼a(α).
To prove these transjections to be psudoinverses, do this with all symbols in ψS⊔ψT.
Finally we prove that Q is axiom preserving. We must show that Q(a(b(α)))∼Q(α) and that Q(b(a(α)))∼Q(α) . Q(a(b(α)))=f(f(g(f(g(Q(α))))))≡f(f(g(h(g(g(Q(α)))))))≡f(f(h(g(g(g(Q(α)))))))≡f(f(f(g(g(Q(α))))))≡Q(α)
Likewise Q(a(b(α)))∼Q(α) .
R is also axiom preserving.
So T1≈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.
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,
T=[ψ,ρ,Ξ,type,arity]
Where ψ={s1,s2,...} are the theories symbols. These can be arbitrary mathematical objects.
Ξ={Ξ1,Ξ2,...} is the set of types, also arbitrary.
type:ψ→Ξ is a function.
Is also a function.
An expression E in a theory is defined recursively, it consists of a pair E=[s,v1,v2,⋯,vn]. Here s∈ψ and ∀1≤i≤n:vi is an expression.
Let arity(s)=[x1,x2,...xm]
Sometimes we will write type(E), what we really mean is type(s), and arity(E)=arity(s) We write symbol(E)=s when we want to refer to just s and ignore v1,...,vn
Expressions have the restriction that m=n the number of elements of Ξ that s is mapped to is the same as the number of other expressions.
We also insist that for all i, type(vi)=xi
The base case happens when arity(s)=[ ] the empty list.
All expressions are strictly finite mathematical objects. There are no self referential expressions.
Expressions can be written s(v1,...,vn)
We can define equality between expressions e=s(v1,...) and f=t(w1,...) recursively by saying e=f iff symbol(e)=symbol(f) and forall i:vi=wi
The distinction between expressions e,f is defined recursively.
e−f=[e,f] if symbol(e)≠symbol(f)
e−f=[e,f] if ∃i≠j∈N:vi≠wi and vj≠wj
e−f=None if e=f
e−f=vi−wi if ∃1 i:vi≠wi
These can be uniquely expressed as strings made up of Ξ∪{ ′(′, ′,′, ′)′}
Lets define V(n)=V(Ξn) to be the set of all possible expressions of type Ξn.
A function f:V(n1)×...V(nt)→V(m) is called basic if it is constant, or it is the projection function ( so f(e1,...et)=ek for fixed k≤t) or f can be expressed as
f(e1,...et)=s(v1,...vn) where s is constant and each vi is a basic function of e1,...et.
Note you can cross as much extra junk into f as you like and ignore it. If f(e1,e2) is basic, so is g(e1,e3,e2,e4)=f(e1,e2).
Basic functions can be said to have type(f)=Ξm and arity(f)=[Ξn1,...Ξnt]
Basic functions can be defined in the style of f(α,β)=s1(c1,α,s2(α,β))
Finally, ρ={[f1,g1],[f2,g2],⋯} where fi and gi are basic functions with the same domains and codomains. type(vi)=type(wi)
We write x(α)≡y(z(α)) to mean that the pair of basic functions f(α)=x(α) and g(α)=y(z(α)) are matched in ρ. Ie [f,g]∈ρ where x,y,z∈ψ
We express the concept that for expressions e,f that e−f=[p,q] and there exists [f,g]∈ρ and expressions v1,...vn such that p=f(v1,...vn) and q=g(v1,...vn) by saying
e≡f.
We express that ∃ e1,e2,...,en such that ∀ i<n:ei≡ei+1 and e1=e and en=f as e∼f. (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.
a(b(α))≡α
b(a(α))≡α
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(a)−count(b). Theorems look like a(a(a(b(b(0)))))∼b(a(a(0))).
Now consider the theory T2 formed by the symbols f,g,h
f(f(f(g(g(α))))≡α
f(α)≡h(g(α))
f(h(α))≡h(f(α))
g(h(α))≡h(g(α))
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×count(f)−3×count(g)+5×count(h) is the same.
When S=(ψS,ρS,ΞS,typeS,arityS) is a theory and similarly for T.
We can define the disjoint union, S⊔T to be the theory (ψS⊔ψT,ρS⊔ρT,ΞS⊔Ξt,typeS⊔typeT,arityS⊔arityT)
Consider a function f:ΞS→ΞT and a function Q:ψS→basic functions in T, such that type(Q(si))=f(type(si)) and wherearity(si)=[X1,...Xn] means arity(Q(si))=[f(Q(s1)),...f(Q(sn))].
These arity conditions mean that for any expression e=s(v1,...vn) i n S, we can define an expression in T
VT is the set of expressions in T. Call Q∗:VS→VT a transjection if it meets the condition that Q∗(e)=Q(s)(Q∗(v1),...Q∗(vn)). For each Q meeting the above conditions, there exists exactly one transjection.
We can now define a relation.
We say S≲T iff there exists Q∗:VS→VT a transjection such that e∼f in S iff Q∗(e)∼Q∗(f) in T. Call such transjections projections.
Say S≈T iff S≲T and T≲S.
Theorem
S≲T and T≲U implies S≲U.
Proof
There exists a Q:VS→VT and R:VT→VU projections.
The composition of basic maps is basic, by the recursive definition.
The composition of transjections is a transjection.
So R∘Q is a transjection.
For all e,f∈VS, then e∼f⟺Q(e)∼Q(f)⟺R(Q(e))∼R(Q(f))
Hence R∘Q is a projection.
Lemma
S≲S
Let Q be the identity. The identity map is a projection.
Theorem
Suppose S and T are theories, with Q:VS→VT and R:VT→VS transjections.
Suppose that for all e=s(v1,...,vn)∈VS we know that R(Q(e))∼e.
And the same when we swap S with T. Call Q and R psudoinverses.
If we also know that for all [f(v1,...vn),g(v1,...vn)]∈ρS a pair of basic functions, that for all v1,...vn we know Q(f(v1,...))∼Q(g(v1,...)) . 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∼b∼c... when the expressions contain the arbitrary constants v1,...vn.
All the stuff above implies that S≈T.
Proof
Consider e≡f∈VS. We know that e−f=[a,b]. st there exists [f,g]∈ρS and some v1,... such that f(v1,...)=a and g(v1,...)=b (or visa versa.)
This tells us that Q(a)∼Q(b)
If ∀i:Q(vi)∼Q(wi) then Q(s(v1,...vn))∼Q(s(w1,...wn)). True because Q(s) is a basic function, and they preserve similarity.
Repeat this to find that Q(e)∼Q(f).
If e∼f then e=e1, f=en and ei≡ei+1, so Q(ei)∼Q(ei+1) so Q(e)∼Q(f).
On the other hand, if Q(e)∼Q(f) then R(Q(e))∼R(Q(f)) because the same reasoning also applies to R. For any e′,f′∈VT we know e′∼f′⟹R(e′)∼R(f′).
We know Q(e),Q(f)∈VT. But S and T are psudoinverses, so e∼R(Q(e))∼ R(Q(f))∼ f hence e∼f⟺Q(e)∼Q(f)
Therefore S≲T. Symmetrically, T≲S so S≈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≈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≈T2.
Q:T1→T2
Q(0)=0 , Q(a(α))=f(f(g(Q(α)))) , Q(b(α))=f(g(Q(α))).
R:T2→T1
R(f(α))=a(a(R(α))) , R(g(α))=b(b(b(R(α)))) , R(h(α))=a(a(a(a(a(R(α)))))) , R(0)=0 .
For example, pick the symbol a. To show that Q and R are psudoinverses, we need to show that R(Q(a(α)))∼a(α). We know R(Q(a(α)))=R(f(f(g(Q(α)))))=a(a(a(a(b(b(b(R(Q(α)))))))))∼a(a(a(a(b(b(b(α)))))))∼a(α).
To prove these transjections to be psudoinverses, do this with all symbols in ψS⊔ψT.
Finally we prove that Q is axiom preserving. We must show that Q(a(b(α)))∼Q(α) and that Q(b(a(α)))∼Q(α) . Q(a(b(α)))=f(f(g(f(g(Q(α))))))≡f(f(g(h(g(g(Q(α)))))))≡f(f(h(g(g(g(Q(α)))))))≡f(f(f(g(g(Q(α))))))≡Q(α)
Likewise Q(a(b(α)))∼Q(α) .
R is also axiom preserving.
So T1≈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.