Possibly silly question about HoTT as a foundation

[Matt Oliveri]

In what sense(s) can HoTT be a foundational system?

Would it be fair to say that HoTT is still conceptually dependent on the non-invariant notion of strict equality because of judgmental equality (at the very least)?

Can HoTT be a conceptually self-contained foundation in light of this?

Thanks, I've been wondering these for a while.

[Andrej Bauer]

I am just now writing up slides for a tutorial on reals in HoTT and I
had to explain in what sense judgmental equality is "not logic".

I would put it as follows. The formal rules of type theory tell us two things:

1. How to *construct* stuff -- types and their elements (intro rules)

2. How to *use* stuff by (elimination rules)

3. When we are allowed to replace one construction by another (equality rules)

The equality rules are thus not about some prior notion of equality.
Rather, they again describe constructions, or at least one aspect of
them: when is one construction equivalent/replaceable/convertible with
another one. This is a primitive notion, just like "type" and
"element" are primitive notions.

Whether this is a satisfactory "foundational system" depends on what
one is looking for. There is certainly ample evidence that a lot of
mathematics (including logic) can be derived within such a system.

With kind regards,

Andrej

> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Peter LeFanu Lumsdaine]

On Sun, Sep 14, 2014 at 10:25 AM, Matt Oliveri <atm...@gmail.com> wrote:

I guess it depends what you mean by “self-contained”.

Studying HoTT as a logical system (an “object theory”), judgemental equality is a proposition in the *meta-theory*, which is not invariant under the propositional equality of the object theory.  But that’s fine, and doesn’t prevent the meta-theory itself from also being HoTT.

It seems parallel to the observation that in the proof theory of ZFC, syntactic equality is a non-extensional notion — the terms “{0,1}” and “{1,0}” are syntactically different, although by extensionality, they must denote the same set, i.e. must be provably equal in the object theory.  But this doesn’t cause problems with using ZFC as its own meta-theory, or make ZFC less self-contained as a foundation.

It’s also worth noting that when using HoTT as its own meta-theory, syntax provably forms a *set* (at least under the more straightforward constructions of syntax), so syntactic equality is very well-behaved.

So for these reasons, I wouldn’t see this as making HoTT less self-contained as a foundation.

On the other hand, subtleties of judgemental equality do become an issue when using HoTT to study its own *model* theory — see e.g. Mike’s blog post http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/ for a lot of details on this.  Essentially, it’s unproblematic to (working in HoTT as a meta-theory) redo the standard theory of what models of type theory are, and how they behave; but it seems difficult to actually *construct* such models from universes, in the way that one might expect to.  And non-truncatedness of the universe is the major obstacle there.

–p.

[Vladimir Voevodsky]

Hello,

1. First of all HoTT is not a foundational system. The foundations of mathematics that HoTT is related to are called the Univalent Foundations.

HoTT is the study of a meta-theory of the Univalent Foundations. The analog of "Homotopy Type Theory" in the current set-theoretic foundations is "Set Theory" as a theory of predicate logic - the study of axioms, models etc. 

It is unfortunate that set theoretic foundations of mathematics do not have a name to clearly distinguish them from the study of formal set theory in predicate logic. 

In our foundations there is such a distinction - HoTT is about a particular approach to the meta-theory, the one based Type Theory. 

The Univalent Foundations are the foundations based on the idea of h-levels, on the stratification of mathematical objects into propositions, sets and higher types  that correspond to higher groupoids.  

It is possible that in the future an entirely different approach to the meta-theory of the Univalent Foundations will be found, just as the formalization of sets as types of h-level 2 in the MLTT provides an approach to the meta-theory of the set-theoretic foundations that is entirely different from the one provided by the "set theory".

 2. There is a more narrow reading of HoTT in which HoTT is the name of  particular type system. This is probably what you had in mind in your questions. This reading, in particular for the reason you mention, does not make much sense. 

The more we study HoTT (as a subject) the more we understand that there can be no single type system that is the best one. 

On the more abstract level it is due to Goedel's results. 

On a more concrete level it is due to the fact that there can be a system A of strict equalities and a system B of strict equalities, both A and B being consistent with the Univalence Axiom but the system A + B being inconsistent.

It is similar to the phenomenon first observed probably by Carlos Simpson that when trying to replace an n-category by an equivalent strict n-category it might be possible to make associativity strict but then the units must be weak or to make the units strict but then the associativity must me weak. 

Whether a particular system A of strict equalities can be combined with another system B can be a very difficult question. For example it is currently a conjecture that the system of strict equalities validated by the cubical set model that includes, for example, that the application of functions to paths is strictly associative,  can be extended by adding the strict reduction rule for the J eliminator that exists in the original MLTT. But this conjecture remain open despite a lot of effort to prove it. 

3. The way I see things is that we will have many type systems that can be used to do mathematics in the univalent style. We will create an infrastructure that will help us to describe such systems formally and to construct models and interpretations of these systems in the each other or in the ZFC, formally. 

The system of mathematical objects and constructions being created by us and certified for correctness with this infrastructure then will be 'the HoTT". 

Vladimir.

[Matt Oliveri]

On Sunday, September 14, 2014 6:01:13 AM UTC-4, Andrej Bauer wrote:

I am just now writing up slides for a tutorial on reals in HoTT and I
had to explain in what sense judgmental equality is "not logic".

Cool. I'd like to see them.

The equality rules are thus not about some prior notion of equality.

Can you explain what you mean by that? I understand how the role of judgmental equality is to allow certain constructions, but it still seems to do that by providing an appropriate notion of equality. It's part of the definition of the system whether it's considered "prior" or not.

Whether this is a satisfactory "foundational system" depends on what
one is looking for. There is certainly ample evidence that a lot of
mathematics (including logic) can be derived within such a system.

That's one of the things I want to understand. Why does the ability to derive a lot of math make it a foundation? I can write a lot of programs in Java (or Haskell, or OCaml...), but it's no foundation of software.

Thanks.

[Matt Oliveri]

On Sunday, September 14, 2014 6:28:23 AM UTC-4, Peter LeFanu Lumsdaine wrote:

I guess it depends what you mean by “self-contained”.

Studying HoTT as a logical system (an “object theory”), judgemental equality is a proposition in the *meta-theory*, which is not invariant under the propositional equality of the object theory.  But that’s fine, and doesn’t prevent the meta-theory itself from also being HoTT.

I agree that HoTT can reason about and model itself, that's not what I mean. Actually I'm not completely sure what I mean about "self-contained". So the right meaning, if any, is up for discussion. I'm just picking up on a feeling that "everything" should be homotopy invariant, but meanwhile judgmental equality isn't. It's that idea, which I might be oversimplifying, that doesn't seem self-contained.

It seems parallel to the observation that in the proof theory of ZFC, syntactic equality is a non-extensional notion — the terms “{0,1}” and “{1,0}” are syntactically different, although by extensionality, they must denote the same set, i.e. must be provably equal in the object theory.  But this doesn’t cause problems with using ZFC as its own meta-theory, or make ZFC less self-contained as a foundation.

Syntactic equality is not part of the semantics of ZFC. But it seems like judgmental equality is part of the semantics of HoTT.

It’s also worth noting that when using HoTT as its own meta-theory, syntax provably forms a *set* (at least under the more straightforward constructions of syntax), so syntactic equality is very well-behaved.

I can't tell what point you're making here. Judgmental equality needs to be interpreted as some kind of equality on objects, it seems. Syntactic equality is just incidental and was never supposed to be problematic.

So for these reasons, I wouldn’t see this as making HoTT less self-contained as a foundation.

On the other hand, subtleties of judgemental equality do become an issue when using HoTT to study its own *model* theory — see e.g. Mike’s blog post http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/ for a lot of details on this.  Essentially, it’s unproblematic to (working in HoTT as a meta-theory) redo the standard theory of what models of type theory are, and how they behave; but it seems difficult to actually *construct* such models from universes, in the way that one might expect to.  And non-truncatedness of the universe is the major obstacle there.

Yeah, that's a very interesting post. I've reread it many times, and I'm responsible for about half the noise in the comments area. :)
Thinking about the problem did sort of prompt my questions, but judgmental equality seems to stick out from the rest of the system even once all the technical problems are solved.

[Matt Oliveri]

On Sunday, September 14, 2014 7:57:06 AM UTC-4, v v wrote:

Hello,

1. First of all HoTT is not a foundational system. The foundations of mathematics that HoTT is related to are called the Univalent Foundations.

HoTT is the study of a meta-theory of the Univalent Foundations. The analog of "Homotopy Type Theory" in the current set-theoretic foundations is "Set Theory" as a theory of predicate logic - the study of axioms, models etc. 

It is unfortunate that set theoretic foundations of mathematics do not have a name to clearly distinguish them from the study of formal set theory in predicate logic. 

In our foundations there is such a distinction - HoTT is about a particular approach to the meta-theory, the one based Type Theory. 

The Univalent Foundations are the foundations based on the idea of h-levels, on the stratification of mathematical objects into propositions, sets and higher types  that correspond to higher groupoids.  

It is possible that in the future an entirely different approach to the meta-theory of the Univalent Foundations will be found, just as the formalization of sets as types of h-level 2 in the MLTT provides an approach to the meta-theory of the set-theoretic foundations that is entirely different from the one provided by the "set theory".

Interesting. I'm actually asking about the idea that "everything" in a foundational system should be homotopy invariant. In HoTT (no specific system, as long as it's something like MLTT) at least judgmental equality is not homotopy invariant. But this doesn't seem unusually bad. In (higher) category theory, composing morphisms depends on the morphisms lining up strictly. And the classical definition of homotopy uses strict equality too.

Maybe I was wrong to assume that anyone wanted literally everything to be homotopy invariant.

2. There is a more narrow reading of HoTT in which HoTT is the name of  particular type system. This is probably what you had in mind in your questions. This reading, in particular for the reason you mention, does not make much sense.

No, sorry about the confusion. I'm talking about the kinds of systems HoTT researchers have been talking about, not any one in particular.

The more we study HoTT (as a subject) the more we understand that there can be no single type system that is the best one. 

On the more abstract level it is due to Goedel's results. 

On a more concrete level it is due to the fact that there can be a system A of strict equalities and a system B of strict equalities, both A and B being consistent with the Univalence Axiom but the system A + B being inconsistent.

It is similar to the phenomenon first observed probably by Carlos Simpson that when trying to replace an n-category by an equivalent strict n-category it might be possible to make associativity strict but then the units must be weak or to make the units strict but then the associativity must me weak. 

Whether a particular system A of strict equalities can be combined with another system B can be a very difficult question. For example it is currently a conjecture that the system of strict equalities validated by the cubical set model that includes, for example, that the application of functions to paths is strictly associative,  can be extended by adding the strict reduction rule for the J eliminator that exists in the original MLTT. But this conjecture remain open despite a lot of effort to prove it.

OK. But my question applies regardless of which specific strict equations are available, or the consistency strength of the system.

3. The way I see things is that we will have many type systems that can be used to do mathematics in the univalent style. We will create an infrastructure that will help us to describe such systems formally and to construct models and interpretations of these systems in the each other or in the ZFC, formally.

Yes, this project seems like a great idea to me...

The system of mathematical objects and constructions being created by us and certified for correctness with this infrastructure then will be 'the HoTT".

...but my question isn't about the details of any particular metatheory or models. It's about the idea of wanting things to be homotopy invariant, and whether this is a reasonable thing to want in a foundation. I'm completely OK with all of the work around UF and HoTT, but I don't see how it's foundational.

Thanks.

[Michael Shulman]

I think there are several different questions here that are being confused.


Question 1: Is HoTT (or, more specifically, any particular type theory
used for HoTT) a foundational system?

Answer 1: Yes: it suffices to represent practically all known
mathematics, and plenty of as-yet-unknown mathematics. It is indeed
the case that any Turing-complete programming language could
equivalently be called a "foundation of programming". Computer
scientists don't generally speak that way, but by analogy they could.


Question 2: Is there a foundational system in which absolutely
everything is homotopy invariant?

Answer 2: This is an interesting question, and I don't think the
answer is known. You're quite right that the presence of strict
equality in all known type theories for HoTT means that they are not
such. It's reasonable to hope for such a thing, but I think it's
fairly likely that the answer is "yes, but it's too cumbersome to
actually use for anything." But even if the answer is "no", it
doesn't detract at all from the fact that current type theories for
HoTT can serve as foundations for mathematics, and are *extremely*
homotopy invariant even if not *completely* so.


Question 3: Does the presence of judgmental equality in type theories
for HoTT make them any less "self-contained"?

