AdvancedResearch

Theorem Grading

by Sven Nilsen, 2026

We live in troubled times. However, we also can not let intellectual progress stagnate entirely.

In this blog post, I talk about nuances of truth and a reversal of the direction that Logic has been moving in so far: Up until now, Logic has discarded Sense, since the 18th- and 19th centuries showed that reasoning was independent of Sense.

In order to make further advancements in Logic, I argue, we need to bring back Sense as a language tool.

The current research in Path Semantics builds on a very solid foundation in Logic. It started with the core axiom of Path Semantics, but expanded over time to a set of building blocks I call Standard Path Semantics. There are some parts of philosophy, for example, if you are interested in Path Semantical analogues of Kant’s Transcendental Logic or early Schelling’s work on Nature Equals Mind, that fall outside Standard Path Semantics. Does not mean that the overall Path Semantics project fails to cover these topics, but that there is a Standard mode of Path Semantics, which is when Path Semanticists work in Path Semantics on a regular basis, with additional various Non-Standard Path Semantical theories outside that context.

Non-Standard Path Semantics means, that there is at least one axiom from Standard Path Semantics that is not assumed.

Standard Path Semantics is motivated by the need to standardize “normal” Path Semantics, the part of the theory that connects to all kinds of domains of human knowledge. With other words, it is a working theory, which is not going to change very much.

In addition, Standard Path Semantics is very important to understand, theoretically, how people use symbols in general. Naturally, there is a subset of theory that is more efficient at explaining things, than the average theory, while various philosophers also went beyond conventional ways of thinking. These philosophers’ works also have their place, but they are probably not going to take up a big portion of the central stage of thought.

My overall goal is to start a galactic civilization.

Starting a galactic civilization, has very little to do with designing spaceships. One can think about galactic civilization as a city, while spaceships are like buses moving around in the city. What makes a galactic civilization, or a city, work overall, is some levels of standardization and yet flexibility. It is about finding some balance, where there is enough equilibrium (in Game Theory) to establish higher levels of organization.

It is not like, a galactic civilization will emerge gradually as humans colonize other solar system. This idea, is very naive. Galactic civilizations operate on time scale that span billions, maybe even trillions, of years. Colonizing solar systems, is just one very early phase of this process.

A galactic civilization is probably not how people depict it in science fiction. The biggest constraint is speed of light, which forces communication to advance at a much, much slower pace than here on Earth. This introduces a new kind of danger, that without some form of stability, one civilization in one solar system might for seemingly arbitrary reasons, decide to attack nearby solar systems with weapons of mass destruction.

Such weapons are probably relatively easy to construct, but also very hard to defend against. Therefore, the strongest level of defense in a galactic civilization, is by using mathematics in communication.

With other words, the easiest way to keep interstellar peace in a galactic civilization, is to make sure, that it never gets to some point where there is a risk of potential conflict. However, how do we manage a such high sophisticated level of mathematical knowledge, without even understanding how basic Logic works?

The problem here, I argue, is that we do not really understand Logic as species, even at the basic level needed. If we don’t understand Logic, then it will be very hard to understand anything at all, except that occasionally, Logic seems to have real world applications that can be useful to people. If we do not understand why certain Logical languages work the way they do, then in my view, we lack the language tools to even start reasoning about things like galactic civilizations.

Why is there even something like Standard Path Semantics to begin with?

When civilizations advance in technology, they discover that Logic can be applied in more and more contexts.

One such example, is the Curry-Howard correspondence, that built a bridge between Constructive Logic and computer programs.

The Curry-Howard correspondence implies, that when we think about truth from a Logical perspective, this is linked to design utility in computer programs. Hence, there is no final answer to what is a “true” truth: There is no universal definition we can use. There are many definitions, but they might contradict each other due to pragmatic language design choices.

E.g. Quantum Mechanics and General Relativity are in contradiction: They can’t both be true descriptions of reality. Yet, we use them both very successfully, as long we are careful to avoid situations, where their differences become important.

When we construct computer programs, we assign semantics to the use of computer memory and how it changes dynamically over time. A computer, when the hardware is operating correctly, just does what it has been instructed to do. Therefore, it really matters, what context some computer operates under in the world. If there is no “true” truth, then we must decide what is the proper language tool in a given context by some scientific criteria.

It is more interesting and relevant to talk about language design, than about Logical truth in particular. Make no mistake: The entire motivation to develop Standard Path Semantics, is to get answers from Logic, about choices of language designs. However, overall, we are not interested in truth as such, not in the sense of Ontology in philosophy (the study of what is real). We are more interested in whether the computer programs will work in the real world and what their limitations are.

