[ivan.moony]

Here is a bit of remark on knowledge theory.

While constructing `the language of all languages`, I've been investigating Gödel's incompleteness theorems, and it looks pretty amazing and scary in the same time. Each theory has some properties like consistency and completeness. Consistency means that we can't derive both a sentence and its negation from the axiom set. Completeness means that every sentence or its negation in theory language can be proved. Simplified, Gödel says:

There is no sufficiently complex theory that can be consistent and complete at the same time.

Ok, we'll say, another general truth... But that Gödel guy is really something. His work is based on constructing a sentence that can't be proved or disproved, questioning completeness and consistency, but a form of this sentence is what is really interesting. The unprovable sentence, in a terms of chosen theory, has the following form:

There are sentences in this theory that can't be proved nor disproved.

Wow. I don't know would I call this sentence formation so ingenious or so simple that it almost seems stupid. And it almost seems like the mother nature is joking with us. And it scares me a bit because it reminds me of a strong deja vu because the sentence is indirectly self-referential.

Anyway, knowledge seems to be bounded, if we ask Gödel, so we shouldn't expect AI to be all-knowing-entity.

[ivan.moony]

Following Tarski's work, which is based on Gödel's work, a striking fact arises. Remember that Gödel said that there are sentences which can't be proved or disproved? Well, what would be those sentences?

Tarski showed that proving a truth of some theory sentence happens to be futile. He said that the very notion of truth in some theory is not definable in terms of that theory. What an important concept, what an essence thing, like truth, and it can't be proved. Out of all things, the most important thing like truth can't be derived or proved from a theory dealing with the same truth instances.

Luckily, there is workaround, and that is to define another, more general theory in which we define what a truth is in underlying theory, while the underlying theory inherits a concept of truth without knowing how to define it. Still, what a truth is for this more general theory remains unknown, unless we define even more general theory, and so on.

A consequence is that there couldn't exist a theory that explains what a truth really is. Now imagine the Universe as a big theory. Then it follows that the Universe itself can't define the truth of itself, yet a truth exists, and it is a concept of the history or predictions about the future. So there should be something bigger than the Universe. But what is then bigger than that bigger thing? What is that magic force capable of things we couldn't reach within this Universe? Remember that we are talking about truth itself, so what would this truth represent? Would it be a machine, or something (or should I say someone) conscious?

[ranch vermin]

Large functionless thinking.     Get back to the planet earth and do something more useful with your thinking,  nah just kidding,  this could be important like you say.

[ivan.moony]

Actually, noted theoretical proofs have direct influences to my `language of all languages`. I had a trouble in defining the truth with bidirectional `True <-> (X | ¬X)` and falsehood with bidirectional `False <-> (X & ¬X)`. The whole system was collapsing to `True` (when it is either tautology, satsfiable or even contradiction). I fixed it by unidirectional `True -> (X | ¬X)` and `(X & ¬X) -> False`, but after that I found myself reading about Gödel's and Tarski's work. My language aligned with their results and encouraged me to think I'm on the right path. Otherwise, I'd think I'm making some mistake, and I'd hunt ghosts where there are really no any.

Besides that, it would be interesting to prove whether God exists or not. Now I tend to believe that such a thing is unprovable, just like `True` is unprovable. But guess what? `False` is sometimes provable. Now, what would that mean?

[Freddy]

Truth can be a very relative and subjective thing can't it. One man's truth can be another's fiction.

Even in science they say things like "the world's biggest something", forgetting to add the qualifier of "currently known to science".

Often truth is what we currently believe in.

Just some thoughts.

[ivan.moony]

All we know, or have proven is based on some assumptions, while assumptions are taken for granted. The moment we start questioning the starting assumptions, all we know gets shaken. And all there is before assumptions are other assumptions. It is not wonder that different people think differently, as we all don't share the same set of assumptions. And if we have contradictory assumptions, it is hard to tell which one is right, as assumptions are just that, assumptions without the almighty proof. Well, we have to start from somewhere, and that somewhere is usually left unproven. An attempt to get it proven results in a start before the first start, making it again unproven.

[Edit]
All we can say about a set of assumptions is whether they are contradictory (if they yield both a sentence and its negation). In other words, we can say for sure if a whole of set of assumptions is false. But is it really true, it remains unsolved.

[ranch vermin]

oh I can relate it to my one now.  Dreaming off into the future,  is the robot cant tell the difference between a halucination and reality,  we can.  but it takes personal strength.

robots dont usually halucinate,  but maybe something could happen to its sensors?....?

[EDIT] i should explain more,  im thinking about playback of a recording of the environment, which is what my theory is based apon. [/edit]

[Zero]

Tarski showed that proving a truth of some theory sentence happens to be futile. He said that the very notion of truth in some theory is not definable in terms of that theory. What an important concept, what an essence thing, like truth, and it can't be proved. Out of all things, the most important thing like truth can't be derived or proved from a theory dealing with the same truth instances.