Answer 3: No. A type theory is a set of rules and axioms formulated
in a deductive system, and judgmental equality, being a judgment, is
part of that deductive system in the same way that a typing judgment
a:A is. It exists at a different level *within* the system from
propositional equality, but it's still part of the type theory.
Analogously, set theory is generally formulated with axioms inside the
deductive system of first-order logic, in which the primary judgment
is "P is true/provable", existing at a different level from the
proposition "P" itself. When we construct a model of such a type
theory, we have to interpret judgmental equality and propositional
equality by different things, and usually we interpret them by a
"strict" equality and by "homotopies", but we are interpreting the
whole system of which both are a part.

Mike

[Matt Oliveri]

On Sunday, September 14, 2014 11:49:38 PM UTC-4, Michael Shulman wrote:

I think there are several different questions here that are being confused.


Question 1: Is HoTT (or, more specifically, any particular type theory
used for HoTT) a foundational system?

Answer 1: Yes: it suffices to represent practically all known
mathematics, and plenty of as-yet-unknown mathematics.  It is indeed
the case that any Turing-complete programming language could
equivalently be called a "foundation of programming".  Computer
scientists don't generally speak that way, but by analogy they could.

I don't think it'd make much sense to call any Turing-complete language a "foundation of programming". One can design arbitrarily bad Turing-complete languages, which no one would dream of using. Actually, I'd say the foundation of (computer) programming is computers themselves. The actual programmable physical objects. With math though, I don't think things can be so clear cut, unless you're a Platonist. But I still would've hoped the conditions for a foundation of math would be stronger than just the ability to develop enough math with it.

One of my original questions was "In what sense(s) can HoTT be a foundational system?". I agree that HoTT can develop tons of math, if you're saying that's the only sense in which HoTT is a foundation. But I thought there was more to it than that.

Question 2: Is there a foundational system in which absolutely
everything is homotopy invariant?

Answer 2: This is an interesting question, and I don't think the
answer is known.  You're quite right that the presence of strict
equality in all known type theories for HoTT means that they are not
such.

OK good, we agree so far.

It's reasonable to hope for such a thing,

Is it though? I didn't ask that, but it's worth asking. To me it seems like the advantage of HoTT is it allows the convenient and abstract construction of homotopy invariant things. I actually don't see why it's a problem to have non-invariant things around, other than that it ruins the (perhaps artificial) goal of a conception of math where literally everything is homotopy invariant. In fact, so far it looks to me like non-invariant things are a great thing to have around.

but I think it's
fairly likely that the answer is "yes, but it's too cumbersome to
actually use for anything."  But even if the answer is "no", it
doesn't detract at all from the fact that current type theories for
HoTT can serve as foundations for mathematics, and are *extremely*
homotopy invariant even if not *completely* so.

I give up, how would you even begin to try defining a system where literally everything is invariant? Oh wait, does it have something to do with the peculiar restrictions seemingly imposed by inductive-inductive interpretability?

Just to check: being "*extremely* homotopy invariant" is no reason to be a foundation. Because as long as there are any non-invariant notions, the concepts involved are fundamentally the same as with classical homotopy theory.

Question 3: Does the presence of judgmental equality in type theories
for HoTT make them any less "self-contained"?

Answer 3: No.  A type theory is a set of rules and axioms formulated
in a deductive system, and judgmental equality, being a judgment, is
part of that deductive system in the same way that a typing judgment
a:A is.  It exists at a different level *within* the system from
propositional equality, but it's still part of the type theory.
Analogously, set theory is generally formulated with axioms inside the
deductive system of first-order logic, in which the primary judgment
is "P is true/provable", existing at a different level from the
proposition "P" itself.  When we construct a model of such a type
theory, we have to interpret judgmental equality and propositional
equality by different things, and usually we interpret them by a
"strict" equality and by "homotopies", but we are interpreting the
whole system of which both are a part.

It sounds like you're pointing out that judgmental equality is still part of the language even though it can't be reflected as a type, and therefore the language is self-contained. But I hope not, because that seems tautological. Of course a formal system includes everything that it includes, in exactly the way that it does so. Another reason why I think I'm not understanding you is that the need to interpret judgmental equality seems more like a problem than a solution.

Thanks.

[David Roberts]

On 15 September 2014 15:23, Matt Oliveri <atm...@gmail.com> wrote:
> One can design arbitrarily bad Turing-complete languages, which no one would
> dream of using.

In mathematical terms, this is ZFC.
:-D

David

[Michael Shulman]

On Sun, Sep 14, 2014 at 10:53 PM, Matt Oliveri <atm...@gmail.com> wrote:
> But I still would've hoped the
> conditions for a foundation of math would be stronger than just the ability
> to develop enough math with it.

Do you have any suggestions for what other conditions one might
impose? I've never heard of any. Of course one foundation of math
can be a *better* one than another, just like one programming language
can be better than another, in the sense of being easier to use, more
powerful, more convenient for many purposes, etc., but that's a
different question.

>> It's reasonable to hope for such a thing,
>
> Is it though? I didn't ask that, but it's worth asking.

I think that from a higher-category-theorist's perspective, without
knowing much about foundations, it's reasonable to hope for.

> I give up, how would you even begin to try defining a system where literally
> everything is invariant?

I don't really know; that's why I said it was an interesting problem.
One might start by taking an existing type theory for HoTT and making
absolutely all the judgmental equalities into propositional ones. But
would that be a workable system? I don't know.

> Just to check: being "*extremely* homotopy invariant" is no reason to be a
> foundation.

Homotopy-invariance is an unrelated question to being a foundation or
not. ZFC is a foundation, but it is decidedly not homotopy-invariant.

> It sounds like you're pointing out that judgmental equality is still part of
> the language even though it can't be reflected as a type, and therefore the
> language is self-contained. But I hope not, because that seems tautological.

Yes, that's what I was saying. It is tautological. What do *you*
mean by "self-contained"?

It's important to separate semantics from foundations. When using
HoTT as a foundation, we don't need to think about "interpreting" it
anywhere; we just take it as it is.

Mike

[Matt Oliveri]

That's a joke right? If you've seen some of the "esoteric" programming languages, then you know that even ZFC is pleasant by comparison.

[David Roberts]

Yes, of course there are much worse one can do. For instance, NFU is
even worse than ZFC (and has major failings on top of that - lack of
cartesian closure of the category of NFU sets being one of them).

