Two Types of Ideas

In CTP Theory, there are two basic types of ideas (not including problems, which are treated as separate entities): claims and theories. Claims are simply instances of some kind of data structure that represent some proposition about the world, while theories are functions that take in one or more claims as inputs and return a claim as an output. I think this framework is productive in that it allows for a very rigorous explanation of how the implications of ideas can be explored: If using a set of claims C as an input to a theory T produces a new claim N, N is an implication of T and C (in other words, N can be derived from C and T).

While this division of ideas into two basic types provides a solution to the problem of how to compute the implications of ideas, it seems somewhat inelegant in that it doesn't solve any other outstanding problems in Critical Rationalism. Additionally, this division imposes an unfortunate limit on what kinds of ideas can be derived from other ideas. Theories always return claims, never theories, and so it's impossible for the mind to derive a theory as an implication of any other ideas. While I'm not sure that this limitation imposes any fundamental limit on what a mind working according to CTP Theory could accomplish, it is an unfortunate property, and I suspect that a mind could learn more efficiently if it did have some way to derive new theories as implications of other ideas.

Thankfully, I think there is a satisfactory way to modify CTP Theory so that there is only one type of idea, rather than two, while still maintaining a good explanation of how ideas the implications of ideas can be computed. This modification also, consequently, allows the mind to derive new theories from other theories.

Unifying the Two Types

In short, the modification involves defining a new, unified type of idea, which I will refer to as a "Unified Theory" or "U-Theory" for the purposes of this article, that has the necessary properties to serve the role of both a claim and a theory.

In the old version of CTP Theory, claims are generally meant to represent propositions about the world that the mind thinks to be true, while theories are meant to represent rules of inference for how to derive new claims from existing claims. A U-Theory is meant to be able to represent both of these things. A U-Theory can be interpreted either as a proposition about the world that the mind thinks to be true, or a rule of inference for deriving new propositions from old ones. A single U-Theory may even be interpreted as a proposition in some contexts while being interpreted as a rule of inference in other contexts.

On a computational level, claims are implemented as instances of some type of data structure. All claims in a mind use the same type of data structure, and the type of data structure used in the mind is an inherent property of that mind. Theories are implemented as functions that take in some number of those data structures as arguments, and return a new data structure. The output data structure represents the proposition that results when the rule of inference represented by the theory is applied to the propositions represented by the input data structures. To serve both of these purposes, U-Theories are implemented as instances of some type of data structure that can be interpreted as a function. When a U-Theory is interpreted as a function, it will take some number of other U-Theories as inputs, and will return a new U-Theory as an output. This output U-Theory may itself be interpretable as a function, which means it can serve the purpose that a theory would serve in the old version of CTP Theory. Thus, this change effectively gives the mind a way to derive theories from other theories.

Implementing U-Theories

