New Grounding Results

In this post I detailed a different (and hopefully better) grounding requirement for an AI logic. I've now come up with a logic that satisfies the requirement, based on the speculations in that post.

This logic is nicely simple. All I do is add lambda calculus to first-order logic. The lambda calculus is used as a new way of notating terms, acting like function-symbols act normally. The difference is that lambda-calculus is able to uniquely define computations, while normal function symbols cannot.

The reason first-order logic cannot uniquely define computations is that it cannot rule out nonstandard interpretations. Let's say we try to define some method of computation (such as lambda calculus, Turing machines, etc.). Determining the next step in the computation is always very simple; it wouldn't be a very useful definition of computation otherwise. And since a computation is nothing but a series of these simple steps, it might seem like all we need to do is define what happens in a single step. Once we do that, the logic knows what to do next at each stage, and can carry any particular computation from start to finish without error.

The problem here is that we are only specifying what the computation does do, not what it doesn't. In other words, the first-order logic will carry out the computation correctly, but it will not "know" that the steps it is taking are the only steps the computation takes, or that the result it gets is the only result of that computation. This may sound inane, but first-order logic makes no assumptions. It only knows what we tell it.

The problem is, with just first-order logic, there is no way to say what we need to here. If there was an "and that's all" operator, we could list the positive facts about computations, and say "that's all". The logic would then know that any computational step not derivable from those basic steps never happens. But there is no such operator. I can tell it various things about what the computation does not do, but I will never finish my list.

Another way of putting this is that we can positively characterize computation, but we cannot negatively characterize it. Why not? Well, first-order logic is complete; this means that the rules of deduction can find all implications of statements we make. If we were able to state all negative facts, it would be able to find all consequences of them. But this would go against fundamental facts of computation. In particular, we know there is no way of deducing which computations eventually halt. If computations could be totally negatively characterized in a complete logic like first-order logic, the deduction rules would be capable of telling us this. So, this must be impossible.

In a sense, the reason we can't characterize computations negatively is because first-order logic has an open-world assumption. This means that if the deduction rules do not prove a statement true or false, it could be either. This is as opposed to a closed-world assumption, which would mean that if a statement is not proven true, it must be false.

So how does inserting lambda calculus into the mess help?

Lambda calculus is sufficiently closed to solve the problem. While a first-order theory can be added to without changing the meaning of what's already been stated, a program (stated in lambda calculus) cannot be altered freely. If we modify it, we simply have a different program on our hands. This means we can completely characterize many things that first-order logic alone cannot.

Fleshing out some more details of the logic:

-The deduction system should be a mix of a regular first-order deduction system, and a set of rules for the normal manipulation of the lambda calculus. This is as opposed to axioms describing how to manipulate the lambda calculus. Axioms would be in first-order logic and would therefore do us no good in terms of my grounding requirement, because they would not negatively characterize. The rules negatively characterize because they cannot be added to. (This is a petty distinction in a way; in practice, it wouldn't matter much, since nobody would add more facts to a running system concerning the lambda-calculus manipulation. But they could, and the system would accept these facts, whereas they can't add new rules without changing the system.)

-There is a question about how much to tell the first-order logic about its embedded lambda calculus. We could tell it nothing. But it seems practical for the system to have explicit first-order knowledge about the lambda-terms, so that it could deduce some facts about their manipulation (perhaps deducing facts about the results of certain calculations more quickly than could be explicitly checked by running all of those calculations). However, I have already said that we could keep telling the system more and more facts about computation, and yet never finish. So where do we stop? I have two ideas here. First, it seems reasonable to tell the system only the positive facts about the lambda calculus, since the negative ones are the ones that cause trouble. A few basic negative facts could be added at whim, if desired. This is very flexible. Second, we do not need to limit ourselves to first-order logic. We have lambda calculus at our disposal, and we can use it! In addition to placing the rules of manipulation outside of the system, as deduction rules, we could encode them within the system, using lambda calculus. This would allow the system to "know the deduction rules" despite it being impossible to completely characterize them in first-order logic.

More Hyperlogic

In the previous hyperlogic post I described loosely the arithmetical hierarchy, and a "hyperlogic" to deal with it. Although I didn't describe this in detail, the definition of this hyperlogic was inspired by a particular set of hypercomputers that can calculate functions in the arithmetical hierarchy.

The particular hypercomputers that I was thinking of are infinite-time turing machines, but restricted to change each output square only once during each infinite subcomputation. An infinite subcomputation is the size of the first ordinal infinity, whereas the computation as a whole may be logner (and thus have many infinite subcomputations); the number of infinite subcomputations is determined by the level on the hierarchy. (Additionally I need to stipulate that the output squares can start out either all black or all white depending on if we are calculating an existential (assumed false) or a universal (assumed true).)

So, to extend the hyperlogic further, it seems as if I need a more powerful hypercomputer to use as a basis.

After the arithmetical hierarchy comes the analytical hierarchy. The shift is from 1st-order arithmetic to 2nd-order arithmetic. (It is important to distinguish this from 1st-order logic and 2nd-order logic. 1st order logic is complete and doesn't need hypercomputers to decide its quantifiers, while 1st-order arithmetic is incomplete and does need hypercomputation.) In the arithmetical hierarchy, we are only quantifying over integers. In the analytic hierarchy, we quantify over sets of integers. The space being quantified over is infinitely larger, in a way that makes the previous methods fail.

The class of infinite-time turing machines I was considering uses only countable infinities of time. The analytic hierarchy requires quantification over an uncountable set, meaning it needs uncountable infinities of time.

An uncountable infinity of turing-machine steps may seem strange (or worse, incoherent), but if we ignore the details it works. It doesn't even matter what order everything happens in; since all I need is existential and universal quantification, I can just say that the machine stops and returns true (/false) if an example (/counterexample) is found, and otherwise keeps going until it has checked everything (at which point it returns the opposite truth value).

I do need to specify further how "checking an individual case" works. But this is not too difficult. Quantifying over sets of numbers gives us in each case some predicate that returns either true or false for each number. If there are more than one such quantifiers, we get more than one predicates. Ignoring the inner workings of the predicates, we just use them as given in what is otherwise a normal case of arithmetical hypercomputation.

Now, can we convert this to a finite process that in some sense captures the concept?

My tentative proposal is: look at a generic case of the problem, converting all set quantifiers to undefined predicates. Run the decision procedure for this arithmetical statement. Every time we need a particular value of one of the predicates, split the computation; run one version with the value of the predicate being "true" for the number it was given, and a second version with the value being "false". The result (after all versions of the arithmetical decision process terminate) will be a table with the number of dimensions determined by the number of set quantifiers, and the number of entries determined by how many versions of each quantifier ended up being needed. In any case we can attribute an approximate truth value to the statement by deciding each quantifier in order based on the examples examined.

Now, I am less sure about this method than I was about the arithmetical method. It seemed that improvements to the arithmetical method could never cause a serious increase in power, so that the method was within the realm of "the best we can do". However, for this method it is not clear that the machine is doing the best that can be done. In particular, I am not sure that adding direct 2nd-order theorem proving would not seriously increase the power.

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.