A Basic Hyperlogic

My search for the proper logic is guided by the requirement that desired meaning of the logic must be reflected totally in the rules of inference. This is a form of something called grounding. The idea behind grounding is, roughly, that in order to have a meaning, a symbol needs to have a proper connection to what it actually refers to. This is sometimes used in the AI community to argue that robotics is absolutely required for AI, because an AI shunting symbols around on its own inside computer cannot really "know" anything (its symbols have no meaning). This is idea is also known as embodies intelligence, or situated cognition. The form of grounding that I'm talking about is somewhat different: I want a way to ground logical and mathematical concepts. Mathematical grounding must exist, because humans are able to refer to mathematical entities, and understand mathematical meaning. My aim is to figure out how.

I've discussed the inadequacy of current mathematical logics in the past. In that post, I also made some wild speculations about creating a logic based on "limit computers" and even more powerful machines, . Basically, this post is a revision of those speculations based on some solid facts.

Limit-computers, as well as more powerful imaginary machines, are called "hypercomputers". Similarly, I'll call the logics that match them "hyperlogics".

To measure the power of a hyperlogic, I'll use something called the arithmetical hierarchy. Very approximately: the first level of the hierarchy contains all computable facts. (So for example, it contains the fact that 3 + 4 = 7.) The second level contains facts either of the form "for all x, P(x)" or "there exists x such that P(x)", for any computable predicate P. Notice that we may need to check an infinite number of cases to decide the truth of these facts, but we may not. If the fact is a "for all" fact, then we may run into a case where P isn't true; we have a counterexample, and are done. But if we never find a counterexample, we would never finish checking the infinite number of possible values for x to conclude that P was true everywhere. Similarly for "exists": we can stop if we find a true case of P, but we would need an infinite amount of time to conclude that none exists.

The third level of the hierarchy is the same, except that it takes P to be second-level, rather than first-level. This means we need to check a possibly infinite number of second-level statements to decide a third-level statement. (But remember, we may never finish even the first of these, since checking a second-level statement can take forever.) Similarly, each level contains those statements that can be verified by looking at a (possibly) infinite number of statements on the previous level. (Nice fact: each higher level can be decided by an infinite-time Turing machine given one more infinity of time.)

Mathematical truths beyond the second level cannot be logically determined, because no logic can check them. Yet humans can talk about them. So, the goal is to specify a logic that tells us how to reason about facts on these levels. The logic cannot possibly tell us whether these facts are true or false for sure, beyond facts of the 2nd level. I'm just looking for a logic that does the best it can. If we do the best we can to try to ascertain the truth of a statement, that should ground us, right? Intuitively, the idea is that some external observer looking into our thoughts (or the inner workings of our AI) should say "Oh, this symbol here must represent mathematical entity X, because it is manipulated the way entity X should be manipulated." Ascribing that meaning to the symbol is the best way of explaining the manipulation rules attached to it.

So: for 1st-level statements, use the method of computation. For 2nd-level statements, keep checking 1st-level cases until a deciding case is found, or until we're satisfied that there is none. (This reflects the scientific method: if a hypothesis escapes our best attempts to disprove it,we conclude that it is true.) For a third-level statement, test the 2nd-level cases until a decisive case is found, or until we're satisfied there is none. (Notice: the meaning of "decisive case" is weaker here, because our conclusions concerning 2nd-level statements are not entirely perfect.) And so on. This gives us an approximate decision of the truth of any statement on any level of the arithmetical hierarchy.

It may seem like I've left out some important details. To fully specify the decision method, I should specify how time is to be distributed between cases when checking. For example, on the third level, I could check many 2nd-level cases shallowly, or I could check a few deeply. Also, for higher-level statements, since the so-called decisive cases are not entirely decisive, it might be worthwhile to seek out more than one. If several were found, how should we represent the increase in certainty? These are important questions, but not too important. The statements in question are fundamentally undecidable, so there can't be a really right answer. Any particular technique will fail in some cases. The only thing that can definitely be said is: the more time we spend checking, the better. So I feel I am somewhat justified in leaving out these details, at least for now.

This hyperlogic is nice, but there is a reason this post is titled "a basic hyperlogic". The arithmetical hierarchy does not cover all mathematical truths. So the quest isn't over. But I think this is a good start. I've got a concrete example with a good mathematical foundation, showing that it is possible to create systems more powerful than 1st-order logic for AI.