I’ll give short introduction here to some of the background in constructive logic required to provide constructive criticism, as I saw one person here using a gaslighting argument:
Constructive logic is a weaker logic than classical logic, in which a statement A => B is modeled as a lambda expression in simple type theory. Propositional equality is A == B, consisting of two maps A => B and B => A. The reason A == B is technically an assumed position in logic, is that lambda expressions can capture variables from their environment. It means, A == B is a statement in any possible worlds where one starts with a non-empty or empty context. Tautological equality requires an empty context. In Provability Logic, this statement is derived from sequent calculus |- A == B implies □(A == B). However, unlike First Order Logic theories that builds on predicates, Path Semantics is grounded in Propositional Logic with avatars (newtypes), where ¬(false^true) is trivial to prove and ^ is like a function pointer, unable to capture variables, and as a consequence Löb’s theorem and Provability Logic is inconsistent with the meta-theory HOOO EP. The qubit operator ~ is an extension to normal logic using symbolic distinction and has tautological congruence (necessary worlds semantics), unlike predicates in First Order Logic which have normal congruence (possible worlds semantics). This is how the counter-example to Leibniz’ first principle is constructed. The entire theory of Path Semantics builds upon the qubit operator ~, so path semanticists (those who study this field) consider this operator central.
With other words, if you think about this from the perspective Set Theory using First Order Logic, then you are looking at it through the wrong mathematical bias. This makes some people believe that Path Semantics is bullshit, but I ensure you, that the research is formal and rigorous. I don’t want to teach people stuff here about e.g. First Order Logic that they ought to know in order to provide constructive criticism about Path Semantics. I am not a teacher of First Order Logic, that’s not my job. I try to communicate my own research in the best way I can, but I can’t make people learn stuff about First Order Logic in a way when they think their language (I suppose they use it on a daily basis) can do something it simply can’t. The usual trap is that people do not know how equality behaves properly. You are supposed to know the limitations of your tools and I feel embarrassed if I have to point them out to you. I am very well aware of these limitations and my research is not about that, it is about making progress about something else entirely.
I’ll give short introduction here to some of the background in constructive logic required to provide constructive criticism, as I saw one person here using a gaslighting argument:
Constructive logic is a weaker logic than classical logic, in which a statement
A => Bis modeled as a lambda expression in simple type theory. Propositional equality isA == B, consisting of two mapsA => BandB => A. The reasonA == Bis technically an assumed position in logic, is that lambda expressions can capture variables from their environment. It means,A == Bis a statement in any possible worlds where one starts with a non-empty or empty context. Tautological equality requires an empty context. In Provability Logic, this statement is derived from sequent calculus|- A == Bimplies□(A == B). However, unlike First Order Logic theories that builds on predicates, Path Semantics is grounded in Propositional Logic with avatars (newtypes), where¬(false^true)is trivial to prove and^is like a function pointer, unable to capture variables, and as a consequence Löb’s theorem and Provability Logic is inconsistent with the meta-theory HOOO EP. The qubit operator~is an extension to normal logic using symbolic distinction and has tautological congruence (necessary worlds semantics), unlike predicates in First Order Logic which have normal congruence (possible worlds semantics). This is how the counter-example to Leibniz’ first principle is constructed. The entire theory of Path Semantics builds upon the qubit operator~, so path semanticists (those who study this field) consider this operator central.With other words, if you think about this from the perspective Set Theory using First Order Logic, then you are looking at it through the wrong mathematical bias. This makes some people believe that Path Semantics is bullshit, but I ensure you, that the research is formal and rigorous. I don’t want to teach people stuff here about e.g. First Order Logic that they ought to know in order to provide constructive criticism about Path Semantics. I am not a teacher of First Order Logic, that’s not my job. I try to communicate my own research in the best way I can, but I can’t make people learn stuff about First Order Logic in a way when they think their language (I suppose they use it on a daily basis) can do something it simply can’t. The usual trap is that people do not know how equality behaves properly. You are supposed to know the limitations of your tools and I feel embarrassed if I have to point them out to you. I am very well aware of these limitations and my research is not about that, it is about making progress about something else entirely.