Re: Formalizing the Fundamental Theorem of Arithmetic

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. 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.koskensilta@xxxxxxxxx)

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