Re: A question about FOL theories and models

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.
There is no need to say anything about ZF(C) in order to construct such
a geometry.

I suspect that your real question, however, is not the one that you've
stated. 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 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. 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?

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.
--
Tim Chow tchow-at-alum-dot-mit-dot-edu
The range of our projectiles---even ... the artillery---however great, will
never exceed four of those miles of which as many thousand separate us from
the center of the earth. ---Galileo, Dialogues Concerning Two New Sciences
.

Relevant Pages

  • Re: A question about FOL theories and models
    ... Assuming we've formalized a theory G of "geometry", ... > mathematics you want to do is to be formalized. ... can we formalize the construction of a non-Euclidean ... if set theory seems to be ...
    (sci.logic)
  • Re: area of circle
    ... formalized in ZFC are the result of my not having gone through a rigorous ... examination of how to formalize the classical geometrical definition of pi ... "modern" axiomatization of geometry? ... classical Euclidean geometry, ...
    (sci.math)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... amount of set theory, and then introductory abstract algebra, ... mathematics can be formulated; I didn't say that someone belabored the ... What is the proof that you would formalize? ... S is recursively enumerable & the complement of S is recursively ...
    (sci.logic)
  • Re: Kuratowski Ordered Pair
    ... mathematics chronologically to go along with its logical order. ... one application is in the meta-theory (the mathematical logic ... ABOUT set theory) and the other in the object theory (the set theory ... This is the nature of the beast: If you formalize a theory ...
    (sci.math)
  • Re: Kuratowski Ordered Pair
    ... mathematics chronologically to go along with its logical order. ... one application is in the meta-theory (the mathematical logic ... ABOUT set theory) and the other in the object theory (the set theory ... This is the nature of the beast: If you formalize a theory ...
    (sci.math)