2
$\begingroup$

Among the various models of homotopy type theory (simplicial sets, cubical sets, etc.), is there a computable one? Can the negative follow from the Gödel-Rosser incompleteness theorem?

If there is no such model, wouldn't this be an argument in favour of second-order arithmetic (or similar theories) as the foundation of mathematics from a computational point of view?

Improve this question
$\endgroup$
3
  • 3
    $\begingroup$ If there were a computable model, wouldn't that rather be an argument against it as a foundation? After all, we don't have computable models of second-order arithmetic even in the weak cases, and there can be no computable model of ZFC, etc. $\endgroup$
    – Joel David Hamkins
    Commented Jun 17 at 10:09
  • $\begingroup$ There is no computable model of $\text{RCA}_0$, for example, since if there were, we could diagonalize against the classes to produce a computable class that wasn't present. Just Cantor, no need for Gödel. $\endgroup$
    – Joel David Hamkins
    Commented Jun 17 at 10:14
  • 6
    $\begingroup$ Could you explain what you mean by a "computable model" of a type theory? The cubical set model certainly seems computable to me; at least it is fully constructive and can be implemented in a computer. Do you mean a realisability model, like Uemura's cubical assemblies? $\endgroup$
    – Naïm Favier
    Commented Jun 17 at 10:26

0

Reset to default