W dniu środa, 14 czerwca 2017 12:59:23 UTC+2

*Post by Peter Percival**Post by m***@wp.pl*Notice, that Godel has never proven that any incomplete

theory exists. He has only proven that every theory is

EITHER

Every?

Formally not. Practically yes.

Remember, you're talking about what Goedel has proven

here. What does it mean that Goedel has _practically_

proven every theory is either incomplete or inconsistent?

One example of a theory that is both complete and consistent

is a subset of natural number arithmetic without

multiplication, Presburger arithmetic.

(Provably complete, certainly consistent if all of

arithmetic is consistent.)

*Post by Peter Percival**Post by m***@wp.pl*incomplete OR inconsistent. Considering what he used

our logic can't manage some specific loops.

I think that the important point is that he's _proven_

an obviousness well known for millennia (loosely speaking).

A formal description of some system chooses particular

aspects of the system to describe. I don't think it is

ever _all_ the aspects. I suspect that's not even possible.

A solar system might be seen as point masses moving in

a 1/r potential, for example. There is lots more we could

say about those planets and sun, but that selection of

properties serves our purpose -- for some purposes, if

not for others.

We can choose to formalize certain aspects of our reasoning

and leave other aspects out. The logic of sentences

(propositional logic, zeroth-order logic) treats our

sentences as "point masses" interacting with operators

AND, OR, NOT, and so on. (First-order) predicate logic

includes the zeroth-order description and then adds to that

individuals of some kind and properties of some kind

for those individuals. And so on.

As you say, it should not be surprising that our

incomplete description of our reasoning should have

holes in it, that there should be claims that can be

stated but neither proven nor disproven. We are only

human, after all. But that's not Goedel's point.

Let us say that a formal system "knows" its axioms and

"knows" the theorems that follow from its axioms. What a

formal system "knows" is exactly what it can prove.

For a formal system which "knows" what it "knows"

(that can describe what a proof is in that same system),

that formal system "knows" that it does not "know" everything

(can prove that there are sentences without either proofs

or disproofs).

This piece of wisdom is at least millennia old.

(Whether it is obvious is arguable. I don't think

it would be hard to collect a horde of those who

believe they know everything. But never mind.)

According to Plato, Socrates said

[...] I seem, then, in just this little thing to be

wiser than this man at any rate, that what I do not

know I do not think I know either.

However, Socrates was very wise. How much wisdom must

we include in the description of our reasoning to be

as wise as Socrates? Kurt Goedel showed us: almost none.

If we know some basic logic and some basic arithmetic,

and if we can state what we mean by "proof", then we

"know" that we do not know everything.

The incompleteness of our knowledge is _not_ a result

of our human, finite selves leaving holes in our

incomplete descriptions. The incompleteness of our

knowledge is _a part of our knowledge_ , as much as

2 + 2 = 4 is. It won't go away if we grow wiser, if

we build a better formal system on top of our existing

formal system, any more than 2 + 2 = 4 will go away if

we supplement our natural numbers with negative numbers

and rationals and multivariate calculus.

(If 2 + 2 = 4 did go away, we would need to question

the validity of our supplements.)

Goedel titled his article

"On Formally Undecidable Propositions of

Principia Mathematica And Related Systems".

It is his use of the word "Formally" -- shown by _proof_

within a formal system -- that makes his work

extraordinary, worth all the praise it has received.