Path Semantics is the study of how people use symbols. This field is a sub-field of Semiotics. Unlike Semiotics overall, Path Semantics has a solid foundation in Logic. There are also other sub-fields of Semiotics that study how people use symbols, such as Linguistics, but Path Semantics is a more theoretical approach. In general, we distinguish Path Semantics from other fields by the criteria of the research having something to do with the core axiom of Path Semantics or not. If the research has something to do with the core axiom of Path Semantics, then we consider it Path Semantics. However, if the research does not have something to do with the core axiom of Path Semantics, then we don’t consider it Path Semantics. It just happens, that the core axiom of Path Semantics is central to understanding how people use symbols, hence touching on every known domain of human knowledge in existence, but seen from a more theoretical perspective.

Today, we do not even understand this connection properly, between the way people use symbols in general, and the core axiom of Path Semantics. It is just that the theory has been remarkable successful in making scientific predictions, that seem to hold over the entire course of written history. So, something tells us that we are on the right track, but we have not yet figured out all the pieces of the puzzle.

Standard Path Semantics is needed, simply because there are so many domains of human knowledge. If there was just one particular domain of human knowledge, then we could just develop some theory designed for that particular domain and ignore the rest.

In fact, this is what happens for every domain of human knowledge: It gets specialized. This specialization is part of the world economy, where production within one domain of human knowledge leads to economic activity. People can maintain economic activity and steady income, by contributing to specialization of some domain of human knowledge.

Path Semantics is not a sub-field of Logic, nor a sub-field of Philosophy, despite that it uses the most highest levels in prestige of these fields, just to form a basic foundational theory, so that people can get around to start doing actual Path Semantical work.

One can think about the work that a typical Path Semanticist does, as being a surgeon. A surgeon specializes on particular kinds of operations, but while the work itself, step by step, is pretty formal under normal conditions, a surgeon also needs to handle cases where the formal procedure is not sufficient.

This is what Standard Path Semantics is for: Standard Path Semantics is when you work on normal problems in Path Semantics, while Non-Standard Path Semantics is when you need to expand your work beyond normal and commonly used techniques.

Standard Path Semantics is not designed to do Logic in general, or Philosophy in general. It is designed to do Path Semantics on a regular basis. Kind of like, how Set theorists or Category theorists use their respective foundations.

Now, it turns out, that both Set theory and Category theory are very useful in many domains of human knowledge. Path Semantics adds yet another perspective, which is neither like Set theory nor like Category theory, except in a few situations where there is some overlap between these fields.

A specialist working in some field, might use results from some Set theory, some Category theory and some Path Semantics. This is not uncommon.

For example, Group theory, while being a relatively minor part of the total knowledge in mathematics, finds applications in all sorts of domains, despite that the theory is very narrow.

The same way, the foundation of Path Semantics is ridiculously narrow, even compared to stuff like Group theory. Yet, this ridiculously narrow domain of knowledge, applies to e.g. mathematics as a whole. This is because, people use symbols everywhere in mathematics.

In one perspective, Path Semantics is one of the most specialized fields in existence, but in another perspective, that mathematical knowledge it generates, is applicable to almost any domain of human knowledge.

Standard Path Semantics is a standard toolkit, that needs to cover all these domains of human knowledge. This high requirement, makes it very time consuming for Path Semanticists to check manually whether they can apply their particular version of Path Semantics across domains.

The goal of Standard Path Semantics, is that when people can prove something using Standard Path Semantics, that the mathematical knowledge generated is applicable across many different domains of human knowledge. With other words, this work is an enormous multiplier, something needed to start a galactic civilization.

Hooo: Building a standard implementation for the foundation of Path Semantics

One problem in the foundation of Path Semantics, is that existing language tools are simply not good enough.

Take for example, Dependent Type Theory, which is the basis for mathematical foundations in research related to Homotopy Type Theory. Path Semantics also developed largely from the first projects in Homotopy Type Theory, plus Adinkra physics, a sub-field of mathematical physics of Supersymmetric extensions of the Standard Model. Instead of focusing on foundation for mathematics as a whole, the Path Semantics project sought to research one language mechanism, normal paths, that did not work well with Dependent Type Theory. So, from the very outset, Path Semantics was focused on solving problems with existing language tools.

The problem of formalizing normal paths properly, resulted in research on Meta-Parsing, a technique used to invent the modern computer before C became industrial standard as system programming language, just to get to a level where the syntax needed in Path Semantics could be studied through program implementations.

We are talking about very basic challenges in overcoming problems with existing language tools, that needed building on the cutting edge of research in computer science. This was just to get something working, so further progress could be made.

That’s a typical pattern in Path Semantics: The research pushes the limits of what has been done previously in other fields.

Despite that Path Semantics is centered around research on one specific language mechanism, it needs to overcome challenges, that are considered extra-ordinary advanced, in fields that are already very difficult to learn. However, despite these challanges, we have not stopped making progress in Path Semantics so far. In fact, there are many breakthroughs in Path Semantics that, if they were not so commonly made in this field, would be treated as among the most important breakthroughs ever made, in other fields.

