|
|
Thank you all who have responded.
tchow@xxxxxxxxxxxxx wrote:
In article <rkmFg.421858$Mn5.15315@pd7tw3no>,
Nam Nguyen <namducnguyen@xxxxxxx> wrote:
ZF(C), after all, is just one theory out of infinite number
of 1st order ones. (Formally, FOL framework never insists that
we have to know about ZFC to formalize a different theory.)
Assuming we've formalized a theory G of "geometry", how could we prove
that the 5th "postulate" - as an axiom - is unprovable in G, without
mentioning anything about ZF(C)? In other words, how could we possibly
come up with a specific model of G in which the 5th is false? Thanks.
The answer to your question as you've stated it is, we construct a
non-Euclidean geometry, such as an elliptic or a hyperbolic geometry.
By "construct a non-Euclidean geometry" I take it you mean we form
a _model_ *in our mind*. This model might or might not be an abstraction
of what we observe physically. But nonetheless it's abstract and it's
a *legitimate* model of G, as far as FOL is concerned. At least that
seems to be what you mean here.
There is no need to say anything about ZF(C) in order to construct
such a geometry.
Agree. And the key point here is "There is *no need*". In other words,
when it comes to the *abstraction/subjectivity" of a model, there might
be no need for anything else, except for one's mental capacity to
perceive such a structure M is a model (and except for a suitable
model-constructing language of course).
> I suspect that your real question, however, is not the one that you've
> stated.
There is indeed motivation behind my question; I'll come to
it a bit later.
> Implicitly, perhaps, you feel that you can't "do mathematics"
> unless you state ahead of time some axiomatic system in which the
> mathematics you want to do is to be formalized.
I certainly do not feel that way.
> I believe that this
> is a serious misconception about the nature of mathematics and of
> formalization, but I also know from experience that trying to convey
> this point on USENET tends to lead to interminable and fruitless
> discussions, so I'll sidestep it for the moment.
Speaking for myself, I've experienced "doing mathematics" both ways.
I'm currently pursuing a certain 1st-order formalization, by starting
with some vague concepts first, and then with a bit more concrete
ZF(C) model, but still struggling with a final set of axioms. OTOH,
in my highschool years, I heard of the 5th postulate and "one" form
of its negation's (isn't it scary to put it that way?). But it took
my mind years to have a mental image (i.e. model) of what a 2-dimensioal
Riemman geometry is. So I'm of a different opinion in that in
"doing mathematics" it probably doesn't matter whether one start with
axioms first and model later, or the other way around.
> Your question might
> therefore be, can we formalize the construction of a non-Euclidean
> geometry without using set theory? Or, if set theory seems to be
> unavoidable, is ZF(C) required, or are there weaker set theories that
> suffice?
Let me explain my motivations here. What if abstractly we could *not*
come up with any model for T = G + ~(5th postulate)? In such case,
how would we know for certain whether T is or is not inconsistent.
Conversely, if we syntactically formulate a theory T and have proven
a "handful" numbers of theorems, and have a structure M where these
theorems are true, is *always guaranteed* that if we *assume* M is
a model of T, M would genuinely be model of T? (Think of Shoenfield's
finite axiomatization of N, and the "standard model" of arithmetic
of the natural numbers, which is N itself - which is quite circular!
[Given that we're talking about the foundation of reasoning!])
> For these kinds of questions, I do not believe that there is anything
> special about the construction of a non-Euclidean geometry, as opposed
> to any other piece of mathematics, e.g., the construction of finite
> simple groups or expander graphs. The general answer in all these
> cases is probably going to be something like, "Set theory is probably
> the most natural language in which to formalize the proof in question,
> although if you insist on dispensing with set theory, you can probably
> choose some other general foundation for mathematics, and that will
> work just as well. If you use set theory, then the full power of
> ZF(C) is almost certainly not needed." There may be exceptions to
> this general rule, but the construction of non-Euclidean geometries
> is so "low-powered" that it can almost certainly be formalized in any
> nontrivial theory you care to name.
So I'm not really after some antique systems (Euclidean or other
geometries); nor am I disregarding the utility of ZF(C) in typical
mathematical works. The issue here, imho, is the 2 "dualistic"
components of FOL reasoning: the concreteness/objectivity of anything
finite, such as formulae, proofs, inference rules; and the
abstraction/subjectivity such as semantic, interpretation, truth,
and models. To the extend that in general we could not infer one
component from the other, our ability to face with some of the
"severe" problems in FOL would be insufficient (or "incomplete"?).
(The 2 problems that I think we're well aware of are: the general
consistency of a T, and the Golbach Conjecture).
Imho, it's time that we need to revamp FOL, to move on with modern
day needs of reasoning. We should not pretend, for instance, that
the arithmetic syntactic formalization is consistent, while we just
*assume as a priori* the existence of a "model", without knowing
for absolute logical certainty that this "precious" one be indeed
a model.
--
-----------------------------------------------------
What we call 'I' is just a swinging door which moves
when we inhale and exhale.
Shunryu Suzuki
----------------------------------------------------
|
|