Harry Potter in The World of Path Semantics
post by Sven Nilsen (bvssvni) · 2023-03-22T20:22:37.874Z · LW · GW · 17 commentsThis is a link post for https://raw.githubusercontent.com/advancedresearch/path_semantics/master/papers-wip2/harry-potter-in-the-world-of-path-semantics.pdf
Contents
17 comments
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.
17 comments
Comments sorted by top scores.
comment by Dave Orr (dave-orr) · 2023-03-22T20:38:30.053Z · LW(p) · GW(p)
Next time I would actually include the definition of a technical term like Leibniz's first principle to make this post a little less opaque, and therefore more interesting, to non experts.
Replies from: bvssvni↑ comment by Sven Nilsen (bvssvni) · 2023-03-22T20:41:40.961Z · LW(p) · GW(p)
Thank you! Post updated to include the definition.
comment by Sonata Green · 2023-04-19T23:14:42.138Z · LW(p) · GW(p)
I think this might be trying to talk about something related to identity of indiscernibles, the disquotational principle, and the masked-man fallacy. I'm not sure how you get from "different names for the same entity" to "magical clones", though.
comment by Sven Nilsen (bvssvni) · 2023-03-24T15:43:41.369Z · LW(p) · GW(p)
The paper about the counter-example to Leibniz's First Principle in Path Semantics has been released: https://github.com/advancedresearch/path_semantics/blob/master/papers-wip2/counter-example-to-leibniz-first-principle.pdf
comment by Sven Nilsen (bvssvni) · 2023-03-23T00:42:38.320Z · LW(p) · GW(p)
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.
comment by Viliam · 2023-03-22T23:53:42.992Z · LW(p) · GW(p)
Uhm, could someone other than the author please confirm that this entire "path semantics" thing is something other than word salad? To me it seems like not just the HP story, but this entire thing is GPT generated.
Replies from: bvssvni↑ comment by Sven Nilsen (bvssvni) · 2023-03-23T00:04:58.467Z · LW(p) · GW(p)
Author here. This is based on research from implemented theorem proving. See the links in the post.
Replies from: Viliam↑ comment by Viliam · 2023-03-23T08:44:31.636Z · LW(p) · GW(p)
I apologize, but the links all go to pages written by you, so I don't count it as independent confirmation. Wikipedia has nothing on "path semantics". Google mostly returns things written by you; plus one paper with this title, but its content seems unrelated, so perhaps it is a coincidence.
So, from my perspective, it just seems like something you made up. That is not necessarily a bad thing, you may have invented something useful, I have no idea. Some kind of peer review would be nice. Unfortunately, your posts here did not start a technical discussion.
At this moment, my working hypothesis is that no one here understands this, but most people assume that someone else does.
Replies from: bvssvni↑ comment by Sven Nilsen (bvssvni) · 2023-03-23T11:18:07.743Z · LW(p) · GW(p)
I assume you can assume for yourself that what I write is nonsense, but this does not prove that I am writing nonsense. Claiming that my work is generated by GPT is false, when it isn't.
That's not how logic works. If no evidence I provide can convince you otherwise, then your condition for changing your mind is predicated on that the agent proving you evidence is not me. This is not acceptable for me, because if I give you link to somebody who uses my work or a computer program that uses my theory, then you will not accept it as a reason to investigate further.
You didn't make a claim that some of my work is wrong, you made the claim that the ENTIRE thing is wrong, which is a gaslighting argument.
↑ comment by Walker Vargas · 2023-03-23T17:18:19.598Z · LW(p) · GW(p)
No, if you are contributing to a preexisting discussion, there should be some older work you can cite. For example, you learned about the theory of path semantics from something that wasn't written by you. Cite that source.
Replies from: bvssvni↑ comment by Sven Nilsen (bvssvni) · 2023-03-23T18:11:32.229Z · LW(p) · GW(p)
Path semantics is built upon previous works, e.g. Homotopy Type Theory: https://homotopytypetheory.org/
This kind of previous work is cited all of the place. I have no idea why you think there is no preexisting discussion going on.
↑ comment by Viliam · 2023-03-23T15:47:53.571Z · LW(p) · GW(p)
Eh, I am quite aware of the chance that I am just making an idiot out of myself. Yet I felt that this was a question someone should ask, because... well, you know the story about the Emperor's new clothes.
If I am wrong here, I am really sorry. However, please consider the evidence I have, from my perspective. What conclusion would you make out of it in my place?
- you talk about something no one else does, on the entire part of internet indexed by Google;
- yet you talk about it as if it's something people are supposed to know;
- googling for "Leibniz' first principle" is similarly fruitless (okay, you added it to the article, but the weird thing is using a phrase no one else on the entire internet does, and assuming it standard);
- this is a website with many people highly knowledgeable about math and logic, yet none of them started a dialog (whether agreement or disagreement) with you;
- I happen to have some decent-but-not-exceptional background in math myself, and nothing on the Wikipedia page about first-order logic seems related to what you wrote here.
I emphasize that it is not the last bullet point alone, but all five of them together, that made me write this.
What conclusion would you have made in my place? What is your explanation for why no one else seems to talk about "path semantic" and "semantical qubit" on the internet?
If no evidence I provide can convince you otherwise, then your condition for changing your mind is predicated on that the agent proving you evidence is not me. This is not acceptable for me, because if I give you link to somebody who uses my work or a computer program that uses my theory, then you will not accept it as a reason to investigate further.
If the computer program that uses your theory was also written by you, that indeed would not convince me.
On the other hand, a scientific paper written by someone else, referring to your paper or to your program, that could make me change my mind, if you could link it.
Replies from: bvssvni↑ comment by Sven Nilsen (bvssvni) · 2023-03-23T16:58:21.127Z · LW(p) · GW(p)
Yes, all you needed was simply to ask: https://www.academia.edu/45073917/Asymmetries_of_Complementary_Nilsen_Theories?email_work_card=title
Here is a theory based on the work of 3 people in collaboration: https://github.com/advancedresearch/joker_calculus
I can give you more examples.
Let's say you don't trust the Pocket-Prover library. Yet, this library is a brute force theorem prover that no person so far has reported bugs. I understand you won't trust it without further investigation, but there are no other people who have reasonable doubt about it. Where does this line of reasoning come from? The program is not trusted because... I was the one who wrote it? Isn't the point of logic to be reproducible independent of who write it?
Gaslighting arguments are always used by people that are interested in another kind of discussion than the person who submits the original content. Let's say I made an error in some argument somewhere. This is natural. However, to claim the entire thing is generated by GPT, is unrealistic, you know it, yet you joke about it as if you expect other people to feel the same way you do.
This is logic, not about your emotions! I can't help it if my project rubs you in the wrong way. I try to provide more angles for people to make the learning curve a little easier to handle. Most people involved don't understand all of it, but they understand some parts to some degree such that the big picture seems a little more plausible than entirely wrong.
If you were willing to let me answers questions you might have, then there is a dialogue. Blocking me from that discussion is gaslighting. For example, I don't know which part you are confused about yet. Can you point to something concrete that you did not understand? Maybe I can help you find the external sources or get you in touch with people who might help you, if you are interested.
I can tell that you are not interested and not looking for a constructive dialogue. That was obvious from the first word in the first sentence in your first comment.
↑ comment by Viliam · 2023-03-23T22:31:51.040Z · LW(p) · GW(p)
Blocking me from that discussion is gaslighting.
No one is blocking you from discussion. The reason why you get so few responses is (my best guess) because no one here understands what you are talking about.
To put it bluntly, I am trying to figure out whether you are a crackpot. So far, your defense seems unimpressive to me.
What you do is supposed to be math, but it does not resemble the math as I know it. Words like "path semantic", "semantical qubit", "joker calculus", "Seshatism", "HOOO EP", it all seems completely made up. The only person on the internet who uses these words is you.
The paper that refers to you, is summarized as "Explorations of the relations between Inside Theories and Outside Theories of Sven Nilsen in relation to Sexuation of Lacan, the Antimonies of Kant and the deconstructive equations of Derrida as taken up by Zizek." That sounds to me like something written in a parallel universe, where math is considered a sub-discipline of literary criticism. Your most quoted sources are yourself, and Wikipedia.
It's not just me who is confused. Looking at r/rust, where you posted about your library, the reactions are: "I can’t even remotely parse this.", "Bro I have no idea.", "im so confused", "The document you linked is not published in any scientific journal and hasn't been peer reviewed. Scientifically, it is the equivalent of a blog post.", "It is literally a chain of thoughts, linking together completely unrelated concepts from a wide variety of fields without explaining it."
...actually, now I see that whatever I tried to tell you, someone else already did.
Anyone else who wants to join this debate, please read that Reddit thread first.
Replies from: bvssvni↑ comment by Sven Nilsen (bvssvni) · 2023-03-24T00:29:41.191Z · LW(p) · GW(p)
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.
↑ comment by Viliam · 2023-03-24T09:19:57.552Z · LW(p) · GW(p)
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.
One of us seems to be deeply confused about what math is, because I strongly believe that Gödel's Incompleteness Theorem is not about sexuality or castration. From my perspective, this is some alt-math; a postmodern misinterpretation of how math is actually used (hint: not to make complicated metaphors about penises). If this is actually popular in some branches of academia (which sadly doesn't sound unlikely), may gods have mercy on us.
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.
Someone who self-publishes on Academia edu (writing about topics such as: "Nine Men’s Morris Game as Structural Analogy for the Western Worldview", "Did Schelling Discover the Higher Logical Types of Being?", "Foundational Mathematical Categories and Passive Syntheses in Anti-Oedipus", "Exploring the Tetractys and what is Beyond at the level of the Site/Event and the Holon within the structure of the Emergent Event") is the endorsement for your mathematical theories?
Sorry, I previously wasn't specific, but when I asked for "a scientific paper written by someone else, referring to your paper or to your program", I assumed someone who does math, or computer science. Not a self-publishing philosopher who uses math as a metaphor for sexuality. Because I want to know whether your writing makes sense mathematically, and don't really care whether it can or cannot be used as convenient postmodern metaphor.
Could we agree that "math as known to and used by mathematicians" and "math as known to and used by postmodern philosophers" are simply two different things? And while your contributions may be novel and valuable for the latter, this website is about the former. Thus the confusion.
Replies from: bvssvni↑ comment by Sven Nilsen (bvssvni) · 2023-03-24T16:22:01.154Z · LW(p) · GW(p)
Maybe you can talk to Eric Weiser, who kindly provided me a proof in Lean 3: https://github.com/advancedresearch/path_semantics/blob/master/papers-wip/semiconjugates-as-satisfied-models-of-total-normal-paths.pdf
The experts in dependent types I know, think Path Semantics might help provide a better foundation or understanding in the future, or perhaps languages with some new features. We don't know yet, because it takes a lot of work to get there. I don't have the impression that they are thinking about Path Semantics, since there is already a lot to do in dependent types.
The reason I worked with Kent Palmer, was because unlike in dependent types, it is easier to see the connection between Path Semantics and Continental Philosophy. Currently, there is a divide between Analytic Philosophy and Continental Philosophy and Kent Palmer is interested in bridging these two.