We do not understand currently the reason why research in Path Semantics is so effective, but we will keep doing it, as long it brings new results.

However, we do have some solid understanding why Path Semantics is the only field that can do certain things at the moment. This does not explain the frequency of the breakthroughs compared to the research effort (which is basically zero, compared to any other established field in Science), but it does explain why other fields are not making these same breakthroughs.

For example, we have solid evidence, that certain critiques of Logic can only be made currently, from a perspective of Path Semantics.

The research on Logic that came from the Path Semantics project, was one of the reasons why there is now a foundation in Logic to build on when doing Path Semantics. In Path Semantics, there is a core axiom, which led to various breakthroughs in Logic that shaped up the theory of its foundation. The core axiom is now fully formalized, but we need proper language tools to be able to reason about it. There is no exaggeration, that the research on the foundation of Path Semantics, is centered on the core axiom. What we are trying to do, is to advance language tools so far, that we can begin doing more complex things with it. So far, we have learned many small things from working on the core axiom, but these small things have been major breakthroughs in Logic and Philosophy. This progress looks very promising. If we can get some language tool good enough for sustainable research, then there are good chances that we will get into more depths of Path Semantics.

Right now, the most promising language tool for this planned sustainable research is Hooo.

Hooo is designed from the ground up, to make it easy to maintain source code that produces theorems in constructive propositional logic. Here, we are not trying to do something very clever, such as building in an automated theorem prover, but to focus on making the source readable and checkable for every step, yet also without over-burdening the people who write these proofs.

We have taken inspiration from Metamath, that formalizes a huge amount of standard mathematical theorems. The strength of Metamath lies in its simple design. However, we can not use Metamath the way it is designed, to do Path Semantics. So, a new language tool is required.

Hooo’s design has some new ideas in it, such as dropping for-all quantifiers in the favor of symbolic blocks. This means, that people can write statements pretty straight forward, the way they would do in Logic.

As a result of its design choices, Hooo can in general be a good tool for Logicians. While this is not an explicit goal, it is possible that either Hooo or some similar tool will become popular in this field. Now, there are other tools available for doing lots of Logic, so it is preferrable if people use these tools when possible, to not over-burden the people who are working Hooo for its primary purpose: To serve as a standard implementation for the foundation of Path Semantics.

Theorem grading: Why Sense is brought back as a language tool

The mechanism I’m working on in Hooo (a theorem proving assistant for constructive propositional logic), to deal with the need to handle complexity of perspectives of mathematical language design, is theorem grading.

Theorem grading let’s you list axioms by strength, measured by the grading:

grade <name> [<axiom 1>, <axiom 2>, ...];

The basic idea here is that we don’t use Logic in the sense of Hooo, to reason about just one theory. We want theorems to hold for as many theories at the same time. However, it is too difficult to maintain separate projects for different theories. We want to use one knowledge base and reuse it.

If somebody needs something special, then they can copy the knowledge base and modify it. The default knowledge base will be a standard library for Hooo, that follows with the tool, without needing to add it as a dependency to your project. However, the standard library is completely optional to use. When you want a completely different knowledge base to use in your own research, you can do so too.

In addition to the standard library, there will be additional knowledge bases, designed for particular domains, that can be downloaded and added as dependencies.

Theorem grading is intended to work on a very simple principle: When you work with projects in Hooo, you create a project file. If you don’t have a project file already, then Hooo will generate it the first time you run a check on your project folder. This project file, contains both information that you give to Hooo, but it also gets modified by Hooo that reports the result.

Basically, there is no other input/output needed than the project file. When you add another project as a dependency, Hooo only reads the project file and uses the knowledge about the theorems that is available there.

With other words, Hooo does not run a full check of project dependencies, but only sees what is in the project file. Currently, there is no other information in the project file than some information about the project, theorems and dependencies.

The information used in theorem grading, will be put in the project file, which will then propagate as dependency to other projects. For every theorem and every theorem grade, there is a grade. Most theorems have grade 0, because they usually don’t depend on some axioms in the list, so this grade will not be shown in the project file. We know these theorems have grade 0, because all the other theorems with higher grades are listed.

Here is how grading will look like:

grades {
     exclusive_strength: { ... };
     meta_strength: {
          1: [pow_lift, ...];
          2: [tauto_hooo_imply, ...];
          3: [tauto_hooo_tauto_or, ...];
          4: [tauto_hooo_or, ...];
     };
}

There will be a list under “grades”, one item per theorem grade, that shows all the theorems listed per grade, starting from 1 and counting upwards to the end of the theorem grade list.

For example, meta-strength 4 means that the theorem might depend on 0-3, plus the 4th axiom in the theorem grading list.

grade meta_strength [pow_lift, tauto_hooo_imply, tauto_hooo_tauto_or, tauto_hooo_or];