Bourbaki's set theory was such that the definition of the number 1
would take over a trillion symbols (see
https://www.dpmms.cam.ac.uk/~ardm/inefff.pdf).

But people don't do mathematics in the ZFC language, in reality, even
set theorists, generally speaking. They use much higher-level stuff.

David

[Andrej Bauer]

On Mon, Sep 15, 2014 at 2:53 AM, Matt Oliveri <atm...@gmail.com> wrote:
> Can you explain what you mean by that? I understand how the role of
> judgmental equality is to allow certain constructions, but it still seems to
> do that by providing an appropriate notion of equality

If we understand substitution as a form of construction (which we
certainly should in type theory) then judgmental equality gives us
preconditions for certain substitution-constructions. And since
substitution itself requires no notion of equality (except being able
to recognize variables and to handle alpha-equivalence), we may
explain judgmental equality in terms of its role in
subtitution-construction.

> It's part of the definition of the system whether it's considered "prior" or not.

I am confused as to how it can be. A foundational system is a
self-contained contraption. It is *motivated* by external factors
(such as pre-mathematical intuitions), but we have learned not to mix
philosophy with mathematics. A foundational system must stand on its
own, to the greatest extent possible. Whether a particular concept in
a foundational system is "prior to the system" is precisely the kind
of philosophy that may lurk around the foundational system, but should
never be allowed to enter it -- at least not under the current
conception of what a formal system may be.

With kind regards,

Andrej


With kind regards,

Andrej

[Matt Oliveri]

On Monday, September 15, 2014 2:00:41 AM UTC-4, Michael Shulman wrote:

On Sun, Sep 14, 2014 at 10:53 PM, Matt Oliveri <atm...@gmail.com> wrote:
> But I still would've hoped the
> conditions for a foundation of math would be stronger than just the ability
> to develop enough math with it.

Do you have any suggestions for what other conditions one might
impose?  I've never heard of any.  Of course one foundation of math
can be a *better* one than another, just like one programming language
can be better than another, in the sense of being easier to use, more
powerful, more convenient for many purposes, etc., but that's a
different question.

I guess I don't have any non-negotiable demands to add. I'm saying that what makes a good foundation is different from what makes non-foundational theories good.

It seems to me that a foundation should have as little conceptual and technical baggage as possible, while still being able to encode all math. The encoding can be complex and cumbersome, as long as it can be done once and for all. Notice that ZF has HoTT beat hands down on conceptual and technical simplicity.

With the goal of machine checked math in mind, another good feature for a foundation is having some kind of synergy with the foundations of computation. HoTT seems headed in the wrong direction here, since most programs are not higher-dimensional. (And no program is fundamentally higher dimensional, given that computers encode everything as binary.) But maybe there's a foundationally-useful synergy I don't know.

>> It's reasonable to hope for such a thing,
>
> Is it though? I didn't ask that, but it's worth asking.

I think that from a higher-category-theorist's perspective, without
knowing much about foundations, it's reasonable to hope for.

But the experience so far has been that not having propositional strict equality makes some things difficult. Presumably, not having judgmental equality would make even more things difficult. What benefits would a higher-category-theorist be hoping to obtain that would offset these difficulties?

> I give up, how would you even begin to try defining a system where literally
> everything is invariant?

I don't really know; that's why I said it was an interesting problem.
One might start by taking an existing type theory for HoTT and making
absolutely all the judgmental equalities into propositional ones.  But
would that be a workable system?  I don't know.

The language I tried to interpret is instructive. Ostensibly, it didn't have judgmental equality, because all the terms were normal forms. But the interpretation in HoTT didn't work anyway, apparently because of type equality used by applications not being interpretable in any obvious way. Even without asking for any particular equations, the usual presentation of dependent type theory effectively defaults to syntactic equality as judgmental equality, and that's not invariant either. Removing judgmental equality from a dependent type system is already a problem. That's why I was wondering if you were thinking of the inductive-inductive approach, which seems to smoke out this kind of implicit judgmental equality.

> Just to check: being "*extremely* homotopy invariant" is no reason to be a
> foundation.

Homotopy-invariance is an unrelated question to being a foundation or
not.  ZFC is a foundation, but it is decidedly not homotopy-invariant.

Good, that's what I thought.

> It sounds like you're pointing out that judgmental equality is still part of
> the language even though it can't be reflected as a type, and therefore the
> language is self-contained. But I hope not, because that seems tautological.

Yes, that's what I was saying.  It is tautological.  What do *you*
mean by "self-contained"?

Like I said to Peter Lumsdaine, I'm not really sure what I mean either. I just had a sense. I was hoping the discussion would work out the proper meaning, but since no one seems to know what I could mean, I guess there's no problem.
 

It's important to separate semantics from foundations.  When using
HoTT as a foundation, we don't need to think about "interpreting" it
anywhere; we just take it as it is.

Right, we don't need to, but if a foundation can only interpret itself indirectly, say via an encoding as sets, then it seems like a hint that you've taken a detour through a superior foundation. I'm just speaking generally though. I think a HoTT system can have a direct interpretation of (a smaller version of) itself.

[Michael Shulman]

On Sun, Sep 14, 2014 at 11:56 PM, Matt Oliveri <atm...@gmail.com> wrote:
> I guess I don't have any non-negotiable demands to add. I'm saying that what
> makes a good foundation is different from what makes non-foundational
> theories good.

Sure. But what makes a foundational theory *good* is a different
question from what makes a theory foundational at all. (-:

> What benefits would a higher-category-theorist be hoping to obtain
> that would offset these difficulties?

The assurance that everything is invariant. (-:

Mike

[Matt Oliveri]

But one shouldn't expect everything to be invariant. Thanks to HoTT, those things expected to be invariant can often be made invariant by construction. That seems like the real win. And we've basically won as long as we keep this homotopy invariant mode. Adding non-invariant things in such a way that the invariant mode still works still seems alright to me.

[Michael Shulman]

On Mon, Sep 15, 2014 at 12:28 AM, Matt Oliveri <atm...@gmail.com> wrote:
> But one shouldn't expect everything to be invariant.

If one is a higher category theorist, why not?

[Matt Oliveri]

Well a higher category theorist can expect what they want. I guess this is a way that math is different from programming. One typically doesn't write a program because they expect it's possible. But maybe that's just me being cynical.

[Matt Oliveri]

On Monday, September 15, 2014 2:37:08 AM UTC-4, Andrej Bauer wrote:

On Mon, Sep 15, 2014 at 2:53 AM, Matt Oliveri <atm...@gmail.com> wrote:
> Can you explain what you mean by that? I understand how the role of
> judgmental equality is to allow certain constructions, but it still seems to

> do that by providing an appropriate notion of equality.

If we understand substitution as a form of construction (which we
certainly should in type theory) then judgmental equality gives us
preconditions for certain substitution-constructions. And since
substitution itself requires no notion of equality (except being able
to recognize variables and to handle alpha-equivalence), we may
explain judgmental equality in terms of its role in
subtitution-construction.

It sounds like you're saying you could rearrange the rules so that judgmental equality is only used in some substitution rule? And maybe even that you'd only need equality of variables somehow?

Can you point me to some typing rules that demonstrate what you're talking about? I don't understand yet.

> It's part of the definition of the system whether it's considered "prior" or not.

Whether a particular concept in
a foundational system is "prior to the system" is precisely the kind
of philosophy that may lurk around the foundational system, but should
never be allowed to enter it -- at least not under the current
conception of what a formal system may be.

It sounds like we agree on this then. I wasn't sure what you meant by "prior" in the first place.

[Michael Shulman]

On Mon, Sep 15, 2014 at 12:50 AM, Matt Oliveri <atm...@gmail.com> wrote:
>> > But one shouldn't expect everything to be invariant.
>>
>> If one is a higher category theorist, why not?
>
> Well a higher category theorist can expect what they want. I guess this is a
> way that math is different from programming. One typically doesn't write a
> program because they expect it's possible. But maybe that's just me being
> cynical.

I'm not sure what your point is. We don't generally do things in math
for no other reason than that we expect them to be possible either.
The reason for hoping to be able to make everything invariant would
be, as I said, that then everything would be automatically invariant.
Higher category theorists are interested mainly in properties of
higher categories that are invariant under equivalence, and those of a
certain philosophical bent may consider non-invariant properties of
such to be meaningless. Non-invariant properties are obviously
technically useful with current technology, but this brings along with
it certain baggage like having to make sure that the properties we are
interested in are actually invariant. Since (the argument goes)
non-invariant properties have no "real" mathematical meaning, why not
hope for a system in which they don't even exist?

I'm not necessarily saying I subscribe to such a view now, although I
have at times in the past (and I'm not saying I *don't* subscribe to
it now either). But I think it's a perfectly reasonable view.

[Vladimir Voevodsky]

On Sep 15, 2014, at 1:53 AM, Matt Oliveri <atm...@gmail.com> wrote:

That's one of the things I want to understand. Why does the ability to derive a lot of math make it a foundation? I can write a lot of programs in Java (or Haskell, or OCaml...), but it's no foundation of software.

What is a foundation of software?

V.

[Vladimir Voevodsky]

On Sep 15, 2014, at 2:53 AM, Matt Oliveri <atm...@gmail.com> wrote:

Interesting. I'm actually asking about the idea that "everything" in a foundational system should be homotopy invariant. In HoTT (no specific system, as long as it's something like MLTT) at least judgmental equality is not homotopy invariant. 

Judgmental equality can not be assumed (in a context) but only verified. So you may say that in the MLTT version of  the meta-theory everything that can be assumed (and in particular anything that can be used in an inductive argument) must be homotopy invariant.

In the HTS (https://github.com/vladimirias/2013_IAS_Joyal_Conference) non-homotopy invariant equality can be assumed at the cost of there being types (or fibrant types) and pre-types. The univalence axiom then only holds for types. Mathematically meaningful propositions and constructions should be objects of types. But pre-types can be used in the construction of objects of types making HTS into a potentially more powerful meta-theory than MLTT.

Vladimir.

[Matt Oliveri]

Good question. The term isn't used as far as I know. I was trying to draw an analogy between formalized math and programming. The foundation is the bottom part of a building, which everything else rests upon. Most high-level languages are not low-level enough to be a foundation, I'd say. With math, I suppose you get to pick which concepts are the low-level ones, but not with programming.

[Vladimir Voevodsky]

On Sep 15, 2014, at 7:37 AM, Andrej Bauer <andrej...@andrej.com> wrote:

If we understand substitution as a form of construction (which we
certainly should in type theory) then judgmental equality gives us
preconditions for certain substitution-constructions. And since
substitution itself requires no notion of equality (except being able
to recognize variables and to handle alpha-equivalence), we may
explain judgmental equality in terms of its role in
subtitution-construction.

Right!  In fact, I have been trying in my recent talks and conversations to use the 

names "substitutional equality" and "transportational equality".

However, I would suggest a further distinction keeping the name "judgmental" for the equality that 

can not be assumed but only verified.

Then in the MLTT the only substitutional equality is the judgmental one while in HTS we have a type-based 

substitutional equality.

Vladimir.

[Vladimir Voevodsky]

On Sep 15, 2014, at 7:56 AM, Matt Oliveri <atm...@gmail.com> wrote:

> It seems to me that a foundation should have as little conceptual and technical baggage as possible, while still being able to encode all math. The encoding can be complex and cumbersome, as long as it can be done once and for all. Notice that ZF has HoTT beat hands down on conceptual and technical simplicity.

In this sense all maths can be encoded in sequences of 0's and 1's and this "foundation" beats any other in the conceptual and technical simplicity.

Here is what I wrote for a general audience lecture on foundations at the IAS. I said that any usable foundation of mathematics should have at least three components:

> The first component is a formal deduction system: a language and rules of manipulating sentences in this language that are purely formal, such that a record of such manipulations can be verified by a computer program.
>
> The second component is a structure that provides a meaning to the sentences of this language in terms of mental objects intuitively comprehensible to humans.
>
> The third component is a structure that enables humans to encode mathematical ideas in terms of the objects directly associated with the language.

V.

[Vladimir Voevodsky]

On Sep 15, 2014, at 9:38 AM, Matt Oliveri <atm...@gmail.com> wrote:

With math, I suppose you get to pick which concepts are the low-level ones, but not with programming.

Not with programming so far while we only have one type of hardware...

But in maths there are indeed choices and a "foundation" became a misleading name because maths can exist quite well without

any foundation and there can be several foundations at a given time.

A foundation of maths is something like an accounting system that can be used to ensure that things are recorded properly

and that if there is a problem it can be localized and dealt with. 

That's why it is important that a foundation be convenient in practical use. 

Vladimir.

 

[Matt Oliveri]

On Monday, September 15, 2014 5:01:07 AM UTC-4, v v wrote:

On Sep 15, 2014, at 7:56 AM, Matt Oliveri <atm...@gmail.com> wrote:

> It seems to me that a foundation should have as little conceptual and technical baggage as possible, while still being able to encode all math. The encoding can be complex and cumbersome, as long as it can be done once and for all. Notice that ZF has HoTT beat hands down on conceptual and technical simplicity.

In this sense all maths can be encoded in sequences of 0's and 1's and this "foundation" beats any other in the conceptual and technical simplicity.

Sequences of 0's and 1's don't make a foundation by themselves, as you seem to know, since you put "foundation" in quotes. The bit sequences give you all the expressions you need, but you're missing the rules.

You can translate the expressions of an existing system to binary, but it won't make the system any simpler. Maybe you know a system as strong as ZF but simpler. Great! It's actually mainly the conceptual complexity of HoTT that worries me.

How would you teach an undergrad HoTT? It seems harder than teaching set theory. If they will go on to do homotopy theory or higher category theory, it's worth it. You've consolidated a lot of the basic ideas they'll need. But maybe not everyone who wants to write formal proofs needs all those ideas.

Here is what I wrote for a general audience lecture on foundations at the IAS. I said that any usable foundation of mathematics should have at least three components:

> The first component is a formal deduction system:  a language and rules of manipulating sentences in this language that are purely formal, such that a record of such manipulations can be verified by a computer program.
>
> The second component is a structure that provides a meaning to the sentences of this language in terms of mental objects intuitively comprehensible to humans.
>
> The third component is a structure that enables humans to encode mathematical ideas in terms of the objects directly associated with the language.

The first two components I agree are definitely necessary for a foundation of math. It's because of the second component that conceptual complexity should be low. Much better to intuitively explain a simple system and then formalize complex ideas, than to have to intuitively explain a complex system from scratch.

It's the third component that I'm not convinced should be built into a foundation. That can also be done within the foundational system. In software, implementations of high-level ideas can be in frameworks or libraries, rather than as part of a language implementation. They can be built into a high-level language, but they wouldn't be built into a low-level language.

I see HoTT-based systems as high-level mathematical languages. It seems weird to call a HoTT-based system a foundation if it's high-level.

[Peter LeFanu Lumsdaine]

On Mon, Sep 15, 2014 at 11:14 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:

A foundation of maths is something like an accounting system that can be used to ensure that things are recorded properly

and that if there is a problem it can be localized and dealt with. 

For this reason, I’d add another desideratum for a foundation, though I realise some might disagree: correctness of proofs should be decidable (and ideally, efficiently so).

Note that I’m *not* saying “type-checking should be decidable”.  There are good proposed type-theoretic foundations in which type-checking is undecidable, or not known to be decidable.  But these systems still have the more elaborated notion of a *derivation*, checking which is always (as far as I know) decidable; and when type-checking is undecidable, one can argue that derivations, not terms, are what deserve to be considered as the complete “proofs” of the system.

–p.

 

[Matt Oliveri]

On Mon, Sep 15, 2014 at 5:15 AM, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote:

Martin-Loef Type Theory.

MLTT is a great theory for understanding software, but I'm really glad computers don't directly run MLTT! :)

[Vladimir Voevodsky]

On Sep 15, 2014, at 10:52 AM, Matt Oliveri <atm...@gmail.com> wrote:

How would you teach an undergrad HoTT? It seems harder than teaching set theory.

HoTT is the study of the type-theoretic approach to the meta-theory of the Univalent Foundations. Why would you want to teach it to an undergrad?

One can ask how we will teach undergrad maths in the world where the Univalent Foundations are used for doing research maths. That I do not know.

V.

[Matt Oliveri]

On Monday, September 15, 2014 6:05:58 AM UTC-4, v v wrote:

On Sep 15, 2014, at 10:52 AM, Matt Oliveri <atm...@gmail.com> wrote:

How would you teach an undergrad HoTT? It seems harder than teaching set theory.

HoTT is the study of the type-theoretic approach to the meta-theory of the Univalent Foundations. Why would you want to teach it to an undergrad?

Indeed. It looks like I still didn't have your terminology straight. Sorry.

[Vladimir Voevodsky]

On Sep 15, 2014, at 10:52 AM, Matt Oliveri <atm...@gmail.com> wrote:

Here is what I wrote for a general audience lecture on foundations at the IAS. I said that any usable foundation of mathematics should have at least three components: 

> The first component is a formal deduction system:  a language and rules of manipulating sentences in this language that are purely formal, such that a record of such manipulations can be verified by a computer program. 
> 
> The second component is a structure that provides a meaning to the sentences of this language in terms of mental objects intuitively comprehensible to humans. 
> 
> The third component is a structure that enables humans to encode mathematical ideas in terms of the objects directly associated with the language.

The first two components I agree are definitely necessary for a foundation of math. It's because of the second component that conceptual complexity should be low. Much better to intuitively explain a simple system and then formalize complex ideas, than to have to intuitively explain a complex system from scratch.

It's the third component that I'm not convinced should be built into a foundation. That can also be done within the foundational system. 

In the ZFC-based foundations natural numbers have a complex definition. In particular natural numbers are not among the objects that are directly associated with the language.

But I would say that a foundation of maths should provide an explanation of what natural numbers are and how to work with them.

V.

[Matt Oliveri]

How about semi-decidable? That is, valid proofs are accepted, but invalid proofs might make the checker loop.
Is Andromeda checking decidable or semi-decidable? I figured semi-decidable, unless it can somehow avoid loops in the equality-reflected reduction rules.

[Matt Oliveri]

On Monday, September 15, 2014 6:10:20 AM UTC-4, v v wrote:

In the ZFC-based foundations natural numbers have a complex definition. In particular natural numbers are not among the objects that are directly associated with the language.

But I would say that a foundation of maths should provide an explanation of what natural numbers are and how to work with them.

I don't have a strong preference for whether to include natural numbers in a foundation. And I don't know why you brought up this example.

[Matt Oliveri]

On Monday, September 15, 2014 5:14:40 AM UTC-4, v v wrote:

On Sep 15, 2014, at 9:38 AM, Matt Oliveri <atm...@gmail.com> wrote:

With math, I suppose you get to pick which concepts are the low-level ones, but not with programming.

Not with programming so far while we only have one type of hardware...

But in maths there are indeed choices and a "foundation" became a misleading name because maths can exist quite well without any foundation and there can be several foundations at a given time.

Right.

A foundation of maths is something like an accounting system that can be used to ensure that things are recorded properly

and that if there is a problem it can be localized and dealt with. 

That's why it is important that a foundation be convenient in practical use.

It looks like there are actually two notions of foundation here, and I'm talking about one and you're talking about another. A foundation can be any sufficiently strong formal system used to informally justify informal mathematical reasoning, and also to formalize it rather directly. This is what I think you mean. Or a foundation can be any sufficiently strong formal system used to formally justify other formal systems and thus everything they justify, at any level of indirection. This is what I mean.

With the first notion, convenient formalization of new math is important. With the second notion it isn't. This difference in requirements really changes things! For notion two, with no emphasis on convenience, all emphasis is on simplicity, and on efficiency of computer implementations. For notion one, emphasis should indeed be on minimizing the conceptual translation burden for formalizing math research.

Is this right? It would really clear things up for me.

[Vladimir Voevodsky]

Or a foundation can be any sufficiently strong formal system used to formally justify other formal systems and thus everything they justify, at any level of indirection. This is what I mean.

I see now. This is a useful distinction. What you call a foundation I call "an etalon of consistency". For example ZFC is used as an etalon of consistency relative to which the consistency of the MLTT is shown. It is also used as the etalon of consistency for the type systems of HoTT through the use of univalent models. 

In this sense neither the original MLTT nor its strengthened versions that are used in the Univalent Foundations are foundational systems. 

For notion two, with no emphasis on convenience, all emphasis is on simplicity, and on efficiency of computer implementations. 

I am not sure why would you care about efficiency of an implementation. You are not going to actually use it for anything because the translation from the system that you actually use to an etalon of consistency may involve non-linear expansion in size.

Vladimir.

[Thorsten Altenkirch]

From: Vladimir Voevodsky <vlad...@ias.edu>
Date: Mon, 15 Sep 2014 09:11:56 +0100
To: Matt Oliveri <atm...@gmail.com>
Cc: "Prof. Vladimir Voevodsky" <vlad...@ias.edu>, "HomotopyT...@googlegroups.com" <HomotopyT...@googlegroups.com>
Subject: Re: [HoTT] Possibly silly question about HoTT as a foundation

On Sep 15, 2014, at 1:53 AM, Matt Oliveri <atm...@gmail.com> wrote:

That's one of the things I want to understand. Why does the ability to derive a lot of math make it a foundation? I can write a lot of programs in Java (or Haskell, or OCaml...), but it's no foundation of software.

What is a foundation of software?

Martin-Loef Type Theory.

V.

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.

[Peter LeFanu Lumsdaine]

On Mon, Sep 15, 2014 at 12:16 PM, Matt Oliveri <atm...@gmail.com> wrote:

On Monday, September 15, 2014 6:01:34 AM UTC-4, Peter LeFanu Lumsdaine wrote:

On Mon, Sep 15, 2014 at 11:14 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:

A foundation of maths is something like an accounting system that can be used to ensure that things are recorded properly

and that if there is a problem it can be localized and dealt with. 

For this reason, I’d add another desideratum for a foundation, though I realise some might disagree: correctness of proofs should be decidable (and ideally, efficiently so).

How about semi-decidable? That is, valid proofs are accepted, but invalid proofs might make the checker loop.

One can certainly argue for semi-decidability being enough, but I don’t find it quite satisfactory.  Or, at least, I find it considerably *less* satisfactory than decidability.

At an extreme, consider what would be wrong with taking f.o. predicate logic as our system, defining “provability” in the standard way, and then defining a “proof” of any provable formula to be simply the formula itself (and that there are no proofs of any unprovable formula).  This is semi-decidable!  The obvious objection: the semi-decision procedure is not proof-checking, but proof *search*.  But the same objection seems to apply, albeit less flagrantly, to other semi-decidable systems.  “Checking” connotes a decision procedure, not a potentially unbounded search.

Practically, as Vladimir says, one thing one wants for purported proofs is that “if there is a problem it can be localised and dealt with”.  And this certainly seems to fit better with decidability than semi-decidability.  If proof-checking is only semi-decidable, then you may not ever be able to know that a problem exists — just that you haven’t found a way to certify this proof *yet*.

I want my proof assistant — or the referees of my papers — to be able to either say “yes, it’s sound”, or “no, here’s a gap”.  It’s frustrating enough in practice when Coq or a referee seems to be taking forever.  It would be quite disheartening if even in principle, that were all we could expect!

Is Andromeda checking decidable or semi-decidable? I figured semi-decidable, unless it can somehow avoid loops in the equality-reflected reduction rules.

 

I’m a few months out of date, but yes, last that I heard, it was just semi-decidable.  However, iirc the semi-decision procedure did generate *witnesses*, whose correctness could then be (decidably) checked.  So I would prefer viewing these witnesses as the actual proofs, and the unwitnessed proof-terms as just partial proofs, albeit usually fairly close to complete.

–p.

[Andrej Bauer]

On Mon, Sep 15, 2014 at 10:38 AM, Matt Oliveri <atm...@gmail.com> wrote:
> The foundation is the bottom part of a building, which everything else rests upon.

I find this view to be wide spread and detrimental to foundations. It
reminds me of the great system-building philosophers (Hegel comes to
mind) in their search for the ultimate Theory of Everything. Anyhow,
there is much more to a foundation that it "being the bottom part of a
building". Firstly, because attempts to find "a secure foundation" may
(and do) turn out to be futile, and secondly because a good foundation
has much more to offer than a (false) sense of security.

If a foundation is only about the basement, is the rest of the
cathedral built without careful planning an design?

If we believe that foundations are only about providing a secure
support, then we will naturally tend to prefer simplicity over
expressivness, and reductionism over proper conceptual analysis. But
isn't it the job of a foundation to *also* be expressive so that we
*can* speak directly, rather than through layers of coding? Isn't it
its job to also provide useful *concepts* that help us do
mathematics?

Set theory brings in its own share of conceptual baggage, as does
HoTT, or any other foundation. But there is nothing wrong with that!
It is the job of a good foundation to shape the mathematicians'
thoughts through the language it provides and through the concepts it
imposes.

With kind regards,

Andrej

[Michael Shulman]

On Mon, Sep 15, 2014 at 4:47 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> In this sense neither the original MLTT nor its strengthened versions that
> are used in the Univalent Foundations are foundational systems.

Why not? We can and do use them to prove the relative consistency of
other theories. For instance, Peter Aczel proved the relative
consistency of CZF by constructing a model in MLTT (right?), and in
chapter 10 of the book we prove the relative consistency of ZF by
constructing a model in HoTT.

(By the way, while technically you're right that "homotopy type
theory" is not a formal system or a foundation, I don't see any
problem with declaring an implicit coercion so we can speak about it
as if it were one.)

Mike

[Vladimir Voevodsky]

On Sep 15, 2014, at 3:02 PM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:

For this reason, I’d add another desideratum for a foundation, though I realise some might disagree: correctness of proofs should be decidable (and ideally, efficiently so).

How about semi-decidable? That is, valid proofs are accepted, but invalid proofs might make the checker loop.

One can certainly argue for semi-decidability being enough, but I don’t find it quite satisfactory.  Or, at least, I find it considerably *less* satisfactory than decidability.

What seems to be a satisfactory answer is this: general poof checking in the system may be undecidable, however there are algorithms that, when they terminate with the positive outcome on a proof given to them as an argument, guarantee the correctness of this proof.

These procedures should be considered a part of the formal system and should be formally described and certified with the rest of the system (and independently on any implementation of the system in a proof assistant).

V.

[Michael Shulman]

On Mon, Sep 15, 2014 at 10:25 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
>> One can certainly argue for semi-decidability being enough, but I don’t find
>> it quite satisfactory. Or, at least, I find it considerably *less*
>> satisfactory than decidability.
>
> What seems to be a satisfactory answer is this: general poof checking in the
> system may be undecidable, however there are algorithms that, when they
> terminate with the positive outcome on a proof given to them as an argument,
> guarantee the correctness of this proof.

What Peter just said is that he *doesn't* find that to be
satisfactory. And I can see the point. It's certainly essential that
we should be able to check *some* proofs, but if there are also proofs
that we can't check, then that's less than completely satisfactory.

On the other hand, in practice the details of the algorithm also
matter. Just like a theoretically-exponential algorithm can do better
in practice than a theoretically-polynomial algorithm with an
astronomical constant term, a semidecidable system in which all
"naturally occurring" proofs can be checked might be as good in
practice as a decidable one.

[Martin Escardo]

I am watching this discussion with interest. Once some sort of
consensus emerges (which seems to be already beginning to happen), it
would be nice to see the outcome recorded somewhere.

Just one quick, tangential comment regarding (semi-)decidability of
proof-hood, and efficient decidability of proof-hood.

Let ack be the Ackermann function, and f a function I defined, for
which I proved

ack(17,17) = f(13).

Then also "refl" will be a proof, at least in a type theory in which
closed terms of natural number type are normalizing.

But this proof "refl" will never be checked by Coq or Agda, in
practice, as the numeral ack(17,17) is bigger than astronomical.

This is certainly not a "problem" of Coq or Agda, but a problem of the
proof "refl".

A referee wouldn't buy a proof of this equation in a submitted paper
that says "just compute both sides and see that they are equal". The
same goes e.g. for the particular examples of Mersenne Primes in the
literature, which involve a finite, but unfeasible, number of
computations if done by brute-force:

On 15/09/14 18:49, Michael Shulman wrote:
> On the other hand, in practice the details of the algorithm also
> matter. Just like a theoretically-exponential algorithm can do better
> in practice than a theoretically-polynomial algorithm with an
> astronomical constant term, a semidecidable system in which all
> "naturally occurring" proofs can be checked might be as good in
> practice as a decidable one.

And, conversely, a decidable system can be indistinguishable, in
practice, from a semi-decidable system, as illustrated above.

As a referee, I expect to be able to decide efficiently whether the
proofs in the submission under scrutiny really are proofs of the
claimed statements (an expectation which is not always fulfilled, but
this is another story).

However, the use of proof assistants, if it becomes wide-spread, will
inevitably create proofs that are feasible for the computer to check
but not for any human to check.

And this seems to be the case already with proofs in type theory
(before or after univalent foundations), where the use of "judgemental
equality" via "refl" creates huge proofs which look short when
rendered in Coq or Agda. Similarly, the use of implicit arguments
creates the illusion of shorts proofs. I guess this is one of the main
reasons people thinking in type theoretic terms are more tempted to
use proof assistants.

Martin

[Maxime Dénès]

Hello,

On 09/15/2014 03:39 PM, Martin Escardo wrote:
>
> I am watching this discussion with interest. Once some sort of
> consensus emerges (which seems to be already beginning to happen), it
> would be nice to see the outcome recorded somewhere.
>
> Just one quick, tangential comment regarding (semi-)decidability of
> proof-hood, and efficient decidability of proof-hood.
>
> Let ack be the Ackermann function, and f a function I defined, for
> which I proved
>
> ack(17,17) = f(13).
>
> Then also "refl" will be a proof, at least in a type theory in which
> closed terms of natural number type are normalizing.
>
> But this proof "refl" will never be checked by Coq or Agda, in
> practice, as the numeral ack(17,17) is bigger than astronomical.

I agree that decidability is probably overrated, since an algorithm that
doesn't terminate in a lifetime is often not more useful than one which
doesn't terminate at all.

However, it's not quite true that Coq or Agda will "never be" able to
check this proof. In practice, when Coq needs to check that two terms
are convertible, it doesn't expand them to normal form before comparing
them, but tries to be much smarter (reducing lazily and interleaving
comparison steps).

In particular, if you define f(n) to be ack(n+4,n+4) in your example, it
could well be that Coq's kernel is able to check that refl is a proof of
ack(17,17) = f(13) almost instantly (although I haven't tried).

Still, it doesn't go against your argument because this smartness of the
algorithm could also be used in favorable cases of a generally
undecidable problem.

Maxime.

[Maxime Dénès]

It turns out that Coq is indeed smart enough for this case:

Definition ack :=
fix aux1 (m : nat) :=
match m with
| O => S
| S p =>
fix aux2 (n : nat) :=
match n with
| O => aux1 p 1
| S p' => aux1 p (aux2 p')
end
end.

Definition f (n : nat) := ack (n + 4) (n + 4).

Time Check (eq_refl (ack 17 17) : ack 17 17 = f 13).
(* Finished transaction in 0. secs (0.003334u,0.s) *)

Although it is rather fragile: changing the proof term to eq_refl (f 13)
defeats the heuristics and takes forever.

Best,

Maxime.

[Martin Escardo]

(Now this is becoming very tangential.)

If you want to go that route, here is a possible definition of f:

f(x) = (ack(x + 4, x + 4) - 1) + 1,

and where truncated "- 1" is defined in the silly way that scans all
successors until it finds the zero (say with an accumulator as a
parameter in a helper function), and then after that produces the
corresponding number of successors with one ommitted, followed by
zero.

No amount of laziness will help here, but on the basis of this
information we can construct a short proof of my identity, and yet the
verification that "refl" is a proof (which it is) will take ack(17,17)
steps at least.

M.

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Matt Oliveri]

On Monday, September 15, 2014 10:02:40 AM UTC-4, Peter LeFanu Lumsdaine wrote:

On Mon, Sep 15, 2014 at 12:16 PM, Matt Oliveri <atm...@gmail.com> wrote:

On Monday, September 15, 2014 6:01:34 AM UTC-4, Peter LeFanu Lumsdaine wrote:

On Mon, Sep 15, 2014 at 11:14 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:

A foundation of maths is something like an accounting system that can be used to ensure that things are recorded properly

and that if there is a problem it can be localized and dealt with. 

For this reason, I’d add another desideratum for a foundation, though I realise some might disagree: correctness of proofs should be decidable (and ideally, efficiently so).

How about semi-decidable? That is, valid proofs are accepted, but invalid proofs might make the checker loop.

One can certainly argue for semi-decidability being enough, but I don’t find it quite satisfactory.  Or, at least, I find it considerably *less* satisfactory than decidability.

At an extreme, consider [...]

Practically, as Vladimir says, one thing one wants for purported proofs is that “if there is a problem it can be localised and dealt with”.  And this certainly seems to fit better with decidability than semi-decidability.  If proof-checking is only semi-decidable, then you may not ever be able to know that a problem exists — just that you haven’t found a way to certify this proof *yet*.

I want my proof assistant — or the referees of my papers — to be able to either say “yes, it’s sound”, or “no, here’s a gap”.  It’s frustrating enough in practice when Coq or a referee seems to be taking forever.  It would be quite disheartening if even in principle, that were all we could expect!

As Martin and Maxime have excellently pointed out, decidability is no guarantee of practicality, or anywhere close. I actually think incorporating notions of computation into proofs will make proof checking more practical. I would count Andromeda as doing this. So is proof by reflection. Essentially, the proof can give the checker advice about how to efficiently check it. One just needs a way to ensure the notion of proof is sound w.r.t. derivations.

And any semi-decidable notion of proof can be turned into a decidable notion of proof by annotating with an upper bound on the steps needed to check it. A "step" is something that's guaranteed to terminate. If a proof takes more steps than it said it would, it's invalid.

If you want efficient proof checking, you can similarly annotate with a step count where a "step" is (amortized) constant time. This means the worst case checking time is proportional to the max step count in the proof.

Of course, the way these counts are computed is by the author successfully checking the original proof. The counts would be included in the deliverable proofs as a courtesy to people who will re-check them. You can always decide a proof is too slow and complain to the author.

[Martin Escardo]

On 15/09/14 21:34, Matt Oliveri wrote:
> As Martin and Maxime have excellently pointed out, decidability is no
> guarantee of practicality, or anywhere close.

This is not what I wanted to point out.

What I wanted to point out is that arguments for whether proof-hood
should be decidable (or not), or at least semi-decidable (or not),
cannot and should not be purely based on practical grounds.

In practice, one would like "most naturally occurring proofs" to be
checked to be proofs fast, and any accidental (or not so accidental)
non-sense to be rejected, again fast.

Fine.

However, my personal view is that proof-hood should be decidable,
regardless of practical matters: this is the very point and nature of
proofs.

One should be able to mechanically recognize a proof, or reject it as
non-sense (however long this takes). Otherwise proof-hood becomes a
theorem, requiring its own proof.

But then the very question is what is a proof: is it a raw term, in an
untyped language, that happens to have a derivation (and hence is well
typed), or is it the derivation itself?

In the example I gave, the raw term was

refl {N} {ack(17,17)} : ack(17,17)=f(13).

I know that a derivation (in the empty context) exists, by indirect
(meta-theoretic) means, and hence that it is a well typed, genuine
closed term.

I agree this use of raw, untyped terms in a proof assistant (which
will be rejected if they cannot be assigned a type), is very
convenient (as a shorthand) in practice.

But I think that the primary stuff are the derivations. For
derivations, one doesn't ask whether they are (semi)decidable. They
are just inductively defined (in the meta-theory). To give a
derivation is to write a tree using constructors.

I see a proof assistant as (re)constructing a derivation I (rightly or
wrongly) had in mind, from a summary given by me as a raw term.

In this sense, I see no problem in having undecidability of the
existence of a derivation of a raw term: my duty was to give the full
derivation, but I was lazy and invoked a proof assistant to
(re)construct a derivation from partial information (the raw term).

If the proof assistant fails, or even loops, it is not (necessarily)
its fault. In that case, I should be less lazy and give the full
derivation, or at least more information to construct the (hoped for)
derivation.

Derivations can be recognized in linear time. However, we don't want
to write them down ourselves, as they can be long, and in fact
sometimes not linearly long on raw information (as in the given
example).

In this sense, I agree that decidability of well-typedness of raw
terms is over-rated. (And in any case it is already semi-decidable by
brute-force, by enumerating all possible derivations.)

Martin

[Matt Oliveri]

On Monday, September 15, 2014 7:47:17 AM UTC-4, v v wrote:

Or a foundation can be any sufficiently strong formal system used to formally justify other formal systems and thus everything they justify, at any level of indirection. This is what I mean.

I see now. This is a useful distinction. What you call a foundation I call "an etalon of consistency". For example ZFC is used as an etalon of consistency relative to which the consistency of the MLTT is shown. It is also used as the etalon of consistency for the type systems of HoTT through the use of univalent models.

OK good, we have a term for this. Actually, my notion two can be more than an etalon of consistency. It can also be an etalon of truth. For example, many intuitionistic systems are still consistent if you add excluded middle, but for someone who's really, philosophically a constructivist (not me), it's presumably not good to use an etalon with excluded middle. They would want to know that none of their ideas depend on it, since it's not true for them.

More generally, notion two is an etalon of meaning, in that provides the most primitive ideas that all the ideas you trust can be reduced to. These reductions may well be too complex to actually carry out routinely, but their existence still provides some assurance that people are understanding each other.

In this sense neither the original MLTT nor its strengthened versions that are used in the Univalent Foundations are foundational systems.

I think a simple formulation of MLTT might be a sensible etalon for constructivists. Some variant of CZF might be better. I'm not sure. I agree that Univalent Foundations is not an etalon.

For notion two, with no emphasis on convenience, all emphasis is on simplicity, and on efficiency of computer implementations. 

I am not sure why would you care about efficiency of an implementation. You are not going to actually use it for anything because the translation from the system that you actually use to an etalon of consistency may involve non-linear expansion in size.

Well, an implementation of an etalon should at least be efficient enough for it to be practical to maintain the interpretation of fancier systems you want to use. But basically you're right; the etalon wouldn't be used often, so it wouldn't need to be highly efficient.

I don't think any practical etalon would actually have a problem with non-linear expansion. Since it needs to have a practical formalization of the models, and interpretations are compositional, the models basically provide the systems that you actually use, but with a linear expansion plus some constant overhead.

[Matt Oliveri]

On Monday, September 15, 2014 5:34:12 PM UTC-4, Martín Escardó wrote:

On 15/09/14 21:34, Matt Oliveri wrote:
> As Martin and Maxime have excellently pointed out, decidability is no
> guarantee of practicality, or anywhere close.

This is not what I wanted to point out.

Oh, OK. But you did point it out in passing, right?

In practice, one would like "most naturally occurring proofs" to be
checked to be proofs fast, and any accidental (or not so accidental)
non-sense to be rejected, again fast.

Of course. I didn't argue against this. I just intended to elaborate on the point that practicality is rather independent of theoretical properties like decidability.

But I think that the primary stuff are the derivations.

Yes, definitely. Any notion of proof needs to be sound w.r.t. derivability, because the derivations are what the logic defines as the "official" notion of proof. And whether a derivation is valid should be decidable.

[Michael Shulman]

On Mon, Sep 15, 2014 at 3:06 PM, Matt Oliveri <atm...@gmail.com> wrote:
> I agree that Univalent Foundations is not an etalon.

As I said, why not?

[Matt Oliveri]

On Monday, September 15, 2014 1:08:30 PM UTC-4, Michael Shulman wrote:

On Mon, Sep 15, 2014 at 4:47 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> In this sense neither the original MLTT nor its strengthened versions that
> are used in the Univalent Foundations are foundational systems.

Why not?  We can and do use them to prove the relative consistency of
other theories.  For instance, Peter Aczel proved the relative
consistency of CZF by constructing a model in MLTT (right?), and in
chapter 10 of the book we prove the relative consistency of ZF by
constructing a model in HoTT.

It's a good thing to have different flavors of system justify each other. But for any given person, it seems like one flavor or the other provides concepts that seem intrinsically more trustworthy. That is how the etalon is chosen. Usually then, the etalon will be simple, so that it has fewer concepts to trust.

Notice that I've switched from speaking prescriptively to descriptively about what a foundation (etalon) is. I suppose there could be people who find the concepts behind HoTT to be intrinsically more trustworthy than set-level systems. I think they're weird. :) But for them, a HoTT system would be the best etalon yet.