U-Theories are instances of some type of data structure which can be interpreted as functions, but what might such a data structure look like? The programming language [Lisp](https://en.wikipedia.org/wiki/Lisp_(programming_language)) provides a nice example of how this could be accomplished, because code written in Lisp is treated as a data structure that can easily be manipulated by programs written in Lisp (see homoiconicity). Lisp is designed to make it easy to work with nested lists, and Lisp code is also itself composed of nested lists. So, it's very easy to use lisp to write higher-order functions, functions which take other functions as arguments and/or return functions.

There are various ways one could implement U-Theories, but one easy way to do it would be to simply have the data structure used for U-Theories be a nested list. When a U-Theory needs to be interpreted as a function the nested list can be treated as a Lisp function, but otherwise it can simply be treated as a normal nested list data structure, containing whatever data a claim might represent in the old version of CTP Theory.

Some nested lists don't form valid Lisp functions. Thankfully, this doesn't necessarily cause any issue, because the mind can simply refrain from invoking these U-Theories as functions. They can still, of course, be used as arguments to other U-Theories that are interpreted as functions. Such U-Theories are analogous to claims in the old version of CTP Theory, since they simply represent some data that can be used as an input to functions, but aren't themselves invokable.

In the old version of CTP Theory a mind needed to have some built-in rule that defined when two claims directly contradicted each other, in order to detect problems. In this new version, there still needs to be such a rule, but it needs to be defined for U-Theories, rather than for claims. In the past, I suggested that the data structure used for claims could be a pair consisting of a boolean and a list of integers. The inclusion of the boolean value allows for a convenient way of defining contradiction between claims: two claims are contradictory if and only if they contain identical lists of integers and opposite boolean values. A similar strategy can be used to define a contradiction rule for U-Theories: rather than just consisting of a nested list, a U-Theory could consist of a pair of a nested list and a boolean, and two U-Theories can be said to be contradictory if and only if they have identical nested lists and opposite boolean values. When a U-Theory is interpreted as a function, the boolean value can be ignored.

Solving Problems

In the old version of CTP Theory, the mind would find the set of ideas involved in a problem by tracing backwards from the two contradictory claims to the set of all claims and theories that were involved in their derivation. When attempting to solve a problem, the mind would do so by choosing some theory from that set and attempting to modify it, and finally checking to see whether the modification prevented one or both of the contradictory claims from being created. This approach worked because theories were always independent from one another in the sense that none was derived from any other, while claims were always derived as the consequences of theories (or were injected into the mind as representations of sensory input, but we can ignore that case for current purposes). This meant that directly modifying a claim would be a fruitless way to try to solve the problem, because the old version of the claim could just be derived again from the same theories and claims it was derived from previously. Every theory, however, is an independent conjecture that the mind has created, and so a theory could always be modified without any chance of the mind just re-deriving the old version again from some other theories. So, when trying to solve a problem, the mind could narrow down the pool of ideas that it should consider modifying or discarding by simply ignoring claims and focusing on theories.

Since this new version of CTP Theory doesn't involve a clean distinction between claims and theories, this approach no longer works. An idea's set of ancestors isn't cleanly divided into claims and theories, but instead consists only of U-Theories. Thankfully, there is still a way to narrow down the set of involved ideas in a productive way. This involves dividing U-Theories into two types: primary U-Theories and consequent U-Theories. Primary U-Theories are U-Theories which are created by the mind's conjecture algorithm, and thus aren't derived from anything, as all theories were in the previous version of CTP Theory. Consequent U-Theories, on the other hand, are U-Theories which aren't produced directly by the conjecture algorithm, but are instead produced as the outputs of other U-Theories. In other words, consequent U-Theories are those U-Theories which are the consequences from other U-Theories (either primary U-Theories, or other consequent U-Theories). We can use this distinction to narrow down the field of ideas that needs to be considered for modification when trying to solve a problem, in a way very similar to how that was done in the old version of CTP Theory: Only attempt to modify or discard primary U-Theories, and ignore consequent U-Theories. Consequent U-Theories are analogous to claims in the old version of CTP Theory in that even if they were to be modified their old version could be created once again if the U-Theory that they were derived from was invoked again with the same arguments. So modifying consequent U-Theories would be a fruitless approach to solving a problem, for the same reason that modifying a claim would be. Primary U-Theories, on the other hand, are independent in the same sense that theories in the old version of CTP Theory are: they aren't derived from anything. This means that if they are modified then there is no chance of the mind simply deriving them again, so changing them can solve problems in a genuinely fruitful way.

Whenever a theory was modified or discarded in the old version of CTP Theory, all claims that had been derived from it (or derived from claims that were derived from it, etc) would be removed from the mind, since they were consequences of a theory (or a version of a theory) that the mind has decided to reject. Though there are no more claims in this new version of CTP Theory, it is still important to remove the consequences of a U-Theory once that U-Theory has been modified or discarded. For this reason, whenever a primary U-Theory is discarded or modified, all consequent U-Theories that were derived from it (or derived from a consequent U-Theory that was derived from it, etc) will be discarded.

Closing Notes

The change I describe in this post is a significant departure from the way I've talked about CTP Theory in the past, and I think I need some way to distinguish between the older version of CTP Theory and this new version. The "CTP" in "CTP Theory" stood for "Claim Theory Problem", the names of the three main types of entities involved in the theory. Since the theory no longer includes the notion of a "claim" as a distinct type of entity, but instead unifies the notion of "claims" and "theories" into a single "unified theory" entity, I'll call this new version of the theory "Unified Theory Problem Theory" or "UTP Theory" for short. In contrast, I'll call the old version of CTP Theory "Non-Unified CTP Theory", or "NUCTP Theory" for short.

I have used the term "U-Theory" in this article to distinguish the new unified idea type that from the old notion of a "theory" in NUCTP Theory, but I do not plan to keep using this terminology in future writing, unless I am specifically discussing the differences between UTP Theory and NUCTP Theory. From now on, I plan to refer to U-Theories simply as "theories".

I have previously implemented NUCTP Theory, and the code for that implementation is available on github. However, after the changes to the theory that I describe in this post, that implementation is out of date. Further, I do not plan to update this implementation because it was written in python, and some version of Lisp would be more appropriate for implementing the new version of the theory. If I implement UTP Theory at some point in the future (which is not a priority because there are important theoretical problems with the theory that need to be solved before an implementation would be practically useful) I plan to implement it from scratch with Lisp.

Tags: AGI, Epistemology, CTP Theory