This is a short story written with help from ChatGPT, about the intuition behind counter-examples to Leibniz' first principle. This is generally believe to be true among logicians, but the equality as it is expressed in Leibniz' first principle is just an assumption about equality and not a proof of equality.
x=y → ∀F(Fx ↔ Fy) Leibniz' first principle
In short, Leibniz' first principle does not hold for all operators in mathematics, because not all operators are congruent by normal equality.
It is not possible to reason about proofs of equality directly in logic (this is not about terms of types as proofs, but about "actual proofs"). There is a weaker statement of tautological equality that is used to provide this intuition.
If x=y is taken as "tautological equality", then the principle holds, but since tautological equality can be assumed, this does not prove that all properties are the same in the strong sense, but only a weak sense (up to provability within the language).
Now, it is important to remember that this counter-example is relative to the theory of Path Semantics. In the theory of Path Semantics, reasoning with symbolic indistinction (what would be considered actual numerical sameness) is not considered safe, only symbolic distinction. This is why it gets so complex, as there is no way to access the "actual" proof directly.
In Path Semantics, the actual counter-example to Leibniz' first principle is the qubit operator ~ which has tautological congruence. This is not part of the short story and takes a lot more background knowledge to understand. For those interested, one can read about the classical model of path semantical qubit here:
The Pocket-Prover library contains an implementation of the classical model: https://crates.io/crates/pocket_prover
The constructive model is more complex and uses a higher order logic with propositional exponentials (HOOO EP). You can try out an implementation using Rust: https://crates.io/crates/prop
Provability logic is inconsistent together with HOOO EP, so you can not use one to talk about the other. HOOO EP has an associated modal logic, but Löb's theorem is false in this model.
OK, that thread is from last year, before HOOO EP was completed. HOOO EP is now completed.
You should not be confused by the term "Path Semantics", as this is the name of my project. The foundational level of Path Semantics is a set of logical languages consisting of IPL, HOOO EP, PSQ and PSI.
Of course HOOO EP is a made up term. I am the person who invented it. However, the Prop library contains stuff about IPL, which is not something I invented. You don't have to understand HOOO EP to trust that IPL is previous work, as it is well established field. Consider HOOO EP a contribution I have done to Type Theory. The same for PSQ and PSI. PSQ is fully formalized and PSI is almost completed.
It takes time to publish research. The foundation work in Path Semantics is not yet completed, but it is getting closer now as it can model functional programming using the "types as propositions" approach known from Category Theory. There is a link between Path Semantics and Homotopy Type Theory, but this is not yet formalized. I will visit Henri Pointcare Institute this year, as they have the best collection in the world of work in topology.
Let me break down Kent Palmer's paper for you: Zizek saved Lacan's sexuation formulas from the dustbin of history and connected it to work of Derrida. There is an ongoing program in Continental Philosophy where these ideas are being developed. I am not part of this development. However, I helped Kent Palmer to formalize his Schema Theory in propositional logic and developed a grammar of "maximal mathematical languages", which is generalization of Gödel's Incompleteness Theorems extended with results from philosophy of the past century. Kent Palmer is a veteran in this field and is perhaps one of the few people in the world that know the work 6 modern philosophers in great detail. He is hosting reading groups in philosophy and Applied Category Theory. "Nilsen theories" is his naming of the Inside/Outside distinction I used to introduce an underlying structure in the formalization of his Schema Theory. The name "Schema" goes back to Emmanuel Kant, hence the reference to Antimonies of Kant.
The name "Seshatism" comes from the Anti-Thoth argument of Daniel Fischer based on Plato's writings. Thoth was an ancient Egyptian god credited with invention of writing. His female consort, Seshat, was also credited invention of writing by some believers, but this was forgotten by history at the time of Plato. The Anti-Thoth argument is about language bias introduced by the core axiom in Path Semantics, which can be thought of as a kind of Platonic bias. The corresponding anti-bias is dual-Platonic, but I did not want to negate Platonism as there was a whole philosophy and mythology in ancient Egypt that was dual to the later Platonism. Therefore, I named it "Seshatism" after Seshat.
If you are reading a math paper from a researcher that is at the top of their field, then it is very likely that you need to spend a lot of time absorbing the ideas and learn new concepts. This is just natural. I estimate Path Semantics is more than twice as hard to learn than e.g. IPL. I am trying to flatten the learning curve, but there is only so much I can do and I need to complete the foundation first.
You can also take a look at Avalog, which is an implementation of Avatar Logic. I made it from scratch, using my own experience building automated theorem provers. I took the work of Barry Jay about Closure Calculus and formalized it in Avalog. I also formalized an example of MIRI's research into Cartesian Frames, which is Chu spaces. This was just a test run to check whether Avalog made it easier to formalize modern research in mathematics.
So, this is the level of expertise that I work on a daily basis. When somebody like you that claim this is generated by GPT, you can't expect me to take you seriously. I don't know anything about your background, so if I try to explain my own research to you, it's like shooting in the dark. If somebody doesn't understand what IPL is, so what? I got research to do and it's not wrong of me to share things about it. There is a reason the organization is called AdvancedResearch!
I am not good at writing papers, but the papers uploaded are work documents. They are used internally in the organization. There has been people like you trying to figure out whether I am a crackpot, but that's just reddit drama. Good luck with that.