[Michael Shulman]

On Mon, Sep 15, 2014 at 3:46 PM, Matt Oliveri <atm...@gmail.com> wrote:
> Notice that I've switched from speaking prescriptively to descriptively
> about what a foundation (etalon) is. I suppose there could be people who
> find the concepts behind HoTT to be intrinsically more trustworthy than
> set-level systems. I think they're weird. :) But for them, a HoTT system
> would be the best etalon yet.

Ok, so when you say that HoTT "is not" an etalon, you mean it is not a
good choice of etalon *for you*, because you find set-theoretic
concepts more believable than homotopy-theoretic ones. But in the
formal sense, it can certainly be an etalon of consistency, and for
those of us that you consider weird, it can be an etalon of
"believability" or "meaning" (I don't think it makes much sense to
talk about mathematical ideas being "true" in any absolute sense).

[Matt Oliveri]

On Monday, September 15, 2014 6:51:31 PM UTC-4, Michael Shulman wrote:

Ok, so when you say that HoTT "is not" an etalon, you mean it is not a
good choice of etalon *for you*, because you find set-theoretic
concepts more believable than homotopy-theoretic ones.

Yes. And I can say more. It seems to me that HoTT actually involves all the concepts of set theory and many more. So not only is HoTT not my choice of etalon, it seems like a rather unreasonable choice. If a HoTT system were able to eliminate all non-invariant things, like we discussed before, then it seems like you'd have a real trade off. Until then, it seems like taking HoTT as an etalon is giving something up for nothing.

