|
|
Re: Axiomization of Number Theory
Posted:
Jul 29, 2003 2:24 PM
|
|
Charlie-Boo wrote:
>Andrew Boucher <Helene.Boucher@wanadoo.fr> wrote:
>
>
>>Charlie-Boo wrote:
>>
>>
>>># 1. Could you provide formal axiomatic proofs, rather than English
>>>descriptions?
>>>
>>>
>>>
>>For three of your first four, here's where you can find formal proofs.
>>1. If A is a factor of B and B is a factor of A, then A=B.
>>Prop 23 in www.andrewboucher.com/papers/foea/VI1.pdf
>> 2. If A is a factor of B and B is a factor of C, then A is a factor of C.
>>Prop 24 in same paper
>> 4. There are an infinite number of prime numbers.
>>Prop 21 in www.andrewboucher.com/papers/foea/VII4.pdf
>>
>>
>
>I see a whole lot of undefined symbols and no explanation of the
>axioms and rules of inference in the above references. Perhaps you
>can simply give the axioms, rules, and proof here? However, 1 and 2
>are so simple, only 4 is of interest at this point.
>
Yikes! I did say that 4 was at the end of 1800 pages. So, I'm not
going to give you "the" proof, other than in the paper as referenced.
An introduction to the system can be found at:
http://www.andrewboucher.com/papers/foea/I1.pdf
Basically, if you read that, and you understand the meanings of the
special symbols (which can usually be infered from the surroundings),
you should be able to follow the proofs.
The logical system is essentially natural-deduction. I wanted to make
the language dynamic (allow for new symbols), and that complicated the
definition of the language. In any case the axioms and definition of
the language can be found in:
http://www.andrewboucher.com/papers/foea/I11.pdf
Specifically, the mathematical axioms are on pages 19-21. All symbols
used are summarized on pages 30-32.
A summary - all definitions and all propositions proved - can be found in:
http://www.andrewboucher.com/papers/foea/FOEASummary.pdf
>
>You know, this idea of people saying "See reference xyz" and when you
>look you don't really find what you were talking about and then when
>you say "Can you just give your result here?" they call you lazy or
>something, isn't a new one. So, you're not going to try that old
>trick and call me lazy and refuse to actually give the axioms, rules
>and proof here, are you? Because, honestly, I don't see that you
>axiomized it in your papers, though, as I said, we are only talking
>about the first, simplest Theorems that I figured weren't that hard
>(about the most Peano Arithmetic can do) anyway. :)
>
>
>
>>(and incidentally
>>the last proposition, after yikes! 1800 pages of proof).
>>
>>
>
>Bet I can reduce it by a factor of 1800 (with the right axiomization).
>
I bet you can.
>
>
>
>>At some point I may continue further. Hard cash would help. ;-)
>>
>>
>
>Darn, just when you got to the hard ones. Name your price. How about
>$1,000.00 if you prove the other theorems in Peano Arithmetic?
>
You do realize that I was joking.
>
>
>
>>># 2. I listed the theorems in order of complexity, and you stopped
>>>after the first few (simplest) ones. This is as I described: Peano
>>>Arithmetic allows for the derivation of only the simplest of theorems.
>>>Could you address the more complex theorems given later in the list?
>>>
>>>How would you even represent the statement "N is a perfect number." in
>>>Peano Arithmetic?
>>>
>>>
>>>
>>"n is a perfect number" can be translated as "Sum{x : x | n} = n" where
>>"Sum(P)" refers to the x in (hope I got this right):
>>
>>"[m][R][S] ( Seq(R,m,P) & Seq0(S,m) & S'm = x & S'0 = 0 & (i)(i < m => S'(i+1) = S'i + R'(i+1)) )".
>>
>>Here:
>>[..] means "there exists .."
>>Seq(R,m,P) means "R is a sequence from {x : 1 <= x <= m} onto P"
>>Seq0(S,m) means "S is a sequence from {x : 0 <= x <= m}"
>>S'z refers to the y for which Sz,y
>>
>>The last two are exercises to define in second-order arithmetic.
>>
>>
>
>Sum(x:x|n)? Is that in Peano Arithmetic? Are you confusing the
>Predicate Calculus with some Programming Language? And do your rules
>apply to Sum(x:x|n)? I mean, if you're going to throw in arbitrary
>syntax and semantics, your rules will have to likewise be modified for
>this non-Predicate Calculus expression. What happened to the original
>"Peano Arithmetic can do it"?
>
First, second-order Peano Arithmetic is not in the "Predicate Calculus,"
which is first-order logic. Secondly, you have to accept abbreviations,
or be willing to unbundle the abbreviating terms. So e.g. if you don't
want to accept
"Sum{x : x | n} = n"
then I would write
"[m][R][S] ( Seq(R,m,P) & Seq0(S,m) & S'm = n & S'0 = 0 & (i)(i < m => S'(i+1) = S'i + R'(i+1)) )"
for "n is a perfect number," where someone (you can't and I won't) has
to unbundle the Seq wffs. If "<" is not part of the Peano Arithmetic
under consideration, it has to be rewritten as well (say in terms of
addition).
>
>I said "What is the formal wff?" next just in case someone decided to
>drift away from Predicate Calculus and throw in some programming
>subroutine. Do you really maintain that all of the above is a Peano
>Arithmetic wff?
>
Yes.
>
>Could we just stick to ^ v => ~ exists forall and relations, you know,
>Peano Arithmetic wffs? (I failed your two exercises, so I guess
>you'll just have to give a complete answer.)
>
I thought I stuck pretty well.
>
>
>
>>So it's not difficult at all in PA2 (or a near-enough version of it).
>> Maybe you were thinking of PA1.
>>
>>
>
>I'll take either, as long as it doesn't make up new stuff along the
>way.
>
>
>
>>>What is the formal wff? More fundamental than the
>>>question of undecidable wffs being few and far between and the system
>>>being sound (suggesting that true wffs are usually provable), is the
>>>question of whether Peano Arithmetic can even represent the theorems
>>>to be proved in the first place.
>>>
>>>
>>>
>>In my eyes anyway, second-order PA does a good job of representing the
>>theorems.
>>
>>
>
>I'll believe it when I see it.
>
>
>
>>>The Theory of Computation is axiomized with 3 axioms: TRUE(x) [the
>>>universal set is recursively enumerable], YIT(I,J,K) [the
>>>proof/halting YES predicate is recursive] and a single Incompleteness
>>>Axiom -~YES(x,x) ["The set of programs that do not halt YES on
>>>themselves is not recursively enumerable."], which I actually prove by
>>>going slightly outside of the system.
>>>
>>>
>
>
>
>>Cheater !
>>
>>
>
>I'm supposed to prove the axioms within the system?? I only mentioned
>that one of the 3 axioms is "almost a theorem" as an aside. It's an
>axiom, ok?
>
Ok ok. I'll take "cheater" back.
>
>
>
>>Seriously, I don't think any of these three axioms are low enough
>>
>>
>
>Oh really? What if they do the trick anyway (see my article)?
>
You can just assume the proposition itself, and that would do the trick
as well. What you need is to have axioms that have some other
justification that just that they prove what you're trying to prove.
>
>
>>I certainly don't understand why I should accept them as true.
>>
>>
>
>Since when do we prove axioms?
>
I didn't ask you to prove them. I wanted to know why I should accept
them as true. You could, of course, prove your theorem from a
contradiction, but that, I think you agree, would be boring.
> But if you insist, then tell me again
>- you doubt that:
>
>1. The set of natural numbers is recursively enumerable?
>2. The proof/halting YES predicate ("Program A halts YES on input B at
>iteration C.") is recursive?
>
>3. The set of programs that do not halt YES on themselves is not
>recursively enumerable?
>
I wouldn't want to assume 2 or 3, certainly. But that could just be me.
Maybe there are reasons for assuming 2 and 3, which I haven't thought
about, and/or you are able to do something with these axioms other than
just prove your theorem.
>
>Honestly (no offense), but you seem to be grabbing at certain phrases
>that I wrote without looking at the context. I mean, the "going
>slightly outside of the system" was in the context of mentioning that
>one of the axioms is "almost provable within the system" (just an
>aside). The axioms are of course well-known facts. In each case, if
>you look at what I actually said, there's certainly no problem with
>these assertions.
>
>Can we just agree to:
>
>1. No references without giving the result here as well (just in case
>one doesn't really find the result in the cited paper.)
>
No
>2. No "exercises".
>
No
>3. No "wffs" that contain English.
>
Ok
>4. No "wffs" that go outside of Peano Arithmetic (Predicate Calculus)
>syntax (unless you want to give a completely new system, which is ok
>if that is your intent, but then you need to say that and define the
>whole thing.)
>
Not sure.
>5. No demanding money to give the answers.
>
Are you kidding me ??!!
>
>In other words, can we just stick to formal axioms, rules and proofs?
>
>BTW: I've been a reader of your internet publications for years. I
>may have even written you a fan mail sometime in the past!
>
Glad to hear it! I need all the fans I can get !
>
>
>
>>>Charlie Volkstorf
>>>Cambridge, MA
>>>axiomize at aol dot com
>>>
>>>
|
|