Luckily, there is workaround, and that is to define another, more general theory in which we define what a truth is in underlying theory, while the underlying theory inherits a concept of truth without knowing how to define it. Still, what a truth is for this more general theory remains unknown, unless we define even more general theory, and so on. 

I really appreciate the way you always try to crack reality open, ivan. Striking right at knee: logic.

I'm probably being dumb here, but... There's a Python interpreter written in Python, and a Javascript interpreter written in Javascript. How about defining truth in terms of another theory, which happens to be the same? Does the "more general" theory have to be "strictly" more general (>), or can it be "equal or more general" (>=) ??

Could you suggest some good books, for a beginner like me please?

[ivan.moony]

There's a Python interpreter written in Python, and a Javascript interpreter written in Javascript. How about defining truth in terms of another theory, which happens to be the same? Does the "more general" theory have to be "strictly" more general (>), or can it be "equal or more general" (>=) ??

Could you suggest some good books, for a beginner like me please?

I'm sorry, I can only guess, I'm a beginner too in this area. I didn't check, but I guess that superlanguage A can be equal to its sublanguage B. But I also guess that all imperative language are inconsistent, as they don't use negation of sentences, so they don't check when a contradiction is generated, which means they can produce a lie, and with lies we could do extraordinary things like woodoo magic and stuff like that.

The deal with negation is that we can spot a contradiction and prevent a program from being run, or do something based on that conclusion.

Books? All I have are this and this Wiki links. If you start from there, I'm sure you'll find some real interesting references, at least at the bottom of pages. If you are interested in a parallel of logic to functional programming, see Curry-Howard correspondence.

[Zero]

I needed to understand the vocabulary. Here is what I collected from wikipedia.


Theory =
In mathematical logic, a theory (also called a formal theory) is a set of sentences in a formal language.

Sentence =
In mathematical logic, a sentence of a predicate logic is a boolean-valued well-formed formula with no free variables.

Well-formed formula =
In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language.

Consistency =
In classical deductive logic, a consistent theory is one that does not contain a contradiction.

Contradiction =
In classical logic, a contradiction consists of a logical incompatibility between two or more propositions. It occurs when the propositions, taken together, yield two conclusions which form the logical, usually opposite inversions of each other.

Complete theory =
In mathematical logic, a theory is complete if, for every formula in the theory's language, that formula or its negation is demonstrable. Recursively axiomatizable first-order theories that are rich enough to allow general mathematical reasoning to be formulated cannot be complete, as demonstrated by Gödel's first incompleteness theorem.



Completeness... I don't get it. What does "demonstrable" mean?

[ivan.moony]

Completeness... I don't get it. What does "demonstrable" mean?

I think it means provable, having a possibility to deduce itself from a set of axioms. We state a set of starting axioms. Beside axioms, we have an underlying inference mechanism behind the stage. If we can infer every formula in some theory language from the axioms, the theory is complete. I believe such formulas are called theorems. What I don't get is: how a formula can be a part of a theory language if it is not a theorem of that language. In other words, how can it be a part of the theory if we can't infer it from axioms? However, Gödel seems to be able to construct such formulas by his first and second incompleteness theorem.

[Zero]

I thought a well-formed formula was just correct syntactically, without taking meaning into account. How can we prove a formula that is only syntactically correct? What does it mean to prove such a thing?

[ivan.moony]

It's about models. Model is a semantic set of true/false - atom values for which a whole formula is true. I think we can only prove a tautology (formula that is true in all models) or contradiction (false in all models). To prove that a satisfiable formula (true only in some models) `B` is a consequence of satisfiable formula `A`, we have to write what we predict that is a tautology (in a form of `A -> B`). Then we can either derive a contradiction from its negation, or derive `A -> B` from A, B and axioms.

[Edit]
Consider well formed formula as a program that syntactically passes parsing. But that is not a guarantee that the same program is valid. To prove validity, we have to pass the program through a type checker. And parser + type checker = compiler.

[Zero]

So we can add


Model =
A model of a theory is a structure (e.g. an interpretation) that satisfies the sentences of that theory.

Interpretation =
An interpretation is an assignment of meaning to the symbols of a formal language. An interpretation often (but not always) provides a way to determine the truth values of sentences in a language. If a given interpretation assigns the value True to a sentence or theory, the interpretation is called a model of that sentence or theory.



I always thought that syntax correctness included types too, for example a "print" command that must be followed by a string, raises a "syntax error" if something a number follows the "print" command. In fact I was mixing 2 things that was not meant to be mixed. Like CSS in my HTML, sort of.

[ranch vermin]

the truth agrees with itself,  if ever a contradiction - which agreement is true?  u dont know - u can only go with a feeling.   but the truth is a singular group in itself,  it must agree 100%.