But in the
formal sense, it can certainly be an etalon of consistency,

I don't think this idea of etalon can be formalized. Choosing an etalon is a social process. So I guess yes, vacuously?
 

and for those of us that you consider weird, it can be an etalon of
"believability" or "meaning"

Yup.

(I don't think it makes much sense to
talk about mathematical ideas being "true" in any absolute sense).

 
What I meant is that an etalon effectively defines a notion of truth, assuming it has anything that could be informally considered a proposition. The fact that not everyone agrees on the same etalon establishes that truth is not absolute in practice.

[Michael Shulman]

On Mon, Sep 15, 2014 at 4:10 PM, Matt Oliveri <atm...@gmail.com> wrote:
> Yes. And I can say more. It seems to me that HoTT actually involves all the
> concepts of set theory and many more.

No; it doesn't involve the slightly-bizarre concept of global
membership that ZF-style set theory is built on. It does involve most
or all of the concepts of "structural" set theory like ETCS, and both
of them seem to me preferable to ZF.

> I don't think this idea of etalon can be formalized. Choosing an etalon is a
> social process. So I guess yes, vacuously?

I thought Vladimir was saying that an "etalon of consistency" is just
something relative to which you can prove other theories consistent.
That's certainly true of HoTT.

If your only goal is to prove things consistent, or to have fewer
basic notions, then you may want to choose a simpler theory as your
etalon. But as Andrej has pointed out, there are many other
considerations that are at least as important as a simplicity (some
might say "paucity") of basic notions.

[Matt Oliveri]

On Monday, September 15, 2014 7:15:21 PM UTC-4, Michael Shulman wrote:

On Mon, Sep 15, 2014 at 4:10 PM, Matt Oliveri <atm...@gmail.com> wrote:
> Yes. And I can say more. It seems to me that HoTT actually involves all the
> concepts of set theory and many more.