One can think about theorem grading, as adding dimensions to truth. When you just ignore the gradings, you are thinking about truth in a constructive sense only. A constructive sense only, or formal sense, is only sense that has been kept in Logic, since people figured out in the 18th- and 19th centuries, that Sense was independent of formal reasoning. So, when I say Sense here, I mean that there is more than just one Sense being used. Because, in general, we do not think about formal sense as an “actual” form of Sense, but more like a 0-Sense.

You can think about 0-Sense as an absence of Sence. How you interpret it, is completely up to you, because how humans construct meaning, is by assigning it to symbols. I can’t tell you what is correct, to think of 0-Sense as an absence of Sence, or as the first Sense. To me, both these ways of thinking are meaningful. The interpretation does not change how Hooo works, so it is up to you to do whatever that fits with your own brain.

There is a reason for choosing 0-Sense as an absence of Sense, because it got to do with the relationship between universals and particulars in Philosophy.

Sense as theorem grading: Knowledge about particular theorems

Let’s say, we have a theorem with a name foo.

Here, I just picked the name foo, because we do not actually care what kind of theorem foo means. The label foo is not the propositional truth, but the label we use to refer to that proposition.

The thing is, what makes something a proposition, is that all proofs of that propositional are equal to each other. It does not matter what the proof looks like, as long it produces the same theorem as a result.

For example, foo and bar might be two different theorems, but they have the same propositional truth.

From the perspective of Logic, foo is indistinguishable from bar in every context.

However, in practice, foo might be easier to check for a computer than bar. Although foo is logically equivalent to bar, there might be other aspects that we humans care about in practice.

To distinguish foo from bar, e.g. because we want to think about what makes foo more useful to us than bar, we need some form of particular knowledge, that can be used to inform us about these particular theorems.

In most practical applications of Logic in the real world, we need some form of particular knowledge. That is because, when things become complex in the real world, we can usually tell, by trial and experiment, two things that are logically equivalent are not the same thing in practice. This particular knowledge is Seshatic biased.

Seshatism credits knowledge by causality. Because two logically equivalent things can be different in practice, this is a causal significance, for example, when we expect a computer program to terminate.

As long as we constrain our own thinking to reason about whether computer programs terminate or not, we are still operating within logical equivalence. Logical equivalent computer programs have the property that both will terminate, eventually, or, neither will terminate.

However, as soon as we ask when some particular computer program terminates, we enter an entire different domain of knowledge overall. One can think about Logic as Platonic biased.

Platonism credits knowledge by abstraction. Abstraction can be thought of as some computational process, that erases all particular knowledge. When this computational process terminates, the knowledge that is left is universal.

When we reason about computation, we have both aspects of causality and abstraction to think about. Furthermore, the causal aspects have also causal and abstract perspectives. Vice versa, the abstract aspects have also causal and abstract perspectives. You can also have, some causal aspect that looks like an abstract aspect on the surface and vice versa. These two basic operations, perspective and layer, are basic binary operators to construct higher dualities of language biases in Joker Calculus, where the two fundamental language biases are Seshatism and Platonism.

Joker Calculus helps us to express, what kind of language bias we use. It’s like, Joker Calculus moves the camera, but the world itself might remain unchanged. However, since Static and Dynamic are also just different perspectives, depending on the frame of reference, it is possible to move the camera in a such way, that the world itself appears to have a different structure. With other words, knowing which language bias we use in some context, can help us to make Sense of things, as a language tool.

Now, when use Joker Calculus, we can make Sense of things, precisely because the language bias we use is extra-logical. It is not something that Logic itself deals with normally. Except, when you add more dimensions to normal Logic, you are free to encode such Sense into these extra dimensions, and reason about Sense in a formal setting.

In Path Semantics, we study what happens, when we “open up” these higher dimensions. This is because, the basic mechanism in the core axiom, path semantical quality (or equivalently: path semantical qubit), can be thought of, as turning normal Logic into infinite-valued Logic in Standard Path Semantics.

We reason about Platonism and Seshatism with respect to the core axiom of Path Semantics, but in a such way, that there is no one-to-one mapping to expressions in Joker Calculus. Only the two fundamental language biases in Joker Calculus can be directly translated to the Logic.

However, since Seshatism (!(a ~~ a)) and Platonism (a ~~ a) already is at the side of “opening up” toward infinite-valued Logic, it is possible to vaguely relate these higher dimensions to Sense in general. For language bias specifically, we might need to find some higher dimensional “island” that casts a shadow down to normal Logic, but corresponds to some language bias, without necessarily a such language bias being reflected by some expression in Joker Calculus. Currently, we have not explored these “islands” out there to any significant degree, only a few of them have been explored. Like, we have only studied a handful, but there are millions of such islands, even in the first level. Each level adds a tremendously amount of number of new islands, that after a few additional levels, we have no hope to ever explore them all. This means, we need to distinguish Sense in general, from language bias. Language bias can take on particular interpretations in different formal languages. Sense is more vague, but overall, got something to do with higher dimensions.

