W dniu środa, 14 czerwca 2017 12:59:23 UTC+2
Post by Peter PercivalPost by m***@wp.plNotice, 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 PercivalPost by m***@wp.plincomplete 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.