List of Contributions to Mathematics

List of Contributions to Mathematics

This page lists contributions that the Path Semantics project has to mathematics.

1. Counter-example to Leibniz' law "Indiscernibility of Identicals"

See entry about Leibniz' law on Stanford Encyclopedia of Philosophy. The wikipedia article is also informative.

Leibniz' "Indiscernibility of Identicals" is generally considered as an a priori logical truth.

∀ x, y { (x == y) => ∀ F { F(x) == F(y) } }

However, in the constructive model of Path Semantical Quantum Propositional Logic (PSQ), the qubit operator requires tautological congruence, using Higher Order Operator Overloading Exponential Propositions (HOOO EP):

∀ x, y { (x == y)^true => (~x == ~y) }

It means, x == y is not strong enough as it can capture variables from the environment, as propositional equality in constructive logic consists of two maps x => y and y => x, which are lambdas. On the other hand, (x == y)^true are two function pointers x -> y and y -> x, also written x^y and y^x. Function pointers can not capture variables from the environment, so they provide stronger mechanisms to express tautological propositional equality.

In the classical model of PSQ, the qubit operator ~ depends on the entire bit vector (theoretically) while the practical implementations uses a trick to work around undecidability, which works since the output bit vector is randomized. Tautological congruence, which is the same as a modified principle using tautological propositional equality, can be interpreted that two propositions have the same bit vector if and only if they can be proved to be equal without making any assumptions.

Therefore, the first principle has a counter-example and hence is logically false. Also, as a consequence, First Order Logic with this principle is not suitable for modelling mathematics in general. For this reason the qubit operator in PSQ is generally not considered by path semanticists to be a predicate.

2. Mathematical Foundation of Randomness

The qubit operator ~ in Path Semantics has tautological congruence, which means that two outputs are equal only if the inputs can be shown to be equal without making any assumptions. The associated logic is Higher Order Operator Overloading Exponential Propositions (HOOO EP) which are used to extend Intuitionistic Propositional Logic (IPL). While HOOO EP can be used independently of the qubit operator ~, it is the semantics of the qubit operator ~ itself that provides a grounding of the meaning of randomness seen through the perspective of IPL + HOOO EP.

Tautological congruence of the qubit operator ~:

~x ⋀ (x == y)^true  =>  ~y

HOOO EP:

x^y  =>  (x^y)^z
(x => y)^c  =>  (x^c => y^c)^true
(x ⋁ y)^c  =>  (x^c ⋁ y^c)^true

Thus, since randomness of this sort is well behaved and its meta-logical properties well defined, it provides a mathematical foundation of randomness. This foundation might not be complete, but at least it is a start.

3. Propositional Foundation of Types

Type Theory is the leading candidate for providing a formalist perspective of mathematical foundations. However, in Type Theory, types are judgements that are atomic, hence irreducible.

In Path Semantics, a type judgement can be modeled as a proposition:

(a : b)  ==  (a => b) ⋀ (a < b)

Where < is path semantical order. Path Semantical order associates a natural number to path semantical propositions that describes a propositional level, where each level is an Intuitionistic Propositional Logic (IPL). The core axiom of Path Semantics is assumed between path semantical levels.

Therefore, Path Semantics might be seen as even more fundamental than Type Theory. Furthermore, it uses propositions, which are generally respected in logic as valid mathematical objects.

4. Category Realizable Groupoids

The imaginary inverse operator inv in Path Semantics can be thought of as an opposite category functor that lifts a category into a groupoid. This operator inv is imaginary because it follows the law of composition as if there was a solution for any morphism.

f . inv(f)  ==  id
inv(f) . f  ==  id

A solution of e.g. inv(f) == g is a 2-morphism. For higher categories, e.g. an n-category, this results in an n+1-groupoid.

This brings categories in line with the use of n-groupoids as fundamental objects for higher dimensional mathematics in Homotopy Type Theory.

5. Counter-Example of Set Theory as Foundation for Mathematics

There exists a counter-example of Set Theory as foundation for mathematics in Path Semantics, using the notation of normal path:

f : bool -> bool  =>  f[true1] == true1

Here, true1 is a boolean function of type bool -> bool which returns true for all inputs.

The left side of the equation f[true1] has no model in Set Theory.

One can think about this normal path as contracting unobserved values. It works fine as long there is no distinction being made between tr : bool and fa : bool, since (tr == fa) => false. The idea of such contractions fits nicely with the homotopy interpretation of Homotopy Type Theory.

In Set Theory, a model is required at every step in the proof, since there is no meta-language that allows syntactical manipulations beyond models. Since such syntactical manipulations are abundant in mathematics, it is not merely a "symbolic manipulation system" as previously believed, but an actual foundation of mathematics closer to the homotopy interpretation than sets. The consequence is that Set Theory is unsuitable as a foundation for mathematics (although an arguably useful one when there are underlying models corresponding to sets).

6. Propositional Foundation of Time

The core axiom of Path Semantics allows propositional relations to propagate across path semantical levels:

(a ~~ b) ⋀ (a => c) ⋀ (b => d) ⋀ (a < c) ⋀ (b < d)  =>  (c ~~ d)

In the domain of fundamental theoretical physics, this propagation provides a mechanism to understand time seen from a logical point of view. The qubit operator ~ and the equivalent quality operator ~~ carries propositional states in unstructured time, like General Relativity, while path semantical levels might be thought of local frames of reference with approximate Euclidean-geometric properties. With other words, a path semantical level is a "moment" in time where reasoning can take place.

x ~~ y  ==  (x == y) ⋀ ~x ⋀ ~y

This relates reasoning to physical experience of time and might help to explain why known forms of consciousness take place in integrated information processing systems, such as human brains.

While this model of time does not encode clocks directly, it can also show that special synchronizing propositions might be used as logical analogues of clocks. The physical intuition about time in relativity is reflected in the logical structure.

7. Normal Paths as Mechanism for Orthogonal Concrete/Abstract Dimensions

A computation might be thought of as following a series of instructions to produce an output from some given input. When computation happens over time, as in a one-dimensional setting, it can be thought of as a "concrete" process.

Path Semantics provides a perspective of a corresponding abstract dimension:

        len x len
       o ------> o
       |         |
       |         |
concat |         | add
       v         v
       o ------> o
           len

concat[len] == add

The left side might be thought of as a concrete computation taking place in time, while the right side might be thought of as an abstract projection of this computation. The more abstract a theory is, the more contractions away from the underlying concrete computation.

Since such commutative diagrams can be transposed along the diagonal, there is a perspective where concrete processes can be seen as abstract and vice versa.

This also reflect the time-space symmetry in theoretical physics, where a valid Feynman diagram can be transposed by changing the time with the space axis.