Now, it turns out, that Sense, while still being a very vague concept, can be sufficiently used, since we can think of theorem grading as adding new dimensions.

The question is: What kind of knowledge does the Sense, in the form of theorem grading, gives us?

It turns out, that this is particular knowledge.

With other words, we can distinguish foo from bar, using theorem grading.

Constructively, foo and bar can be logically equivalent. However, when we add theorem grading, we get a new language tool, such that we can say something particular about foo that does not hold for bar and vice versa.

Sense has been excluded from Logic since the 18th- and 19th centuries. However, now the direction is reversed: We are bringing Sense back as a language tool.

Advancing Logic further: Why we need to bring Sense back as a language tool

Theorem grading solves a particular issue in Path Semantics, were we are reasoning about theories across many domains of human knowledge.

However, because we also know that theorem grading necessarily leads to bringing back Sense as a language tool, where Sense gives us particular knowledge, it follows a research question, whether we should thinking about advancing Logic in general this way.

I argue, yes, we should think that way.

As an example, I am going to demonstrate this about one of the most important results in Logic ever: Gödel’s work on incompleteness of mathematics.

Gödel showed that mathematics was either incomplete or inconsistent. However, the meta-theorem technique Gödel used in his proof, is among Path Semanticists not accepted.

A Gödel sentence about arithmetic is a parameter-free predicate. The choice of encoding in Gödel’s proof introduces circular problems.

Now, Logicians might object to this critique of Path Semanticists, because they can argue that Provability Logic covers the notion of provability used in Gödel’s proof.

However, Path Semanticists do not accept Provability Logic either. According to their notion of provability, Löb’s axiom is absurd.

Path Semanticists use HOOO EP, a meta-theory that allows propositional logic to include both meta- and object language. HOOO EP captures the essence of meta-theory in Constructive Logic (IPL), based on function pointers as the underlying mathematical objects using the Curry-Howard correspondence.

Provability Logic is from the perspective of Path Semantics just a theory in Modal Logic, which can be modeled using HOOO EP. With other words, the entire field of Modal Logic is just a sub-field of Path Semantics, which plays a minor role in the foundation of mathematics. Just an Avatar-extension.

Now, there are very valid reasons to treat Modal Logic as a separate discipline from Path Semantics. One should not think about Path Semantics as a final answer, but as a perspective. So, from the perspective of Path Semantics, Modal Logic as a whole has a specific natural interpretation.

The natural interpretation one gets of Modal Logic from the perspective of Path Semantics, enlightens our understand of Modal Logic and in particular Provability Logic, that there are subjective choices in mathematics when giving semantics to notions of provability.

Path Semantics is not Logic. For example, Modal Logic is not “part” of Path Semantics, but a theory. Path Semanticists call it an “Avatar-extension”, using the language of Outside theory.

Neither is Path Semantics philosophy of mathematics. Path Semantics has no Ontology, as far we know today.

Despite that Path Semantics uses some parts of Logic at the highest level in the world, and it also uses some parts of Philosophy at the highest level in the world, Path Semantics itself is not regarded as either a sub-field of Logic, nor Philosophy.

Path Semantics is a sub-field of Semiotics.

As far as we understand Path Semantics today, it is a sub-field of Semiotics in the sense that Path Semantics is the study of how people use symbols. Semiotics is the field that studies signs, where symbols are a kind of sign you can’t learn just by looking at them. You have to be instructed to know.

With other words, the critique of Gödel’s proof that mathematics is either incomplete or inconsistent, is not accepted in Path Semantics because it uses (according to their theory) a “wrong” notion of provability, that is merely a theory in Modal Logic.

Now: Is mathematics incomplete?

Can Path Semantics show that mathematics is incomplete?

There is a proof in Path Semantics, that when you add HOOO EP (meta-theory) to IPL (Constructive Logic), you can prove that IPL is actually an EL (Existential Logic).

An Existential Logic, is stronger than Constructive Logic.

In Classical Logic, it is true that for all a:

true -> (a | !a)

One can also write this as (a | !a)^true.

The above is expressed in HOOO EP.

This is not provable in Classical Logic, nor Constructive Logic.

Why? It is impossible to express the idea in these languages.

What Logicians normally do, is appealing to a meta-language, usually Sequent Calculus, where the sequent:

|- (a | !a)

Is provable from the axioms of Classical Logic (this is often a trivial proof, because it’s usually one of the axioms).

Therefore, when people talk about what Classical Logic means, which is the basis for stuff like binary encoding of information in digital computers, they have two choices:

  1. Use something like Sequent Calculus
  2. Dive into Path Semantics and HOOO EP

So, it’s a really basic choice.

