[FOM] A question about isomorphic structures
louis.garde at free.fr
Sun Mar 27 05:36:36 EDT 2016
Le 26/03/2016 18:01, Arnon Avron a écrit :
> By the way, is "the carrier of a structure A" not
> a *set*? If not - what is it? And if yes - does not it means that
> we still need some set theory for the alleged "alternative foundations"?
The structures in HoTT are formally defined in the same way as the sets
So "the carrier of a structure A" in HoTT means the same thing as "the
carrier of a set S" in set-theory.
What is the "carrier of a set S" for you ? Some sort of meta-set ?
It's not easy to answer what "the carrier of a structure A" is, just as
it is not easy to answer what "carrier of a set S" is.
But there is a different way to look at mathematical objects.
A structure is defined with (formal) rules, and its "carrier" is any
collection of objects, in mathematics or anywhere else, that satisfies
Once defined, the structure can be mapped to many different possible
With classical foundations, you first define a "carrier" - sets - and
then define structures above them.
With HoTT, you first define structures, and then study their "carriers".
The univalent axiom says that two equivalent structures (that share the
same "carriers") are identical (share the same properties).
In a set-theoretic point of view, it does not really make sense: two
equivalent structures defined on differents sets always have some
differents properties, so they cannot be identical.
For instance, [0, 1, ...] is equivalent to [1, 2, ...] but not
identical, as 0 is member of the first set, but not of the second.
How to define natural numbers in set-theory ? There are many equivalent
ways to do it.
All these definitions are equivalent, but the resulting sets are not
identical. So what are the 'real' natural numbers ? Is '0' really the
empty set, or not ?
There can be no good answer to these questions in set theory; but
usually we do not really care, because we understand intuitively that
the 'real' natural numbers are "what is common to all the possible
equivalent definitions". In other words, what is interesting is the
structure of the natural numbers, not their possible "carriers".
This is exactly what HoTT and its univalent axiom allows you do to.
> I guess that I'll get here answers of the type "you are trying
> here to understand things from the set-theoretical point of view,
> using the set-theoretical language, instead of trying to understand
> them from the internal HoTT point of view, using its own language".
> This might well be true. But then I see no point in arguing with a
> camp with which I do not share even my basic language and concepts.
That's a strange point of view ! For sure if we start from the
assumption that "ZFC is the foundation", then there is not much to argue.
I can understand that in your daily work you are not interested in HoTT,
and there is no point in arguing about it.
But from the "philosophical" or "metamathematical" point of view, there
are concepts in HoTT that you cannot just ignore, unless you think that
HoTT is not valid mathematics (which would be a very restrictive point
of view), or you admit that you are not interested in foundation of
-all- mathematics, but only in foundation of -set-theoretic- mathematics.
If you are interested in foundation of all mathematics, and think that
set-theory explains everything, then it is a challenge for you to show
how to re-write in set-theory the basic concepts of HoTT, including its
definition of logical consequence, and logical negation.
More information about the FOM