No; it doesn't involve the slightly-bizarre concept of global
membership that ZF-style set theory is built on.  It does involve most
or all of the concepts of "structural" set theory like ETCS, and both
of them seem to me preferable to ZF.

Good point. Yes, I guess I was comparing HoTT and set-level type theory. I am still surprised that someone would find higher-dimensional math more intrinsically believable than material sets, but that does seem to be a real trade off.

> I don't think this idea of etalon can be formalized. Choosing an etalon is a
> social process. So I guess yes, vacuously?

I thought Vladimir was saying that an "etalon of consistency" is just
something relative to which you can prove other theories consistent.
That's certainly true of HoTT.

I hope not. Consistency proofs are relative. You can prove anything consistent in an inconsistent system. So a consistency proof is not informative to you if you don't already trust the system it's proved in.

If your only goal is to prove things consistent, or to have fewer
basic notions, then you may want to choose a simpler theory as your
etalon.  But as Andrej has pointed out, there are many other
considerations that are at least as important as a simplicity (some
might say "paucity") of basic notions.

I'm not sure what you're saying. The reason I think it's important to distinguish an etalon from any old strong formal system is to separate the "fundamental" ideas from other interesting ideas. Of course there will be disagreement about what the fundamental ideas are, but I don't think anyone thinks all ideas are fundamental. And I figure that some set of ideas would not be considered fundamental if a strict subset is fundamental. If that's true, then fundamental sets of ideas are minimal in a rather straightforward sense.

Maybe trying to pick out fundamental ideas is silly. I don't think so, but I don't want to argue about it.

[Michael Shulman]

On Mon, Sep 15, 2014 at 4:53 PM, Matt Oliveri <atm...@gmail.com> wrote:
> Maybe trying to pick out fundamental ideas is silly. I don't think so, but I
> don't want to argue about it.

Maybe not "silly" per se, but I don't see any reason that there would
be an observer-independent notion of "fundamentality".

> And I figure that some set of ideas would
> not be considered fundamental if a strict subset is fundamental.

This claim only makes sense if "fundamentality" is a property of sets
of ideas rather than individual ideas (otherwise the set of all
fundamental ideas would certainly contain strict subsets). But in
that case, I don't see any reason to believe it.

For instance (probably the case you had in mind), HoTT could be said
to contain as a "strict subset" structural set theory, and both can be
argued to be "fundamental sets of ideas". But SST's fundamentality is
not just a restriction of the fundamentality of HoTT, nor is HoTT's
fundamentality simply obtained by forgetting down to SST, so I don't
see any problem with regarding both as independently fundamental.

Mike

[Martin Escardo]

On 15/09/14 14:27, Thorsten Altenkirch wrote:
> On Sep 15, 2014, at 1:53 AM, Matt Oliveri <atm...@gmail.com

> <mailto:atm...@gmail.com>> wrote:
>
>> That's one of the things I want to understand. Why does the
>> ability to derive a lot of math make it a foundation? I can write
>> a lot of programs in Java (or Haskell, or OCaml...), but it's no
>> foundation of software.
>
> What is a foundation of software?
>
>
> Martin-Loef Type Theory.

Hmmm... Would anybody regard MLTT as a foundation of software (and in
any case, what would a foundation of software be, or what does that
even mean?)

However, is there any credible foundation of *constructive
mathematics* other than MLTT?

There certainly are a number of *formal systems* for constructive
mathematics, such as HA, HA^omega, and many more (see below).

Is there any theory of constructive mathematics, other than MLTT, in
which computation is built-in (at the meta-level), and doesn't have to
be extracted, and, more importantly, can be left unmentioned when
writing proofs?

This is very important for some people (including myself): because
computation is not mentioned when proofs in MLTT are written up, the
theory is compatible with e.g. excluded middle as a postulate (sure,
then the computational content is lost).

While there are constructive counter-parts of ZFC such as IZF and CZF,
their constructive content is not seen directly (in the case of CZF it
is seen by translation to MLTT).

So here is another etalon: MLTT is primary as a constructive
parameter, rather than as a consistency parameter.

In some sense, MLTT it is not just a foundation of constructive
mathematics: it is a foundation of neutral or absolute mathematics. It
just happens that (by careful design), in the context of type theory,
neutrality implies constructivity.

Now, regarding univalence, we have seen that both (1) it cannot be
formulated in ZFC, and (2) it not only can be formulated in MLTT, but
also it is a natural, very general extensionality axiom (which does
destroy the built-in computational properties of MLTT, and hence if
one wants to compute with univalence, as one can, this has to be added
(rather than inherited from MLTT)).

Thus, in this sense, HoTT is a very natural incarnation of univalent
foundations: one starts with a neutral foundation, and then one
specializes it, by just adding on very natural extentionality axiom
(which was all along waiting to be decided negatively or positively).

The computational content is lost. Of course! This is what happens
when one adds axioms to MLTT.

But then it is interesting that the idea of adding computational
content to the extended theory didn't come exclusively from the
constructivists: we have Voevodsky's conjecture (still open, but
approximated by the constructively given (and implemented) cubical
model.)

From this point of view, I find it very difficult to advocate ZFC as a
foundation (sure, it is a consistency etalon): it is difficult to find
a neutral core, with inherent computational content.

Martin

[Matt Oliveri]

On Monday, September 15, 2014 8:01:13 PM UTC-4, Michael Shulman wrote:

On Mon, Sep 15, 2014 at 4:53 PM, Matt Oliveri <atm...@gmail.com> wrote:
> And I figure that some set of ideas would
> not be considered fundamental if a strict subset is fundamental.

This claim only makes sense if "fundamentality" is a property of sets
of ideas rather than individual ideas (otherwise the set of all
fundamental ideas would certainly contain strict subsets).

Yeah sorry, I overloaded "fundamental" there.

But in that case, I don't see any reason to believe it.

Well yeah, I guess it was just a more specific rephrasing of my belief that an etalon should be conceptually simple.

For instance (probably the case you had in mind), HoTT could be said
to contain as a "strict subset" structural set theory, and both can be
argued to be "fundamental sets of ideas".  But SST's fundamentality is
not just a restriction of the fundamentality of HoTT, nor is HoTT's
fundamentality simply obtained by forgetting down to SST, so I don't
see any problem with regarding both as independently fundamental.

Is this purely hypothetical, or do you consider both to be good etalons? If you do, can you explain why?

[David Roberts]

Hi,

Matt wrote:
>Is this purely hypothetical, or do you consider both to be good etalons? If you do, can you explain why?

taking up the cause for ETCS, I will supply this quote from Tom
Leinster (taken from http://arxiv.org/abs/1212.6543):

"Perhaps you will wake up tomorrow, check your email, and find an
announcement that ZFC is inconsistent. Apparently, someone has taken
the ZFC axioms, performed a long string of logical deductions, and
arrived at a contradiction. The work has been checked and re-checked.
There is no longer any doubt.

How would you react? In particular, how would you feel about the
implications for your own work? All your theorems would still be true
under ZFC, but so too would their negations. Would you conclude that
your life’s work had been destroyed?

I believe that most of us would be interested but not deeply troubled.
We would go on believing that our theorems were true in a sense that
their negations were not. We are unlikely to feel threatened by the
inconsistency of axioms to which we never referred anyway.

In contrast, the ten axioms above are such core mathematical
principles that an inconsistency in them would be devastating. If we
cannot safely assume that composition of functions is associative, or
that repeatedly applying a function f:X→X to an element a∈X produces a
sequence (fn(a)), we are really in trouble."

The ten axioms are (one version of) ETCS and are:

Composition of functions is associative and has identities.
There is a set with exactly one element.
There is a set with no elements.
A function is determined by its effect on elements.
Given sets X and Y, one can form their cartesian product X×Y.
Given sets X and Y, one can form the set of functions from X to Y.
Given f:X→Y and y∈Y, one can form the inverse image f^{−1}(y).
The subsets of a set X correspond to the functions from X to {0,1}.
The natural numbers form a set.
Every surjection has a right inverse.

The standard argument that these are not sufficient to prove the
existence of the disjoint union of all the P^n(N), for n=1,2,3,...
which apparently some people find indispensable to their day-to-day
working on mathematics, can be countered by positing a collection
axiom schema (Leinster refers to McLarty's version in the above
paper).

Cheers,
David

> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Matt Oliveri]

On Monday, September 15, 2014 8:09:11 PM UTC-4, Martín Escardó wrote:

On 15/09/14 14:27, Thorsten Altenkirch wrote:
> >     What is a foundation of software?
>
> Martin-Loef Type Theory.

Is there any theory of constructive mathematics, other than MLTT, in
which computation is built-in (at the meta-level), and doesn't have to
be extracted, and, more importantly, can be left unmentioned when
writing proofs?

This is very important for some people (including myself): because
computation is not mentioned when proofs in MLTT are written up, the
theory is compatible with e.g. excluded middle as a postulate (sure,
then the computational content is lost).

While there are constructive counter-parts of ZFC such as IZF and CZF,
their constructive content is not seen directly (in the case of CZF it
is seen by translation to MLTT).

Maybe I don't know what you mean. Don't proofs in IZF or CZF have computational content too? Maybe your problem is that proofs are not objects? In that case, I think you need to use the same universe of dependent types for both mathematical types and propositions, and I guess that essentially means MLTT.

In some sense, MLTT it is not just a foundation of constructive
mathematics: it is a foundation of neutral or absolute mathematics. It
just happens that (by careful design), in the context of type theory,
neutrality implies constructivity.

Maybe I don't know what you mean by "neutral", but using the same universes for propositions and types seems pretty non-neutral.

From this point of view, I find it very difficult to advocate ZFC as a
foundation (sure, it is a consistency etalon): it is difficult to find
a neutral core, with inherent computational content.

This is a good point. I think an etalon would ideally be as neutral as possible. How about intensional MLTT, but with a separate predicative hierarchy for propositions? That might satisfy a lot of predicativists. I don't know what a good impredicative etalon would be. There seem to be a lot of weird ways to be impredicative. I personally like IZF's way of being impredicative, but I don't know how to make that structural off hand.

[Michael Shulman]

I no longer know what people in this thread mean by "etalon". I
thought Vladimir introduced the word to distinguish two different
meanings that are often attached to the word "foundation": (1) a
context in which to formalize informal mathematics (which he proposed
to call "foundation") and (2) a system with respect to which to
measure the consistency of other systems (which he proposed to call
"etalon"). But now it seems that many of us are using "etalon" for
meaning (1); or, at least, most of the criteria being applied seem to
me mainly applicable to that usage.

So as regards the question

> Is this purely hypothetical, or do you consider both to be good etalons? If
> you do, can you explain why?

If by "etalon" you mean a yardstick of consistency, then it's a fact
that they are equally well-suited to that as ZFC is, simply because a
version of each of them is equiconsistent with ZFC.

If you mean a foundation, whose role is to formalize informal
mathematics, provide a unified conceptual framework in which to
describe mathematics, basic tools for mathematicians to use in their
daily work, etc. then they are certainly both such a thing. Long
experience of mathematics shows that SST is equally good as ZFC at
doing these things, indeed it is closer to what mathematicians do and
use on a daily basis than ZFC is. And HoTT includes SST, so it is
equally adequate for those things, while also supplying more.

Mike

[Michael Shulman]

On Mon, Sep 15, 2014 at 7:39 PM, David Roberts <drobert...@gmail.com> wrote:
> The standard argument that these are not sufficient to prove the
> existence of the disjoint union of all the P^n(N), for n=1,2,3,...
> which apparently some people find indispensable to their day-to-day
> working on mathematics, can be countered by positing a collection
> axiom schema (Leinster refers to McLarty's version in the above
> paper).

