A More Direct Attack

So, as I noted last time, there are many possible ways to fit the predicate "True" into a language. Which of the many ways is correct? What does that even mean? What makes one better than another? Or, are all of them OK? Is it merely a matter of taste, since all of them capture the normal everyday uses of the concept of truth? In other words, is "truth" merely a concept that might be used in slightly different ways by different people, meaning there is no right answer?

I also noted last time that these logics do not seem to automatically solve the other problems I'm worried about; in particular, they do fairly little in the way of providing a foundation of mathematics.

The goal is to create a logic that can talk about its own semantics; a logic that can reference any mathematical ideas that were needed in describing the logic in the first place. Tarski started the whole line of research in this way; he asked, if a logic could define its own notion of truth, then what? (And he showed that, given some additional assumptions, such logics turn out to be contradictory.) But the theories I referenced last time, and those like them, have diverged somewhat from this line of inquiry... instead of providing a logic capable of defining its own truth predicate based on the semantic notions a human would employ in explaining the logic to another, these theories simply put the truth predicate in the language to begin with, and attempt to state rules that make it behave as much like our concept of truth as possible without allowing Tarski's contradiction.

That's totally different!

So, a more direct approach would be to try to create a logic that can define itself; a logic that can develop its notion of truth from more basic concepts, rather than declaring it as given. I suspect that such an attempt would not result in the same multitude of possible solutions.

The Logic of Definitions

On a related train of thought-- I have come up with another idea for a logic. The idea was based on the observation that many of the proposed solutions to defining truth were actually proposals for a theory of definitions in general; truth was then treated as a defined term, using the dfollowing definition, or some variant:

" "X" is true" means "X".

The revision theory treats this as a rule of belief revision: if we believe "X", we should revise our belief to also accept " "X" is true". The supervaluation theories claim that the above definition is incomplete (aka "vague"), and formulate a theory about how to work with incomplete definitions. (But, see this blog for a note on the ambiguity of the term "supervaluation".)

So, I have my own ideas about how to create a logic of definitions.

--The base logic should be normal classical logic. It could simply be first-order logic if that is all you need in order to define your terms; it could be arithmetic if that is needed; or it could be axiomatic set theory, if you need it to define what you want to define. In other words, the basic theory will depend on what you want to talk about with your definitions, but the logic that theory is set in will be classical.
--The logic of the defined concepts, however, will be violently non-classical. A defined predicate may be neither true nor false in some cases, because its definition simply fails to say anything one way or the other. It could be both true and false in other cases, when the definition implies both.

This is, of course, only a rough outline of the logic... it differs from most treatments of definitions (such as revision theory and supervaluation theory) by allowing not just statements that are assigned no value, but also statements that get both truth values.

Other's Inventions

