Re: Formalizing the Fundamental Theorem of Arithmetic

On May 24, 12:50 pm, Aatu Koskensilta <aatu.koskensi...@xxxxxxxxx>
wrote:
On 2007-05-24, in sci.logic, george wrote:

In other words, the best answer to the original question
is another question, namely, "What is the most natural
and straightforward encoding of a multiset of natural numbers
as a natural number"? And you DON'T get to say
"the product of multiplying the nth prime to the mth
power for every n in the multiset" -- that is precisely the
encoding we are trying to INVERT (i.e., if you do that, then
every number's prime factorization is best represented by the
number that is ITSELF; somehow I DOUBT that that COULD COUNT
as "a proof of the fundamental theorem of arithmetic").

Under some coding schemes the fundamental theorem of arithmetic does indeed
come out as a triviality, the formal proof of which has nothing to do with
its proof in the ordinary sense.

How could that be when an "ordinary proof" is a subset (part) of a
formal proof?

"The skeptic will say, 'It may well be true that this system of
equations is reasonable from a logical standpoint, but this does not
prove that it corresponds to nature.' You are right, dear skeptic.
Experience alone can decide on truth." - Albert Einstein

C-B

This is an illustration of the fact that
when formalizing mathematics we must exercise our judgment and good sense to
decide whether the formalization captures the aspects of ordinary
mathematical reasoning we find relevant.

--
Aatu Koskensilta (aatu.koskensi...@xxxxxxxxx)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus


.