Types as formulas?

Question

This is mainly a terminological question. Is it permissible to refer to a type (e.g. $A$ in $a:A$) as a formula (i.e. speak of "type formulas"), or should the word be reserved to terms? This implies "OK" but this "not really". What's the consensus?

Answer 1

As always, you can do whatever you want as long as you define your terms, and there is almost never a universal consensus on notation and terminology. If you are reading a text, you will have to see what definitions they use. That said, there are definitely more common terms as well as terms that it would make sense to avoid since they would conflict with other commonly used terms.

Neither types nor terms should be referred to as "formulas" in general. There may be some cases where some uses of either types or terms might be reasonably referred to as "formulas", but in general the term "formula" is not really used in type theory.

The examples of "formula" you give are even further off than what a type theorist would likely think you meant by "formula". Type theory is very closely related to logic where the term "formula" has a fairly specific meaning. Terms in type theory usually don't have truth values, so it is usually not appropriate to refer to them as "formulas". (Type theories used as a higher-order logic may actually have a type of truth values, and an expression whose type was the type of truth values could reasonably be referred to as a "formula", but formally it is just a special-case of a term/expression. In a different vein, type theories exploiting the propositions-as-types principle may use different syntax or even have a deeper distinction between types in general and those viewable as propositions. Types viewable as propositions might reasonably be called "formulas" in such a context, but again, they are just special-cases of type expressions.)

In most type theories, for $a:A$, $a$ will be referred to as a "term" or an "expression". It may also be referred to as a "value", though that often means, in particular, a term in normal form. $A$ will be referred to simply as a "type" or perhaps a "type expression". In many type theories, types are terms too (indeed you may have $A:\mathcal U$, i.e. the type $A$ itself has a type). Therefore, all of "term", "expression", and "value" apply (in those contexts) with the same caveats. In programming language theory, which significantly overlaps with type theory, "expression" is often juxtaposed against "statement" or "declaration". An "expression" is a term that has a value while "statements" and "declarations" usually do not. Many type theories do not have these other syntactic classes and only have "expressions". "Term" is a fairly generic word in this context without having too many connotations.

In a logic context, which is, again, very closely related to type theory, "term" means something that you can quantify over and apply predicates to, e.g. numbers. "Terms" are what "formulas" talk about in this context. The way "term" is used in logic, type theory, and programming language theory, is more or less consistent.