My goal mentioned in the previous post was creating a logic that can reason about its own semantics (somehow sidestepping Tarski's proof of the impossibility of this). Well. This is a very ambitious goal. Luckily, I am not the first to desire such a thing, and there is a vast body of work on the subject. I find not one solution, but three:

Fixed Point Theories
Supervaluation Theory
Revision Theory

There are other theories than these, but these are the ones I saw mentioned the most.

It is comforting to see that "grounding" is often mentioned in connection with these theories, although the word is not being used in quite the same way I am currently using it. The word comes up particularly often in association with fixed-point theories.

Some of the differences between the three theories are superficial. For example, fixed-point theories are often stated in terms of three truth values: true, false, and neither-true-nor-false. Revision theorists reject this idea, and instead simply fail to assign a truth value to some sentences. This makes no difference for the math, however.

So, in a sense, the three theories are very similar: each describes some method of assigning truth values to some, but not all, sentences. Each of the methods sound overly complicated at first, compared to typical paradox-free mathematical settings, in which truth-assignment is very straightforward. But, once one realizes that the complexity is needed to avoid assigning truth values to meaningless statements such as paradoxes, each of the methods seems fairly intuitive.

Unfortunately, each method yields different results. So which one is right?

I've got to do a lot more research, to find out more about how they differ, other alternative theories, and so on. I suspect the fact that I am looking for concrete results rather than merely a philosophically satisfying logic will help guide me somewhat, but I am not sure.

Also, it appears that most of these logics are developed as modifications of arithmetic, rather than set theory. But, I am looking for a logic that can serve as a foundation for mathematics. It appears that a "direct attack" on the self-reference problem does not automatically get me what I want in terms of the general reference problem. So, I still need a good theory on how mathematical facts about uncountable sets can be grounded...

Direct Attack

My approach thus far to the issue of finding the correct logic has been incremental. For each logic, find something I cannot represent but want to, and attempt to extend the logic to include that. So, since I've settled on a form of lambda logic as a logic for arithmetical concepts, the next step would be to look for an extension into the hyperarithmetical hierarchy or the analytic hierarchy, or possibly to set theory. These form a progression:

arithmetic hierarchy < hyperarithmetic hierarchy < analytical hierarchy < axiomatic set theory

So, a jump directly to set theory would be nice, but the hyperarithmetic hierarchy would be the easiest next step.

This process can continue indefinitely, thanks to Tarski's Undefinability Theorem: no logic is able to define its own semantics, so if I want to find a way to extend some logic X, the standard way would be to look for a logic Y that can define the semantics of X. However, my vague hope is that if I work in these incremental extensions for long enough, I will eventually understand the undefinability principle well enough to see a way around it, thus making one final extension to the logic that encompasses all possible extensions.

This is a silly idea.

So, what about a direct attack? For it to work, I need to find a way around the Undefinability theorem. The undefinability theorem makes some specific assumptions; so, I know before starting that the logic I come up with needs to break these assumptions.

I'll outline the theorem's proof.

First, Tarski asks us to assume a minimal fact about the concept of truth: For all statements X, X is true only when X.

T(x) <=> x

This is called "Tarski's T-Schema". The idea is that if a formalization does not satisfy this, it cannot be a concept of truth. It is possible that more than the T-schema is required for a proper notion of truth, but if there are any, they aren't needed for Tarski's proof. (So, the T-schema is one of the critical assumptions to scrutinize. Is it really a necessary property of truth?)

Next, assume that some logic can talk about its own concept of truth. The idea is to prove that it can then say "This sentence is false", causing a paradox within that logic.

To prove this, we need one more assumption: the logic must contain arithmetic. This is a rather large assumption. However, it is one I am obviously making. So let's continue.

The reason arithmetic is required for the proof is that the Diagonal Lemma holds for any logic extending arithmetic. (So, if the Diagonal Lemma holds for some other logic, we don't need to require that the logic extends arithmetic.)

The diagonal Lemma states that if we can represent some predicate P, then we can create a sentence that says "I am P". In short, the Diagonal Lemma shows that any language extending arithmetic contains self-referential sentences.

Now: if the language can negate predicates, then it can express the predicate "not true" (since we've already assumed it can express "true"). Therefore, by the Diagonal Lemma, it can express "I am not true". Call this sentence Q.

By Q's definition, we have Q<=>~T(Q). (In english, this just says that Q and "Q is not true" say the same thing.) By the T-schema, we have Q<=>T(Q) (meaning Q and "Q is true" say the same thing). Therefore, we have T(Q)<=>~T(Q) (meaning "Q is true" and "Q is not true" say the same thing). Now we seem to have serious problems. In a classical logic, this proves a contradiction, finishing Tarski's proof that no such logic can exist.

So, it seems that there are plenty of ways to get around the undefinability theorem. However, it is not obvious which one is the right way.

Here is a list of some assumptions that could be violated:

1. The T-schema
2. The Diagonal Lemma
3. If we can express a predicate P, we can express its negation ~P
4. Every sentence is either true or false
5. No sentence is both true and false

This is not a new problem, so there are many proposed solutions. Of course, my version is somewhat unique, since I want a solution that not only allows "truth" to be defined, but also any other coherent concept that a human might wish to define.

Some initial thoughts.

The T-schema seems solid, although I can't rule out the possibility of counterintuitive exceptions.

The Diagonal Lemma is an assumption I cannot break, since what I am proposing is a logic that can refer to anything a human can refer to. It is conceivable that the logic humans use does not admit the Diagonal Lemma, but if that is the case, then my goal is impossible because it implies that humans cannot define the logic that they use. If my goal is acheivable, then it is acheivable with a self-referential logic.

Assumption 3 seems solid, but again maybe there are some strange counterintuitive exceptions.

Assumption 4 seems false in the presence of sentence Q; it is far from obvious that sentence Q is actually true or false.

Q could also be seen as a counterexample to assumption 5, if it is seen as both thrue and false rather than neither. Personally I prefer neither.

Source:
http://plato.stanford.edu/entries/self-reference/#Matt-sema

Paradox

I discovered a paradox in the version of lambda logic that I am creating. It is not difficult to fix. However, I'll explain the paradox before I explain how I fixed it.

Here it is symbolically (or rather, semisymbolically, because I'm not using any math rendering):

L = lambda x . (x x)
H = lambda x . exists y . output((x x), y)
I = lambda x . (H x (L L) 1)

With these definitions, the expression (H I) is paradoxical. I'll explain why.

The first important thing is that I am treating an existential statement as if it were a function that returned true or false. In lambda logic (the official version), this is allowed:

True = lambda x y . x
False = lambda x y . y

So, True is a function that takes 2 arguments and returns the first, while False takes two and returns the second. This should be thought of in terms of if/then/else statements. We can make triples (a b c), and if a evaluates to True, b is returned (the "then" clause); but if a turns out false, then c gets returned.

I define L for convenience. L takes an input, x, and returns x applied to itself. The compound statement (L L) is an infinite loop in lambda calculus: it takes L and applies it to itself, resulting in (L L) again. This isn't paradoxical in itself, because the logic does not assume that a result exists for every computation.

The second term, H, takes a term and detects whether it has a result when applied to itself. That is the meaning of "exists y . output((x x), y)": there exists an output of (x x). (I could have used the L construct, writing (L x) instead of (x x), but that wouldn't be any shorter, would it?) So, the way to read (H x) is "x outputs something when handed itself as input".

I is what I call the switch operation. If F is a function that returns some result (when applied to itself), then (I F) doesn't return anything. If F doesn't, (I F) does. How does it work? Well, I is written in the if-then-else format. The "if" part is the "H x", meaning "x returns something when applied to itself". The "then" part is (L L), a statement that never returns anything. The "else" is just 1, a number. Any concrete thing could be put in this spot; it just gives the function something definite to return.

Now, the paradox comes when we consider (H I). This expression asks the question, "Does the switch operation return anything when applied to itself?" Either it does or it doesn't. If it does, then (because it is the switch operator), it doesn't. If it doesn't, then it does. Contradiction. Paradox.

The problem is that I am allowing lambda-terms to be formed with non-computable elements inside them (such as the existential statement inside H). To avoid the paradox, but preserve the ability to represent any statement on the arithmetical hierarchy, I should restrict the formation of lambda terms. A set of computable basic functions should be defined. The list could include numerical equality, addition, subtraction, multiplication, exponent, et cetera. (Any operation that takes nonnegative integers and returns nonnegative integers.) However, it is sufficient to include only the function F(x), where F(x)=x+1. (Everything else can be developed from this, using lambda calculus.) Also-- it should be understood that the terms that can be created (from these basic computable terms plus lambda) are all the entities that exist within the logic. So, if the logic says things like "exists y . output((x x), y)", it should be understood that the "y" that exists is one of these terms.

Now, why doesn't the official version of lambda logic need to avoid throwing existential statements inside lambda expressions? The reason is that strong predicate I use, "output(x, y)", that means "y is the result of evaluating x". Lambda logic proper only uses a function that represents the performance of a single computational step. If I try to define H, I get a statement that always evaluates to True, because there is always a result of performing a single computational step.

More on Lambda Logic

I've read more about Lambda Logic. The Lambda Logic that I found is actually a bit different than the one that I was considering on my own. First, it is not referentially strong-- the logic has a complete inference method, which means it can only talk about provable things. So, it can't really reference lambda-computations in the way I want, because there are unprovable facts about computations.

Another interesting point-- Lambda Logic is inconsistent with the Axiom of Choice!

Latest Finds


My logic exists!
Its official name is "lambda logic". Makes sense.

Also, the Opencog Prime documentation was recently released. Worth a look! The knowledge representation used there is also of the form I've been considering-- there are both explicitly represented facts, and facts that are represented implicitly by programs.