Back to the Ground

In the previous post, I described a way of constructing arbitrarily powerful logics. This description does not amount to an algorithm-- it invokes something human mathematicians do (listing larger infinities), but doesn't provide a way to implement that on a computer. Worse, it is known that by the standard definition of algorithm, such an algorithm does not exist; I can only hope that it does exist as a limit-computable algorithm. (Note: I just found out that the term "super-recursive algorithm" that I used last time can refer to algorithms decidedly not implementable on normal computer hardware... so I guess there is not a single term that refers to exactly those super-recursive algorithms that are implementable on standard hardware. "Limit-computable" is closer...) But, I think this is likely, since I think humans use such an algorithm.

Anyway. What I did not describe was a way of "grounding" each new level. I have previously discussed at length an idea for grounding "two", based on non-monotonic logic and an understanding of meaning within the network of beliefs rather than only in terms of the outside world. But, what about grounding the higher operators? With no manipulation rules, they are quite pointless!

Actually, the operators are not exactly the problem. If we wrap two statements in an "implies" statement, the truth/falsehood of the result relies on no more then the validity of the deduction from the first statement to the second. In other words, in some sense we aren't adding anything, we're just making explicit something we already do. But then something strange happens: we're suddenly able to wrap quantifiers around the statement. This becomes problematic. At that stage, we've got to create the manipulation rules that the next stage will wrap up in an explicit operator.

Actually, the same problem applies for the system two. I haven't specifically talked about how one statement in two might be derived from another.

But, really, the use of the "implies" operator is not essential: I could just have well used a "true" operator that took one statement. "A implies B" is true in the metalogic when "A -> B" is provably true in the base logic, with "->" representing truth-functional implication.

Reducing "implies" to "true" in this way changes the appearance of the whole system greatly-- it makes obvious the direct connection to Tarski's Undefinability Theorem and the hierarchy of truth predicates that it was originally taken to entail.

So, the manipulation rules for "true" are sufficient to account for the manipulation of "implies". First, we can adopt the famous T-schema:

something <=> true(something)

This does not lead to paradox because there is indeed a hierarchy established, rather then a single "true".

Second, boolean combinations and sentences with quantifiers are subject to the typical deduction rules.

Third, quantifiers are additionally subject to fallible rules: existential quantifiers are fallibly refuted by (infallibly) refuting many instances, and universal quantifiers are fallibly affirmed by (infallibly) affirming many instances. (One may wish to allow fallible evidence as well, but there is no normative justification for doing so: the resulting beliefs will never converge to the truth!)

fourth, "true(something)" is to be interpreted as "exists(affirmation of something in a lower logical system)", so that it is fallibly refutable like other existential statements. ("Affirmation" means proof if the lower system is one, limit-proof if the system is two, and so on. (So, in general, a proof of finite or infinite length.) Different logical primitives could be used in order to let this definition of "true" actually occur within the system; in particular, we could introduce more and more powerful quantifiers rather than more and more powerful truth-operators.)

So, do these definitions ground the system's mathematical knowledge (Assuming we;ve also supplied the system with a method of enumerating infinities)? Well, it's hard to say, isn't it? "Grounding" is a philosphical issue. We need a concrete definition. Try this: a system's knowledge of X is grounded iff it reasons about X in the way that a human who knew about X would reason. More precisely, it captures everything worth capturing about the human way of reasoning. The answer to the question still isn't obvious; I do not have at my disposal a list of all the things worth capturing about human mathematical reasoning. But, I do have a partial list of things that I think are worth capturing...

-first-order reasoning
-limit-computable fallible reasoning
-arithmetical meaning
-set-theoretic meaning
-mathematical induction
-transfinite induction

The theory above does not totally encompass all of limit-computation (it uses sigma-1 and pi-1 but not delta-2!). It does not entirely explain set-theoretical intuition (it includes "grounding" for uncountable entities, since it (hypothetically) enumerates any infinity a mathematician might; but, it doesn't support direct talk about sets). It doesn't support mathematical induction or transfinite mathematical induction.

So, still work to be done!