2
$\begingroup$

I'm interested in HoTT, especially its application to foundations of mathematics.

I believe strongly that Univalent Foundations is the very foundation of mathematics.

So,I have a question.

(Q) Univalent Foundations(or such variant systems of HoTT that provide a foundation of mathematics) and canonicity property are compatible?

Of course, the answer to the question depends on the definition of such systems.

Indeed the system in Appendix A.1 in the HoTT book has canonicity property,

while the system in Appendix A.3 doesn't.

But regardless of the definition of such systems, in order to provide a foundation of mathematics, they should have at least the following property.

For any computable function, there exist a term express that function in the system.

The above requirement may be irrelvant,but I want to require it here.

Then,in the above context,I want to ask (Q).

My own answer to the question is the following.

As far as I understand, any type system that has canonicity isn't Turing complete.

So,there is a computable function that can't be expressed in such system.

Therefore, by the above definition of such systems,

any formalization of HoTT as a foundation of mathematics(in the above sense) can't be compatible with canonicity.

Is it right?

$\endgroup$
7
  • $\begingroup$ I'm not sure I understand your question, but I have the impression that the problem is what do you call "computable" ? every primitive recursive function can be expressed as term $[ \mathbb{N},\mathbb{N}]$ every partial recursive functions can be expressed as a function from $D$ to $\mathbb{N}$ where $D$ is the domain of definition of the function (a recursive subset of $\mathbb{N}$) or as a function from $\mathbb{N}$ to the set of sub-singleton of $\mathbb{N}$. What you call a "computable function" is a recursive function that just "happen" to be total... $\endgroup$ Nov 22, 2016 at 8:30
  • $\begingroup$ ... But saying that such a function can be represented by a term in some type theory mean that this type theory can prove that the function is total ! So you would have the same problem with any recursively axiomatisable theory: type theory but also ZFC or ZFC plus any axiom scheme you like... $\endgroup$ Nov 22, 2016 at 8:35
  • $\begingroup$ Thank you for your comments! But I don't know something yet. >saying that such a function can be represented by a term in some type theory mean that this type theory can prove that the function is total ! Yes, so partial recursive functions can't be represented in general. But, how such systems have the strenghness of consistency equal to ZFC? $\endgroup$
    – iwu
    Nov 23, 2016 at 5:23
  • $\begingroup$ >So you would have the same problem with any recursively axiomatisable theory: type theory but also ZFC or ZFC plus any axiom scheme you like I don't think so, because ZFC can define uncomputable function(like the busy beaver function) and the propositions about it. Of course,such propositions is undecidable in general ,or uncomputable functions are computable! then, ZFC is undecidable. $\endgroup$
    – iwu
    Nov 23, 2016 at 5:23
  • $\begingroup$ What I'm saying is that even working in ZFC, the "computable functions" that you can define as functions from $\mathbb{N}$ to $\mathbb{N}$ are only the partial recursive functions which are provably total in ZFC. There exists computable function, i.e. "partial recursive functions which happen to be total" that are not provably total in ZFC and hence that cannot be interpreted as total function from $\mathbb{N}$ to $\mathbb{N}$ in ZFC. And this has nothing to do with ZFC, it will basially apply to any recursively axiomatisable theory that is strong enough to formalise arithmetics. $\endgroup$ Nov 23, 2016 at 11:21

1 Answer 1

2
$\begingroup$

This paper gives a proof of Canonicity for Cubical Type Theory

$\endgroup$
3
  • $\begingroup$ Thank you for your answer! That paper is very interesting! But I don't understand it yet. In that paper Canonicity is proven , but how such systems have the strenghness of consistency equal to ZFC? For example,how about the system with the cumulative hierarchy V as HITs(in the HoTT book)? I guess such strong system can't have canonicity... $\endgroup$
    – iwu
    Nov 23, 2016 at 5:50
  • $\begingroup$ Huber's paper shows canonicity for a system with some higher inductive types. V is not expected to give a problem, because it is a quotiented W-type ("Aczel's tree construction"). However, we don't have a formal proof of that yet, I believe. $\endgroup$ Nov 24, 2016 at 12:54
  • $\begingroup$ Thank you for your comment! I could understand what I have mistaken. So, now I expect HoTT(formulated so that it's sufficient to provide a foundation) will be proved to have canonicity in the future!(Of course,by Godel's result,such proof is impossible internally) $\endgroup$
    – iwu
    Nov 26, 2016 at 11:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.