With other words, just to express what we even mean about Classical Logic formally, so we can reason about it formally, requires meta-theory.

Consider here, that if you pick 1) you usually accept the doctrine of Gödel and Provability Theory.

If you pick 2) you go with Path Semantics.

It is a very basic problem, that as soon as you start thinking formally about something as simple as Classical Logic, you are forced into choosing of notions of provability, that might seem very esoteric on their own in isolation.

These choices are not really esoteric. They are very fundamental choices.

It’s not like, you are going to solve this problem by spending a few days thinking about it. There are very strong reasons to believe, that you either accept doctrine that is handed down the mathematical tradition, without any justification except making arbitrary language design choices, or:

You embrace the Path Semantical perspective.

There is no justification in the mathematical tradition of why one chooses this particular notion of provability that Provability Logic gives you. So, if you want to follow the evidence, then there is only one option at the table:

Path Semantics.

With other words: There are nobody else but Path Semanticists in the entire world, that are critiquing fundamental results about mathematics that are otherwise almost universally accepted, based on a purely formal basis. If you become a Path Semanticist, then you choose to stand outside the normal mathematical tradition.

It’s not like, Path Semanticists are just doing nonsensical work. On the contrary, it is even more rigorous work than the level a normal Logician, let alone a normal mathematician, is expected to perform.

Path Semantics is the only field that can critique what we’re doing. That’s why it’s useful.

You can argue that, ofc, Path Semantics is about the study of how people use symbols as a whole in general, from a theoretical perspective. So, when we apply language designs in e.g. Logic, we are working in a limited context and don’t have to worry about Path Semantics.

That’s correct.

Actually, this is how people use symbols in every field of Science. Not just Science, but in every part of civilization that uses symbols, we apply symbols in a limited context.

Only when you’re reasoning at the civilization level, you need to start worrying about Path Semantics.

So, back to Classical Logic:

Classical Logic is the very basic language tool of all modern technology. So, right there, we’re taking a very broad perspective.

Now, there is an even more basic language tool: Constructive Logic. It’s even more important, than Classical Logic.

Constructive Logic is important for stuff like computer software, where type systems use Constructive Logic to ensure that some aspects of computer programs are safe.

There are weaker languages than Constructive Logic, e.g. Linear Logic, but when you do that, things start to get complex again.

Constructive Logic has a nice tradeoff between complexity and utility. It is not as simple as Classical Logic, but it is easy to either add an axiom (a | !a)^true for all a, or, prove some statement p as !!p.

Any theorem p in Classical Logic holds in Constructive Logic in the form !!p.

Now, an Existential Logic, is a logic where:

true -> (!a | !!a)

Or, written: (!a | !!a)^true.

Existential Logic was first developed in the Path Semantics project. It was discovered, before it was proven that Constructive Logic is “really” an Existential Logic under HOOO EP.

With other words, Path Semanticists discovered, that when you actually use the correct notion of provability, HOOO EP, according to their own theory, Constructive Logic itself becomes another Logic, which nobody had even heard about before Path Semanticists started thinking about this stuff.

The idea that you can only critique what people are doing with symbols in Logic, or in general mathematics, from a perspective of Path Semantics, is simply because there is no other way to make a such choice that you can reason about justification of language designs formally. It is not a such shallow idea that you might think at first.

There is only Path Semantics that does these kind of breakthroughs in recent years. Not a single field in entire Science is competing.

With other words, Path Semanticists have now some kind of monopoly. It can and should be ignored most of the time, but right now, there are no other ways to achieve such a critique formally.

The question is:

Should we interpret the proof that Constructive Logic (IPL) is “really” an Existential Logic (EL) under HOOO EP, as the truth that mathematics is incomplete?

Path Semanticists are like: Depends on your perspective.

That’s very unsatisfying, right?

It’s like, you have been on this pilgrimage to learn the secrets and the truths of existence, the universe and everything. You finally meet somebody that can give you an answer. However, they say something like:

“Well, if you like to. That’s just your opinion.”

Incompleteness is very weird.

Incompleteness is the property, that not all true statements are provable in an incomplete theory. The statement (!a | !!a)^true is not provable in Constructive Logic (IPL), so if that statement is true, then by logical consequence, IPL is incomplete.

Path Semanticists are not vague here.

You would think, that when Path Semanticists give a such answer, that they are just bullshitting you. However, it is an answered that is based on a lot of research.

There is the Curry-Howard correspondence, that says Logic and computer programs are two perspectives of the same theory.

If you are biased toward Logic, then you might think that, there is only one “true” truth about (!a | !!a)^true.

The problem is, there is another perspective: Computer programs. In this perspective, it is often desirable to have some notion of privacy.

Privacy is the motivation of abstraction.

Whether it’s privacy in nodes of a network, that helps to increase the overall security (everybody knows that too much surveillance is extremely unsafe and those who advocate for it are abusers) or whether it’s a module, or a class in programming.

