2
$\begingroup$

I'm taking rules of inference to be metalinguistic and to describe when you can write down a certain syntactic expression in the object-language given that you already have others written down (e.g. &-Intro in Natural Deduction). I'm taking an axiom to be a syntactic expression in the object-language (logical or non-logical, if the distinction matters, please mention that).

I have been told there is no distinction between rules of inference and axioms in HoTT. Being charitable (I don't think this is a denial in a distinction of the concepts, just their extensions), I am taking this to mean every rule of inference is an axiom and vice-versa.

This is not obvious to see from glancing at the book Homotopy Type Theory: Univalent Foundations of Mathematics. For example, page 434 has the $\Pi$-FORM rule which seems clearly like an inference rule in the metalanguage as it features a turnstile which I take it is not part of the object-language (and also the notation which utilizes the horizontal bar). If there is no distinction, then somehow this should be formalizable simply as a single expression in the object-language? And the same for any other rule?

An example I was given to demonstrate this was the rule:

if $\Gamma\vdash a:A$ and $\Gamma\vdash b:B$, then $\Gamma\vdash (a,b):A\times B$. And, the type $A\rightarrow B\rightarrow A\times B$.

To me this seems like conflating rules of inference with types just because there is a correspondence between the two.

So is there a distinction between rules of inference and axioms in HoTT?

$\endgroup$
9
  • 3
    $\begingroup$ Who says there is no distinction between rules and axioms in HoTT? $\endgroup$
    – Zhen Lin
    Mar 24 at 4:31
  • $\begingroup$ I'll try to answer your question in a longer post, but I'll just quickly point out here that the expression you wrote toward the end requires a small correction. It should presumably read "if $\Gamma \vdash a : A$ and $\Gamma \vdash b : B$, then $\Gamma \vdash (a, b) : A \times B$." $\endgroup$
    – Menander I
    Mar 24 at 5:41
  • $\begingroup$ In my opinion, you are conflating two different distinction here: the distinction between the object language and the metalanguage, and the orthogonal distinction between axioms and rules of inference. An axiom, to me, is simply a rule of inference with no premises. $\endgroup$
    – Pilcrow
    Mar 24 at 13:09
  • $\begingroup$ @Pilcrow I know of this way of viewing them and it might be an adequate way to conceptualize rules of inference and axioms, but I don't know how standard this is in the logic community. For example, this doesn't align well with the phrase "axioms of ZFC" and the like. People don't think about axioms of ZFC as "rules of inference for set theory with no premises". They just take them to be expressions in the object language that are taken to be the starting point for the theory. $\endgroup$
    – Alvaro P.
    Mar 24 at 15:18
  • 1
    $\begingroup$ As best as I can tell, without having heard exactly what you've been told, I would say that what you've been told is wrong. HoTT maintains a distinction between rules of inference and axioms just like most other type theories, as you've explained. Can you give a citation or reference to whoever told you this? $\endgroup$ Mar 27 at 1:05

1 Answer 1

2
$\begingroup$

The HoTT book makes a difference between axioms and rules in the "Open problem" section of its Introduction chapter. See also the "Basic metatheory" chapter in Appendix A.4.

This is related to the constructivity property of the theory, and more accurately to its canonicity property. In short, we could say that an axiom is a rule of inference that is not constructive.

In a perfectly constructive setting, you expect that any closed term $a$ of type $A$ reduces by normalization to a canonical form that is a composition of the constructors of $A$.

This good property holds when you restrict HoTT to the inductive types defined using the uniform pattern consisting in the formation / introduction / elimination and computation rules.

In the HoTT book, the canonicity property is lost when you add other inference rules that do not match that pattern, such as the axiom of choice, the law of excluded middle, function extensionality, or univalence. A term defined with such axioms cannot be reduced by normalization to a canonical form defined with only the constructors: the axioms "do not compute", they postulate the existence of a canonical term with an expected property, but do not tell you how to effectively compute this canonical term.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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