Hi.

> This argument, taken to its limit, is known as "ZFC", the
> zermelo-frenkel-axiom-of-choice axioms. Some mathematicians, the
> constructivists, try to ground everything in ZFC.

Sorry, but at these points you are just wrong. Using ZFC, or for
that matter ZF+something as an axiomatic basis for mathematics
is a way to provide a common set of axioms for abstract reasoning,
it has nothing to do with grounding as discussed here. Moreover,
constructivists limit the way proofs are done, they usually do not
have anything against ZF.

> False. There are non-ZFC systems that get explored.

Yes, usually ZF+something as far as axioms are concerned. There
are as well other proof systems and other non-ZF foundations for
mathematics, but all of these can be embedded in ZF+something
if needed - as this is the basis for establishing their correctness.

> More generally, the study of what one can derive from a set of axioms is
> known as "first-order logic", which taken to its abstraction, involves
> the category of logic, aka Grothendieck's Topos theory.

First-order logic is just one kind of logic and there is indeed a calculus
for it that allows you to make derivations syntactically. But the study of
first-order logic is by no means limited to syntactic derivations nor are
all derivations done as for first-order logic - even the constructivists you
mention use their own calculus.

> Then, there's things like "model theory" which simply aren't grounded
> in this way.

Almost all proofs in model theory can be derived from ZFC axioms in
first-order logic, perhaps some very rare proofs assume a little bit more.

> Modern algebraic geometry, e.g. schemes, are not grounded on ZFC, mostly
> cause its not constructivist. Non-concrete categories are, well,
> roughly speaking bigger than the biggest infinities, and so ZFC doesn't
> really address that.

All modern mathematics can be traced back to ZF+something, even
category theory can be defined (I guess assuming some large cardinals).
It is good that it can be done, as it gives a quite uniform notion of
correctness. But obviously this is not the only way to see it and hardly
any mathematician uses only ZFC axioms directly in his work.

I think that people normally use much more concrete models in their
heads when working and only later write proofs down in an abstract way.
This I guess is captured more formally by things like representations (think
of base-ten encoded numbers as a representation of numbers meant in
an abstract way) and there is a large theory of representations already
developed and used in mathematics. I think this theory has more to do with
grounding as meant in this thread than ZFC axioms.

- lk

-----
This list is sponsored by AGIRI: http://www.agiri.org/email
To unsubscribe or change your options, please go to:
http://v2.listbox.com/member/?member_id=8660244&id_secret=53235675-032f5a

Reply via email to