|
|
tchow@xxxxxxxxxxxxx wrote:
> In article <rkmFg.421858$Mn5.15315@pd7tw3no>,
> Nam Nguyen <namducnguyen@xxxxxxx> wrote:
> >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)?
You could formalize some meta-theory about G.
> > In other words, how could we possibly
> >come up with a specific model of G in which the 5th is false?
Constructing a counter-model is only one way of proving
something unprovable. There are other ways. But if you want
to do it this way, you do indeed have to pause to ask yourself,
Just What Kind Of Thing is a model?
In the modern paradigm, a model is a structure, that is, it is
something that gets associated to components of the language
in which the axioms are stated. It has a function for every (named)
function in the (signature of the) language and a relation for every
predicate in (the signature of) the language. The question of what
the ranges of these functions (or the domains of these relations)
can be is complicated. In principle, arguably, they could be anything.
In practice, they are usually sets; ZFC is the default
model-construction
language.
> 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.
That is far from clear.
"A geometry" is ambiguous in this context; it could itself
be just a theory. What you need to construct is a MODEL of
the axiom-set "the axioms of G plus the denial of the axiom you
were trying to prove independent". Presumably you already have
a model of "the axioms of G plus the axiom you were trying to
prove independent". Whatever language you used to describe
the previous model (the one asserting/confirming the independent
axiom) will serve as a foundation for a language in which you could
specify the counter-model (the one denying the independent axiom),
but it may not be sufficient; the counter-model may need new terms;
if the independent axiom was a universal generalization then the
counter-model may require the existence of things that couldn't exist
in the affirming model, or that, even if they could exist, weren't
named
in the language.
> 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.
This is over-stating the case. His specific question was about
specifying
a counter-model. What are some relevant guidelines for that? How
does
anybody ever, given L, specify an L-structure? The fact that
structures nowadays are usually defined in terms of functions -- and
that these functions have domains that are sets (indeed, the model
in general has to have a domain that is a collection) means
that something like ZFC is necessarily/inescapably going to be
relevant.
> Your question might
> therefore be, can we formalize the construction of a non-Euclidean
> geometry without using set theory?
This is a stupid question; I mean, OF COURSE we can
specify a non-Euclidean geometry without using sets.
The original question, however, involved proving the indpendence
of an axiom, via the specific tactic of constructing a counter-
model. It is the model-construction part, NOT the non-
Euclidean geometry part, that is insisting on ZFC (or on SOME
model-construction language that relies heavily on functions).
> 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,
Wrong. Set theory IS NOT about formalizing proofs, in the context
of this question. IT IS about constructing models. The existence
of a model can and does all by itself prove some things, but that
is not the point. The point is that proofs are in the theory and
models
are in the meta-theory.
> although if you insist on dispensing with set theory, you can probably
> choose some other general foundation for mathematics,
You mean, in this context, "model-construction language".
> and that will work just as well. If you use set theory, then the full power
> of
> ZF(C) is almost certainly not needed.
It goes without saying that if your language is
rich enough to have infinitely many terms (e.g., if it has both a
constant
and a function) then your axioms have a model where every object
in the domain of quantification is a term in the language.
You don't need to use ZFC or anything else
to construct the domain of the model. But you may need to use
something
close to it for describing the functions and predicates over this
domain.
|
|