... in which case the theory becomes equiconsistent with ZFC, and
hence would be equally impacted by a contradiction in the latter. (-:

[maxim....@googlemail.com]

>...to formalize informal mathematics

sound like paradox.

>...daily work...,...daily basis...,...Long experience of..., 

sounds like phrases from a statistics.

Why foundations must be a formal system(axiomatic system)?

Why foundations not a statistics, for example? 

[Matt Oliveri]

On Tuesday, September 16, 2014 12:20:03 AM UTC-4, Michael Shulman wrote:

I no longer know what people in this thread mean by "etalon".  I
thought Vladimir introduced the word to distinguish two different
meanings that are often attached to the word "foundation": (1) a
context in which to formalize informal mathematics (which he proposed
to call "foundation") and (2) a system with respect to which to
measure the consistency of other systems (which he proposed to call
"etalon").  But now it seems that many of us are using "etalon" for
meaning (1); or, at least, most of the criteria being applied seem to
me mainly applicable to that usage.

I didn't think anyone was using etalon for (1). I brought up the idea of an "etalon of meaning" which is a formal system of basic concepts that are used to establish the meaning of other concepts, not just their consistency. This is what I've meant by "etalon".

So as regards the question

> Is this purely hypothetical, or do you consider both to be good etalons? If
> you do, can you explain why?

If by "etalon" you mean a yardstick of consistency, then it's a fact
that they are equally well-suited to that as ZFC is, simply because a
version of each of them is equiconsistent with ZFC.

Suppose I told you I came up with a new formal system S, and that it can prove the consistency of ETCS. Would you care? Probably not. You already believed ETCS was consistent, and you know nothing about S. S might not even be consistent. Then someone proves in ETCS that S is consistent. I'm guessing at this point you conclude that S is consistent after all. You haven't really learned anything about ETCS. ETCS and S are now equiconsistent, but you have a more basic trust in ETCS than S. You trust S (at least as far as consistency goes) because ETCS says it's OK. S is not your etalon. Maybe it's mine, but maybe not; I could have other reasons for using S.

Hopefully I haven't forged your reactions in this hypothetical scenario too badly. If you still don't see what I mean at this point, I don't know what to say. I already said that choice of etalon is not a formal thing.

If you mean a foundation, whose role is to formalize informal
mathematics, provide a unified conceptual framework in which to
describe mathematics, basic tools for mathematicians to use in their
daily work, etc. then they are certainly both such a thing.

No, that was the other notion of foundation. (The one I still don't see why it's called "foundation".) That's never what I meant.

Long
experience of mathematics shows that SST is equally good as ZFC at
doing these things, indeed it is closer to what mathematicians do and
use on a daily basis than ZFC is.  

 

And HoTT includes SST, so it is
equally adequate for those things, while also supplying more.

HoTT is an excellent tool for formalizing math. That was never in question. By "foundation", I have meant "etalon of meaning" since the beginning of the thread.

[Matt Oliveri]

I was actually thinking that, but I figured I'd better stay quiet, since I don't really know ETCS. :D

The quote from Leinster seemed to imply that if ZFC was inconsistent, math would be OK becuase ZFC isn't much like math. But the real reason math would be OK, if any, is because it doesn't really need all the logical strength of ZFC.

[Michael Shulman]

On Mon, Sep 15, 2014 at 10:14 PM, Matt Oliveri <atm...@gmail.com> wrote:
> I brought up the idea of an
> "etalon of meaning" which is a formal system of basic concepts that are used
> to establish the meaning of other concepts, not just their consistency.

I would consider that part of the role of a foundation (1). For instance, here:

>> If you mean a foundation, whose role is to formalize informal
>> mathematics, provide a unified conceptual framework in which to
>> describe mathematics, basic tools for mathematicians to use in their
>> daily work, etc. then they are certainly both such a thing.

By "a unified conceptual framework in which to describe mathematics" I
think I meant more or less the same thing as "a system of basic
concepts used to establish the meaning of other concepts".

Are you saying you don't understand how ETCS or HoTT can be regarded
as such a system of basic concepts?

Mike

[Andrej Bauer]

On Tue, Sep 16, 2014 at 2:09 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> However, is there any credible foundation of *constructive
> mathematics* other than MLTT?

Sheaves.

If you insist that the only valid explanation of constructivism is a
computational one, and in addition you refuse to use any technology
beyond operational semantics, then proably the only choice you have is
MLTT (or realizability).

But constructive mathematics can be explained independently in terms
of the geometric notion of locality, or more generally a sheaf. (It
would be a mistake to think that a pre-mathematical explanation of
local phenomena must use set theory.)

With kind regards,

Andrej

[Matt Oliveri]

On Tuesday, September 16, 2014 2:02:29 AM UTC-4, Michael Shulman wrote:

On Mon, Sep 15, 2014 at 10:14 PM, Matt Oliveri <atm...@gmail.com> wrote:
> I brought up the idea of an
> "etalon of meaning" which is a formal system of basic concepts that are used
> to establish the meaning of other concepts, not just their consistency.

I would consider that part of the role of a foundation (1).  For instance, here:

>> If you mean a foundation, whose role is to formalize informal
>> mathematics, provide a unified conceptual framework in which to
>> describe mathematics, basic tools for mathematicians to use in their
>> daily work, etc. then they are certainly both such a thing.

By "a unified conceptual framework in which to describe mathematics" I
think I meant more or less the same thing as "a system of basic
concepts used to establish the meaning of other concepts".

That one-phrase definition of "etalon of meaning" was only meant to distinguish it from "etalon of consistency". I was hoping the example of ETCS and S would clarify what I see as the distinguished (from other meaningful systems) status of an etalon. Are you saying you don't agree that some systems should be distinguished as etalons?

Are you saying you don't understand how ETCS or HoTT can be regarded
as such a system of basic concepts?

Back up. I asked "do you consider both to be good etalons?". Specifically, I don't understand why someone would have two etalons. It seems like one or the other would be considered more intuitive.

[David Roberts]

On 16 September 2014 13:50, Michael Shulman <shu...@sandiego.edu> wrote:
> ... in which case the theory becomes equiconsistent with ZFC, and
> hence would be equally impacted by a contradiction in the latter. (-:

That's good, and I was being needlessly superfluous. It does mean that
people who regard \coprod_n P^n(N) as mathematically essential may be
in trouble, or they'll have to find a weaker axiom to build it for
them...

[Michael Shulman]

On Tue, Sep 16, 2014 at 12:35 AM, Matt Oliveri <atm...@gmail.com> wrote:
> I was hoping the example of
> ETCS and S would clarify what I see as the distinguished (from other
> meaningful systems) status of an etalon. Are you saying you don't agree that
> some systems should be distinguished as etalons?

If you're just saying that we should choose a foundational system
whose basic concepts come with a good intuition, then sure, I agree.

> Back up. I asked "do you consider both to be good etalons?". Specifically, I
> don't understand why someone would have two etalons. It seems like one or
> the other would be considered more intuitive.

No, I don't see any reason why "intuitiveness" should be a linear ordering.

It's important that in mathematics, "intuitiveness" is not something
you have to take a priori. We can and generally do learn new
intuitions for new concepts.

[Matt Oliveri]

On Tuesday, September 16, 2014 3:43:47 AM UTC-4, Michael Shulman wrote:

On Tue, Sep 16, 2014 at 12:35 AM, Matt Oliveri <atm...@gmail.com> wrote:
> Back up. I asked "do you consider both to be good etalons?". Specifically, I
> don't understand why someone would have two etalons. It seems like one or
> the other would be considered more intuitive.

No, I don't see any reason why "intuitiveness" should be a linear ordering.

Whoa, deep! :) So one's multiple etalons could be the multiple maximally intuitive systems? Seems like you'd want to find a common upper bound.

It's important that in mathematics, "intuitiveness" is not something
you have to take a priori.  We can and generally do learn new
intuitions for new concepts.

This is certainly true. But the intuition for some ideas seems to come earlier than for others. For students, it would be nice if the foundation to learn was not such a big hurdle for the intuition.

[Michael Shulman]

I don't see any reason why "intuitiveness" should be a lattice either. (-:

[Peter LeFanu Lumsdaine]

On Tue, Sep 16, 2014 at 10:06 AM, Michael Shulman <shu...@sandiego.edu> wrote:

I don't see any reason why "intuitiveness" should be a lattice either.  (-:

I don’t even see it as an *ordering* — I’d see it as something more like (at least) a category :-)  There can be different ways to translate from one system of concepts to another.

[Concrete example: you can translate the syntax of intuitionistic f.o. logic into classical by the identity translation, and translate back by Gödel’s double negation.  Under the first, classical logic looks “equally expressive in language, but stronger in proof”.  Under the second, intuitionistic logic looks “equally strong in proof (the translation is conservative), but more expressive in language”.  Why aren’t these views incompatible?  Because they compose to a non-identity self-translation of intuitionistic logic.]

This a sort of pluralism of foundations.  It’s important conceptually and practically to have *at least one system* which is solid enough to use as a foundation, whatever that may mean.  (And which is socially agreed on as sufficiently solid.)  But there’s no reason this one has to be unique, canonical, minimal, initial, …  One can believe there is a true, real, Platonic world of mathematics, without believing that there’s just one right way of talking or reasoning about it.

–p. 

[Vladimir Voevodsky]

More generally, notion two is an etalon of meaning, in that provides the most primitive ideas that all the ideas you trust can be reduced to. 

Not necessarily.   For example, in HoTTs (I am using the plural to distinguish HoTTs that are various type-theories from HoTT that is the mathematical study of these type theories) types can not be built from sets unless one adds a strong form of the axiom of choice.

The univalent models indeed provide us with intuition about the objects that HoTTs directly address but with a limited intuition not with a possibility of formally reducing everything. 

Vladimir.

On Sep 15, 2014, at 11:06 PM, Matt Oliveri <atm...@gmail.com> wrote:

On Monday, September 15, 2014 7:47:17 AM UTC-4, v v wrote:

Or a foundation can be any sufficiently strong formal system used to formally justify other formal systems and thus everything they justify, at any level of indirection. This is what I mean.

I see now. This is a useful distinction. What you call a foundation I call "an etalon of consistency". For example ZFC is used as an etalon of consistency relative to which the consistency of the MLTT is shown. It is also used as the etalon of consistency for the type systems of HoTT through the use of univalent models.

OK good, we have a term for this. Actually, my notion two can be more than an etalon of consistency. It can also be an etalon of truth. For example, many intuitionistic systems are still consistent if you add excluded middle, but for someone who's really, philosophically a constructivist (not me), it's presumably not good to use an etalon with excluded middle. They would want to know that none of their ideas depend on it, since it's not true for them.

More generally, notion two is an etalon of meaning, in that provides the most primitive ideas that all the ideas you trust can be reduced to. These reductions may well be too complex to actually carry out routinely, but their existence still provides some assurance that people are understanding each other.

In this sense neither the original MLTT nor its strengthened versions that are used in the Univalent Foundations are foundational systems.

I think a simple formulation of MLTT might be a sensible etalon for constructivists. Some variant of CZF might be better. I'm not sure. I agree that Univalent Foundations is not an etalon.

For notion two, with no emphasis on convenience, all emphasis is on simplicity, and on efficiency of computer implementations. 

I am not sure why would you care about efficiency of an implementation. You are not going to actually use it for anything because the translation from the system that you actually use to an etalon of consistency may involve non-linear expansion in size.

Well, an implementation of an etalon should at least be efficient enough for it to be practical to maintain the interpretation of fancier systems you want to use. But basically you're right; the etalon wouldn't be used often, so it wouldn't need to be highly efficient.

I don't think any practical etalon would actually have a problem with non-linear expansion. Since it needs to have a practical formalization of the models, and interpretations are compositional, the models basically provide the systems that you actually use, but with a linear expansion plus some constant overhead.

[Vladimir Voevodsky]

"etalon of consistency" is a formal deduction system that is strongly believed to be consistent.

Univalent Foundations is an approach to a foundation of mathematics - not a formal deduction system.

None of the HoTTs can be an etalon of consistency so far first of all because they do not have sufficiently stable
formulations (and consistency can depend on small details).

V.

[Vladimir Voevodsky]

On Sep 15, 2014, at 11:51 PM, Michael Shulman <shu...@sandiego.edu> wrote:

 (I don't think it makes much sense to
talk about mathematical ideas being "true" in any absolute sense).

Mike, you work on models too much! There are true mathematical ideas. 

For example pi_4 of S^2 is Z/2 . It is true.

Vladimir.

[Vladimir Voevodsky]

I guess any formal theory that is precisely defined can be an etalon. But in practice it is convenient to certify HoTTs against ZFC, not the other way around.
Vladimir.

[Vladimir Voevodsky]

As I have elaborated on previously (https://github.com/vladimirias/2010_80ies_aniversary_lecture) it is entirely possible that Peano arithmetic is inconsistent (in fact I made a formal conjecture that it is inconsistent).

Vladimir.

[Vladimir Voevodsky]

> 2) a system with respect to which to
> measure the consistency of other systems (which he proposed to call
> "etalon").

Right. It is how I defined "etalon of consistency".

V.

[Michael Shulman]

On Tue, Sep 16, 2014 at 4:35 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> None of the HoTTs can be an etalon of consistency so far first of all because they do not have sufficiently stable
> formulations (and consistency can depend on small details).

Are you saying that your notion of "etalon" is not just mathematical
but also social? That an etalon of consistency has to be sufficiently
stable and widely known throughout mathematics for it to be "generally
accepted" as a criterion of consistency? I didn't understand that at
first.

Mike

[Michael Shulman]

On Tue, Sep 16, 2014 at 4:45 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> Mike, you work on models too much! There are true mathematical ideas.
>
> For example pi_4 of S^2 is Z/2 . It is true.

