Re: Is it a new Arithmetic?
From: namducnguyen (namducnguyen_at_shaw.ca)
Date: 08/31/04
- Next message: Immortalist: "Re: Existence as predicate"
- Previous message: Immortalist: "Re: Which of These Politicians Lies?"
- Next in thread: Aatu Koskensilta: "Re: Is it a new Arithmetic?"
- Reply: Aatu Koskensilta: "Re: Is it a new Arithmetic?"
- Messages sorted by: [ date ] [ thread ]
Date: Tue, 31 Aug 2004 03:44:44 GMT
William Elliot wrote:
>On Fri, 27 Aug 2004, namducnguyen wrote:
>
>
>>William Elliot wrote:
>>
>>
>
>
>
>>>>>>The nonlogical axioms of N are:
>>>>>>
>>>>>>N1. Sx =/= 0
>>>>>>N2. Sx = Sy -> x = y.
>>>>>>N3. x + 0 = x.
>>>>>>N4. x + Sy = S(x + y)
>>>>>>N5. x . 0 = 0.
>>>>>>N6. x . Sy = (x . y) + x.
>>>>>>N7. ~(x < 0)
>>>>>>N8. x < Sy <-> x < y \/ x = y.
>>>>>>N9. x < y \/ x = y \/ y < x.
>>>>>>
>>>>>>
>>>>>>If A is a formula of L(N), then the formula
>>>>>>Ax[0] & forall X(A -> Ax[SX]) -> A
>>>>>>
>>>>>>
>>>>>>
>>>>All I wonder, and might not have phrased it correctly, is that instead
>>>>of a full blown normal induction schema, could we replace it with identical
>>>>axiom schema - except there exists one formula B that falls outside the
>>>>schema in the sense that:
>>>>
>>>>~( Bx[0] & forall X (B -> Bx[SX]) -> B) is one axiom
>>>>Is this possible?
>>>>
>>>>
>>>>
>>>Sure, let B(x) be x /= x.
>>>
>>>
>>I'm not sure where you'd be going with B(x) being x /= x.
>>
>>
>
>Wake up, x /= x for B(x) fulfills your speculation.
>
>
>
>>I think you would agree that x = x is the identity axiom - a *logical*
>>axiom - and that x /= x is its negation, and that any formula built up
>>from these 2 with logical connectives is *logically decidable*.
>>
>>
>
>So what? I see no revelance.
>
>
>
>>But in this context of the theories N and PA (as previously mentioned),
>>we're talking about *nonlogical* additional axioms, which are
>>*undecidable*, to the theory which they're additional.
>>
>>
>
>We are? You've made no mention of that before.
>
Are you suggesting that every time we typically talk about axioms in
typical theories like PA, ZF, etc.., we *have to always* mention that
these are not logical axioms, lest that someone else might not understand
the context of usage of the word? [I thought that one of the requirements
of 1st-order theory is that it has to have _nonlogical_ axioms?]
>
>
>
>>In brief, *your* B(x) being x /= x doesn't seem at all like a candidate
>>for building up nonlogical axioms, under discussion.
>>
>>
>>
>Hey look, you asked if you could add a certain axiom. I replied
>yes, it could be possible, as for example when B(x) was x /= x.
>
In any rate, B(x) being x /= x still is not a base to build a non-logical
axiom that I'm looking for [though this might not have been obvious
to you].
>
>
>
>>If, for the sake of discussion, we consider as a "theorem" any theorem
>>that is not an axiom [i.e. its proof is of length > 1], then, in PA,
>>consider the formula:
>>
>>(1) An (n + 0 = n).
>>
>>Is (1) a theorem in the sense just described above? I'd think the answer
>>is "No": it's an axiom. The work that we typically call a "proof" of (1)
>>seems to be nothing more than showing that (1) could be decomposed
>>into a form that fits the Induction Axiom *schema*. Then that we accept
>>the schema as axiom-schema means we accept (1) as one axiom that could
>>be added to N.
>>
>>
>
>Baloney.
>
Right. My mistake. (1) is actually N3. But what I meant something like:
(1') An (n0 + n = n + n0) [where n0 /= 0]
In brief, any theorem in PA that could be written as one induction-axiom
of the induction axiom-schema, could be viewed as an additional axiom
w.r.t. to the system N' = N1 + N2 + ... N8. But then so could its
negation: e.g. N' + ~(1') is a consistent theory. If not maybe you could
help to explain?
>
>
>
>>In other words, (1) as a formula of L(N) is undecidable
>>w.r.t. to N. Which means N + (1) are N + ~(1) are 2 different theories,
>>*despite the fact that only (1) fits into the Induction axiom-schema*.
>>
>>
>>
>
>More Baloney. N + (1) = N, N + ~(1) = inconsistent theory.
>
>To show N1 is independent of N - N1 is likely easy.
>
>
>
>>It's precisely such observation that I wonder if we could modify the word
>>"schema" slightly: to denote a collection of axiom-formulae, all but one
>>would - in form - fit into particular schema; the one that doesn't have a
>>fit to the schema, its negation would.
>>
>>
>
>It's not clear what you're saying. Either you're mumbling
>or struggling with a non-native language.
>
>
>
>
>>That's basically where I'm coming from on a possible modification the
>>Induction Axiom schema. For a new arithmetic perhaps. But more likely,
>>for better understanding the old one, I hope.
>>
>>
>>
>You can tinker with the axioms any way you want.
>
>
>
>>But "B(x) be x /= x" doesn't seem to be a right start, imho.
>>
>>
>>
>Indeed, none of your modifications of N seem of any worth.
>Have you found a B(x) for your question for which
> the added axiom doesn't cause an inconsistency
>and
> it's not deducible from the others.
>
Note that in the [axiom-schema] form:
Ax[0] & forall X(A -> Ax[SX]) -> A
A is an general axiom of the form; and A has *many meanings*.
But as an axiom, for example, N5 has *only one meaning*.
In other words, *we don't have to spell out all the axioms of
the schema*. All is needed is they all have the same form as above.
Similarly, if we choose the negation ~Ak, for some Ak of the schema,
to be an axiom, then we only need to stipulate the *existence* of one
Ak - of the same schema-form - which is not an axiom, but in which ~Ak is.
[Or so it seems to me but I'm not quite sure. And that's why I posted
to ask.]
>
>If you're looking for a statement independent of N, ie undecidable in N,
>then you're going to have to do something much more sophisticated
>than your quick thoughtlessly feeble attempts, something astounding
>like Godel's incompleteness theorem. You may enjoy looking up
>Goodstein's theorem, describable in N, unprovable in N, provable in ZFC.
>
I'd think we owe a lot to Godel's work on undecidability of certain
formal systems. But I'd also believe that many situations have their own
merits and that GIT might not be a blank-cheque for addressing _all_
issues,
even issues related to undecidability. For instance, the 5th postulate
and AC
are 2 examples of undecidable formulae, yet they don't seem to share the
same history - or form - as that of Godel's G's.
In this particular case, intuition seems to indicate there is some kind
of "quantifier":
"For-All-but-One"
that could be applied to the induction-axiom-schema axioms. But I don't know
if the framework of FOL would vehemently forbid such a quantifer-concept,
despite a clear intuition. And I could be wrong but I just don't see
that this
new concept would have anything much to do with GIT.
- Next message: Immortalist: "Re: Existence as predicate"
- Previous message: Immortalist: "Re: Which of These Politicians Lies?"
- Next in thread: Aatu Koskensilta: "Re: Is it a new Arithmetic?"
- Reply: Aatu Koskensilta: "Re: Is it a new Arithmetic?"
- Messages sorted by: [ date ] [ thread ]
Relevant Pages
|