All this is based on the idea of privacy.

Without privacy, there is no distinction between being in coma and being alive. When you remove privacy gradually, people who are seemingly alive start to exist in a way that is similar to coma, and vice versa.

When you remove privacy entirely, there is only existence left.

Existence without life.

In Star Trek, the reason The Borg is so terrifying, is not because The Borg kills people. The Borg transforms them into something people are not. They are terrifying as an enemy, because people are scared of losing the way they are existing, not their lives. People fear losing what is most characterizing of their way of life, no matter what kind of species they are, despite all their differences, which still is significantly different from The Borg: Privacy.

Privacy is fundamental for life.

In Existential Logic, every proposition has the property (!a | !!a)^true for all a. It can be interpreted as everything being either dead or not-not-dead. However, this not-not-dead is not the same as something being alive.

In Classical Logic, every proposition has the property (a | !a)^true.

You can interpret it as everything being either alive or dead. There is nothing in between. So, whatever you think makes something alive, in Classical Logic, is kind of like, it must happen, as long it’s not dead.

The HOOO EP axioms remove privacy from Constructive Logic.

It is simultaneous true that, if you knew absolutely everything about Constructive Logic and there was no notion of privacy from your perspective, that Constructive Logic would appear to you as indistinguishable from Existential Logic, but also, this is just a perspective.

For example, imagine you are an all-knowing deity, that exists before time in the universe has started. You are thinking about all that will happen, before it happens.

This is just a perspective.

Even if a such deity existed, then it would not make the universe real yet, just by thinking about it.

Aristotle thought, that the world itself, the cosmos, was produced by a deity that was pure thinking. A pure activity of reasoning. Remember, Aristotle doesn’t know about computers, so he uses thinking to describe reasoning.

What happens in the world, to Aristotle, was thought, in a higher reality.

However, Aristotle was a student of Plato. Plato tried to unify various mystery religions into one coherent philosophical system. Plato’s idea was that when you experience something, e.g. seeing a color, you were participating in a “communion” with the divine. The color experience, is a universal.

There wasn’t really a big disagreement between Plato and Aristotle in the way later philosophers thought about them. The way Plato thinks about Platonism, is actually Platonic Seshatism, continued by Spinoza. It’s a dual-Platonic position from the perspective of Platonism.

Platonism never existed.

Platonism, the way modern philosophers think about it, is just an idea, that people pretended exist sometime, supposedly invented by Plato and later developed into a modern form.

In this modern form, Platonism is so useful, that we can’t let it go. Just too useful, right?

Doesn’t change history.

Platonism has never existed in history, as any doctrine of philosophy that was pushed by some thinker.

Now, some Medieval philosophers invented another position, to object to what they thought of as Platonism, which they called “Nominalism”.

The problem is, Nominalism is not dual to Platonism.

Path Semanticists say that Nominalism is only another version of Platonism, where you assume stuff in a particular way, that has no basis in Logic. It’s just a way of making assumptions, that way is not expressible from within Logic.

That’s why, Seshatism, not Nominalism, is dual to Platonism.

Platonism never existed. However, it was credited by philosophers as having existed.

Seshatism actually existed as a philosophical framework, used by scribes in Ancient Egypt during the Bronze Age. The name comes from Seshat. A goddess that was forgotten.

Seshat is making a return in modern time.

Seshat was a goddess of writing, knowledge and science. Her symbol was the hemp plant. Such symbols were used in wall paintings and reliefs, so people could recognize characters from an artistic system around “Stretchable Book of The Dead” that could expand, depending on artistic constraints.

For example, if an artist had a 10m wall, then they would include fewer elements than if they had a 20m wall.

However, when these stories were written down on papyrus at the end of the Bronze Age, people wrote down the shorter versions. They got copied more often and became canonical over time.

Seshat was a goddess that functions kind of like an artistic filler, when an artist had very good space, they included Seshat because they needed to put something on the wall. Scribes liked Seshat, so she was one of their favorites.

For example, at the backside of the throne, an artist put Seshat.

Few people were ever going to look at the backside of the throne. It might be even the case, that Pharaoh never knew, nor cared, what was on the backside of his own throne.

However, if there was nothing there, it would look strange when people moved furniture around. So, the artist put Seshat on the backside. She was a “filler”.

However, in such spaces, where artists filled in with their own favorite goddess, they expressed their own art. Seshat in this sense, was not something to be worshiped officially, she doesn’t appear to have any dedicated cult in archeological records, but she was a “Muse” for artists and scribes.

The word “Muse” comes from a later time period, when this idea of a personal guiding goddess for artists and scribes was fully developed. That idea did not exist when Seshat was at her height in the Bronze Age.

Unfortunately, when people started to write down these stories on papyrus:

People removed what made artists express their own creativity in the written versions on papyrus, because they thought, it was the official story itself that was important. They didn’t think about the papyrus version as a description of some particular artwork with complete illustrations.

So, when there was no longer space for Seshat, she vanished.

Despite being a goddess of writing, knowledge and science, Seshat vanished almost completely from the records.

These ideas were only passed on through Thoth, which was the male deity. Just one half of the story.

You see, the Ancient Egyptians developed a system, where their philosophical ideas were told in two versions: A female version and a male version. They used this system as a kind of check-and-balances of power with respect to gender:

Ancient Egypt had better rights for woman than most places.

Seshat’s mother, Ma’at, represented balance and justice.

So, the idea was, Ma’at means to treat men and women as equals, by giving children stories that are not meant to be passed on individually, but as a whole.

A library.

Seshat was the goddess of the library.

Amazingly, these ideas, that the whole Western philosophical tradition proudly are claiming as the basis for their entire system of literacy, existed in some form in Ancient Egypt, was lost because they didn’t include these artistic spaces, the fillers, of art when they recorded them down on papyrus.

There was no “canonical” Book of the Dead originally. It was an artistic system, designed to be expanded and fit on various architectures. As an artist, you were trained to recognize the important elements in the story, but also to fill in with more events and details when you had more space.

When people didn’t include the illustrations of Seshat on papyrus, they also didn’t include her in the text. Because, if you mentioned a goddess in the text, people expected to find her somewhere in the illustrations, right?

Seshat was censored out. Later, this censorship became canonical.

If some artist tried to use more papyrus to bring back Seshat, then they would have been criticized as wasting expensive writing materials, to make up a new unholy religion and to challenge the authority of the state.

However, on the wall: Ofc, Seshat had to be there! She was in the filler art.

So, you can see, that it’s only a matter of perspective.

In the same way, if Aristotle’s deity thought about the world, instead did it before time itself, before the universe existed, then there must be something making the universe “real”:

A filler.

A private space.

In that filler, we are.

So, not only did this philosophy fit with explaining how Seshat vanished from written records, to a such extent, that when Plato wrote about Thoth, he either forgot Seshat or didn’t even know about her.

It also explains the perspective of the way we exist: As alive.

When you’re in a coma, you exist, but you are not actually living here, with us. When you fall asleep, you are not living here, with us.

To live here, with us, you need to wake up.

So, life is the process of waking up to reality.

That’s the difference between thinking and being.

Descartes “Cogito, ergo sum” can be translated as “I think, therefore I am”, but you can also go back to Parmenides, the surviving 160 lines and find a similar idea. To Parmenides, thinking and being are related.

However, existence is not the same as living:

“I think, therefore I exist”

This is only one part. That’s just one half.

Here’s the other half:

“I wake up, therefore I live.”

Together, changing “think” to “dream” to make it more poetic:

“I dream, therefore I exist. I wake up, therefore I live.”

As a whole, they produce more harmony. A deeper insight.

Right?

As I said before:

Path Semantics is the study of how people use symbols.

When Path Semanticists give you answers that seem vague, it is not because they have a bad understanding of reality. They are not studying reality, or Ontology.

Path Semantics is the study of how people use symbols.

Sense is useful, because it allows us, to form particular knowledge in Logic. Whereas, Logic so far, has been used to represent universal knowledge, we have to bring Sense back, to advance further.

We can go up into these higher dimensions of Logic, and encode the structure of Sense formally. In the first dimension, we keep the same formal 0-Sense as before. This way, we keep the backward compatibility with 18th- and 19th centuries philosophy of Logic.

When we use theorem grading in Hooo, of course it needs to be based on constructive truth, otherwise it is not very useful to assign some grade to a theorem. Truth must come first.

However, that said, we might reformulate the way we are thinking about theorems, that some particular theorem might not always be true, but only hold in some specific contexts.

This is possible, because we use Sense here to think about things.

Let’s say that foo can be proven without using any axiom listed in any theorem grading list, but it is logical equivalent to bar that has a non-zero grade. Here, one can argue, that foo is better than bar, since foo is a universal truth, while bar is merely a particular truth. The theorem foo is more applicable, since it can be used without increasing the grade of theorems that depends on it.

Now, if we later modify the source, such that a new theorem grading is added, then we can make foo less useful than bar overall.

Therefore, Sense can change over time. Sense does not require a static meaning. The constructive truth can remain static, while changing Sense relative to it.

With Sense, it is possible that Logicians need to start thinking about how it will change over time. Most Logicians might stay close to eternal and static truths, but some of them might venture on into a mental world, where change is important part of their own work.

Sense can lead to situations where people are deceived by Logic, not just shown a path toward truth. However, the way people get deceived, is in Sense, not in truth. That’s why, I think a such form of deception is an acceptable risk to take.

Without taking risks, we are not advancing Logic.

Bring back Sense as a language tool.