What do you mean by "true"?

[maxim....@googlemail.com]

On Tuesday, September 16, 2014 6:42:07 PM UTC+6, v v wrote:

As I have elaborated on previously (https://github.com/vladimirias/2010_80ies_aniversary_lecture) it is entirely possible that Peano arithmetic is inconsistent (in fact I made a formal conjecture that it is inconsistent).

Vladimir.

In my opinion problem with formal systems is even deeper.

Main question about metatheory for the Godel Incompleteness theorems(as well as any metatheorems).

This metatheories exploits the diagonal arguments that is impedicativity with problematic resolution even in first order setting(needs infinite object). 

But moreover, the godelization is a higher order function.

Namely, the proposition/sentence is the definition for class of his own proofs/disproofs, or both in inconsistent case. Moreover it is higher order structure : proofs, proved equivalency of proofs and so on...; "proofs between proofs" of all arbitrary degrees. Something like classes of classes of classes... or "Higher groupoid of proofs".

And this higher order objects subjected to diagonal arguments!

Consistency of Godel metatheory is a big question.

Whether there are  proofs of "antiGodelIncompletenssTheorems"?

Summary: a metatheory is a theory with his own consistency problem(undecidable in formal system concept). I.e. formal system concept needs in external foundations. 

Liar paradox on all metalevels.

P.S. even such depressive results as the Godel Incompleteness theorems not consistently provable. But this is not adds optimism about formal systems perspectives, rather the opposite.

Max 

>> email to HomotopyTypeTheory+unsub...@googlegroups.com.

[Steve Awodey]

On Sep 16, 2014, at 10:47 AM, maxim....@googlemail.com wrote:

On Tuesday, September 16, 2014 6:42:07 PM UTC+6, v v wrote:

As I have elaborated on previously (https://github.com/vladimirias/2010_80ies_aniversary_lecture) it is entirely possible that Peano arithmetic is inconsistent (in fact I made a formal conjecture that it is inconsistent).

Vladimir.

In my opinion problem with formal systems is even deeper.

Main question about metatheory for the Godel Incompleteness theorems(as well as any metatheorems).

This metatheories exploits the diagonal arguments that is impedicativity with problematic resolution even in first order setting(needs infinite object). 

But moreover, the godelization is a higher order function.

Namely, the proposition/sentence is the definition for class of his own proofs/disproofs, or both in inconsistent case. Moreover it is higher order structure : proofs, proved equivalency of proofs and so on...; "proofs between proofs" of all arbitrary degrees. Something like classes of classes of classes... or "Higher groupoid of proofs".

And this higher order objects subjected to diagonal arguments!

Consistency of Godel metatheory is a big question.

Whether there are  proofs of "antiGodelIncompletenssTheorems"?

Summary: a metatheory is a theory with his own consistency problem(undecidable in formal system concept). I.e. formal system concept needs in external foundations. 

Liar paradox on all metalevels.

enough!

this discussion has really gone off the rails.

can someone please try to focus what on earth is being discussed in this thread?

is there some specific question left, or is it just foundational sturm und drang at this point?

Thanks,

Steve

[Dimitris Tsementzis]

I agree, so let me make an attempt, as an outsider, to re-focus the thread and possibly conclude it? The two most important questions that are being addressed in this thread seem to me to be:

(1) Is it necessary that Univalent Foundations must be formalized as a (homotopy) type theory (e.g. HTS or HoTT) of some sort? 

  

ANSWER: The answer that seems to me to be emerging from this thread is NO (even though no alternative formalization currently exists). In particular it is not right to think of Univalent Foundations as being defined by the "equation" UF=(intensional MLTT+Univalence Axiom). One reason for this seems to be that the "universe of infinity-groupoids" has intuitive content of its own, not reducible to a single definitive description by a single formal system. This situation seems to be analogous to how the Cantorian hierarchy of sets has an intuitive content of its own not reducible to a single definitive formalization, e.g. ZFC. I think this is very interesting. It would be good to see if everyone agrees to this and if not, why. Furthermore, it would perhaps be good if (1) can be phrased using terminology that everyone can agree to.

(2) Is the *particular* formalization of Univalent Foundations as (intensional MLTT + Univalence) to be thought of as providing an "etalon of consistency"?

ANSWER:  The answer that seems to be emerging in this thread is NO, but maybe EVENTUALLY. The reason for the "EVENTUALLY" is that this is not a purely mathematical or even philosophical question, but partly a historical/sociological one. In particular, the fact that ZFC is seen as an "etalon of consistency" now is that it has withstood the test of time very well: no-one has been able to prove an inconsistency in it or in any of its countless variations in all these decades. Furthermore, there exist a whole cluster of methods built around ZFC (and its countless variations) with which to answer metamathematical questions in a regimented and precise manner, e.g. to prove equiconsistency of MLTT with other systems or to construct a model of univalence using simplicial sets. In time (intensional MLTT+Univalence) may turn out to be as well-developed a metamathematical tool as ZFC is currently. I don's see anything that would prevent this from happening, but that doesn't seem to me something that can be answered right now or even definitively. The proof of it will be in the ever-expanding pudding.

In short, it seems to me that "etalon of consistency" is a property of a particular formalization (e.g. ZFC) rather than of a particular foundational approach (e.g. Set Theory or Univalent Foundations.) But Univalent Foundations does not just refer to a particular formalization. It refers to the idea of using the hierarchy of  homotopy n-types as the "basic" structures of mathematics. And this (incredible) idea could be formalized in any number of ways, one of which might turn out to be as stable and useful as ZFC in which case we will be able to call it an "etalon of consistency". Indeed (intensional MLTT + Univalence) might turn out to be just that formalization, but we just don't know yet.

Best,

Dimitris

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.

[Michael Shulman]

Thanks Steve.

I am also interested in Vladimir's proposal that "Univalent
Foundations" refers to an idea rather than a particular formalization
of that idea. I assume that under this reading, since it doesn't
refer to any particular formal system, it also doesn't make any claims
about added axioms like LEM or AC, i.e. constructive mathematics can
also be included under the umbrella of Univalent Foundations?

[Dimitris Tsementzis]

I think the analogy is supposed to be as follows:

Set Theory : ZF(C)
Univalent Foundations : Intensional MLTT+Univalence

In this analogy the term "Univalent Foundations" should perhaps more aptly be called "Shape Theory" (or perhaps "Abstract Shape Theory" to emphasize invariance.) "Shape Theory" would then refer to the pre-formal, intuitive understanding of homotopy types (i.e. "shapes") in the same sense that "Set Theory" refers to the pre-formal, intuitive understanding of collections. So with this in mind if I now repurpose the term "Univalent Foundations" to stand as a shorthand for the particular formalization of "Shape Theory" given by "Intensional MLTT + Univalence" the above analogies become

Set Theory : ZFC
Shape Theory : Univalent Foundations

In my opinion this is the correct way to use these terms. I wouldn't actively advocate for using the term "Shape Theory" because it sounds too mysterious and offbeat, but it seems useful to keep in mind especially in the context of such debates where people seem to be unclear about whether they are referring to a particular formalization or the idea that formalization is trying to capture.

And to answer your question form this point of view: in the same sense that you can say that ZF, ZFC, IZF, CZF are all formalizations of "Set Theory" that emphasize different philosophical attitudes towards what is or is not an acceptable form of mathematical reasoning, you could say that Univalent Foundations (in the repurposed sense) with or without LEM or AC etc. are all different formalizations of Shape Theory that emphasize different philosophical attitudes towards what is or is not an acceptable form of reasoning. In that sense constructive mathematics is definitely included under the umbrella of "Shape Theory" (i.e. "Univalent Foundations" in your sense.)

Dimitris

[Michael Shulman]

"Shape Theory" is doubly unfortunate because it already has a
different meaning: http://ncatlab.org/nlab/show/shape+theory. A more
appropriate name analogous to "Set Theory" would be ... um ...
"Homotopy Type Theory"? (-:O

On Tue, Sep 16, 2014 at 7:44 AM, Dimitris Tsementzis

[Vladimir Voevodsky]

Yes, I have been introducing Univalent Foundations lately as an approach to a foundation
of constructive mathematics and explaining that classical mathematics is a retract,
and in particular a subset, of constructive mathematics.

V.

[Steve Awodey]

perhaps an example of UF *not* formalized in HoTT would be doing things in infy-topos theory.

Steve

[Vladimir Voevodsky]

It should be a little different:

Set-theoretic foundations : Set theory : ZF(C)
Univalent Foundations : ??? (Shape Theory) : MLTT + univalence or CIC + univalence or cubical type theory or ...

Vladimir.

PS The name "Shape theory" is taken by an obscure branch of topology (cf. google) so it should be something different. In my Bernays lectures I tried to show
that "shape theory" is a natural development that started at least with Grassmann who called it "the general theory of forms". See
https://github.com/vladimirias/2014_Paul_Bernays_Lectures
especially Lecture 1 p. 16 and then Lecture 2 p. 11 .

[Vladimir Voevodsky]

It could also be simply "homotopy theory" because this is what it currently really is.

V.

[Matt Oliveri]

On Tuesday, September 16, 2014 3:52:58 PM UTC-4, Michael Shulman wrote:

A more appropriate name analogous to "Set Theory" would be ... um ...
"Homotopy Type Theory"? (-:O

Come to think of it, that pun could've been causing confusion in this discussion. Which "HoTT"s were "(HoT)T", and which were "Ho(TT)"?

[Dimitris Tsementzis]

"Homotopy Theory" and "Homotopy Type Theory" are perfectly comprehensible terms for "non-formalized Univalent Foundations" as far as I am concerned, but I think each comes loaded with preconceptions which might confuse newcomers.

"Homotopy Theory" makes it seem as though intensional MLTT+Univalence is supposed to be a foundation only for homotopy theory understood as a branch of algebraic topology.

"Homotopy Type Theory" runs the danger of being read as "Homotopy (Type Theory)" which makes it seems as though Univalent Foundations is just an umbrella term designating certain systems of type theory.

The issue is to somehow use a term that makes it clear that "Homotopy Type Theory" is to be read as "(Homotopy Type) Theory" when it refers to what I called "Shape Theory", i.e. to "non-formalized Univalent Foundations". I think having such a term or at least even parenthesising as such will be helpful in resolving debates such as the one that began this thread in a more efficient manner.

For what it's worth my personal favourite is "Abstract Shape Theory" because as I said it also emphasizes the invariance that the univalence axiom in MLTT formalizes. But for many reasons, including the fact that "Shape Theory" already has a different meaning as pointed out by Mike, I agree that it's perhaps not worth establishing. Finally, the fact that the name of this very list is HoTT is probably an indication that "Homotopy Type Theory" is still perhaps the best term to use both for "Shape Theory" and "Intensional MLTT + ..." taking care to emphasize which particular parenthesization one has in mind whenever the need arises. It seems to me much of this thread occurred because people were talking about different parenthesizations.

Dimitris

[Michael Shulman]

One reason I like the pun is because I don't want to cut up the
subject into one part that's (HoT)T and one part that's Ho(TT).
People and ideas flow back and forth; I don't really see a value in
trying to pin down exactly which is which.

[Matt Oliveri]

Normally I would agree, but it seems like (HoT)T is an area of math, while Ho(TT) is a class of formal systems, or the study of this class. So in a discussion about "foundations", they play different roles.

[Matt Oliveri]

On Tuesday, September 16, 2014 7:26:53 AM UTC-4, v v wrote:

More generally, notion two is an etalon of meaning, in that provides the most primitive ideas that all the ideas you trust can be reduced to.

Not necessarily.   For example, in HoTTs (I am using the plural to distinguish HoTTs that are various type-theories from HoTT that is the mathematical study of these type theories) types can not be built from sets unless one adds a strong form of the axiom of choice.

I don't see how that's an argument against what I said. If you feel that types can be built from sets, but they can't be in some system, then that system is not a good etalon of meaning for you.

The univalent models indeed provide us with intuition about the objects that HoTTs directly address but with a limited intuition not with a possibility of formally reducing everything.

You're right. I should say "etalon of meaning, in that it provides the most primitive formalized ideas that all the formalizable ideas you trust can be reduced to." I see this clarification as kind of obvious; you can't formalize something you can't formalize.

Regarding HoTTs specifically, I thought it was considered a feature that they don't tell you everything about (a particular model of) types.

[Andrej Bauer]

I am joining Steve's plea: this discussion thread is completely
derailed. Can we have it stop?

With kind regards,

Andrej

[David Roberts]

Maybe the discussion could continue of the fom mailing list. They love this kind of stuff... Especially Harvey ;-)

David

—
Sent from Mailbox