> Chris and Pat,
>
> one thing you must agree is that arithmetics is about operations
> such as + and . If one can reason at all, one has to understand how
> to use these operations. (01)
Of course. (02)
> Then people created all sorts of formal systems and wanted to prove
> everything. (03)
Well, more exactly every truth of arithmetic or some broader, but well
specified field like group theory. But yes, that was one early
motivation for the creation of formal systems. (04)
> None of these makes arithmetic any more secure, better, or more
> usable in any way. (05)
Well, while I tend to agree with you, there are some serious issues
here. For instance, the point of the logicist program was to show
that mathematics could be derived from purely logical principles. If
the program had been successful, that would have put mathematical
knowledge generally on a very secure epistemological foundation. The
program failed, of course, at least as initially envisioned. But
there are still lots of good reasons to formalize arithmetic over and
above any epistemological worries, e.g., for the sake of clarity, to
investigate properties of the theories, connections to other theories,
for use in automated reasoning and automated theorem proving, etc. (06)
> Still they talk about an incompleteness and completeness of
> arithmetics. (07)
Point being? (08)
>> (*) Not everything can be proved
>>
>> is, in the worst case, meaningless and, in the best case, ambiguous
>> (and false either way). Provability is always relative to a formal
>> system;
>
> I still understand Gödel's proof as a proof that you just cannot
> govern everything. (09)
Well, I thought I provided you with very good reasons for why you
should *stop* understanding it that way. (I guess by "govern" you
mean "prove".) (010)
> It is clear even without any proof about it. One way to prove that
> all cannot be proved is the simple fact 1+1=2 cannot be proved. (011)
In one sense, yes. It is quite reasonable to think that one cannot
expect to find a proof of 1+1=2 that uses principles that are somehow
epistemically more basic or certain than 1+1=2 itself. However, you
can most certainly prove it in a system of formal arithmetic  Peano
Arithmetic. 1+1=2 is not an axiom of PA. It has to be proved
formally from the axioms. Here's the proof; "S" indicates the
successor function: (012)
1. (x)(y)(x + Sy = S(x + y)) Axiom
2. S0 + S0 = S(S0 + 0) From 1
3. (x)(x + 0 = x) Axiom
4. S0 + 0 = S0 From 3
5. S0 + S0 = SS0 From 2 and 4 (013)
> Or, if you prove it in some formal system, then the axioms of that
> formal system cannot be proven true. (014)
From within the system (if the axioms are independent). Yes. What's
the point? Everyone knows this. (015)
> The theorem was a clear blow to some people who thought that
> everything can be governed, or put under some mathematical axioms.
> There's no denying that. (016)
Certainly not. It pretty much completely torpedoed "Hilbert's
Program" of finding a complete and consistent axiomatization of all of
classical mathematics. But again, there are still lots of good
reasons to axiomatize various branches of mathematics. (017)
chris (018)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontologforum/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontologforum/
Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontologforum@xxxxxxxxxxxxxxxx (019)
