Summary
My question is about how (i) a certain presentation of pure type systems in the $\lambda$-cube, bears on (ii) a standard definition of consistency in pure type systems. In short, I'm presenting pure type systems to an audience familiar with presentations of first-order logic, but not with presentations of typed languages that invoke typing contexts (for brevity, I won't explain why here). As a result, I think my presentation of pure type systems has weird implications for the standard definition of consistency, according to which a system is consistent just in case not all types are inhabited. And all this raises some interesting issues concerning the relationship between two different definitions of consistency, namely, the standard one, and one closer to the original definition from e.g. first-order logic. That's what I'd like to ask about.
Presentation
Most of what follows is based on (Barendregt, 1992). Let $V$ be an infinite collection of variables, and let $C$ be an infinite collection of constants. The pseudo-expressions $\mathcal{T}$ are generated as follows.
\begin{equation*} \mathcal{T}= V \mid C \mid \mathcal{T}\mathcal{T} \mid \lambda V{:}\mathcal{T}.\mathcal{T} \mid \Pi V{:}\mathcal{T}.\mathcal{T} \end{equation*}
Now for the rules and axioms that describe expressions, which for present purposes, are strings of the form $\phi\mathbin{:}\psi$ (which can be derived from the empty typing context). My audience is familiar with presentations of first-order logic languages that invoke clauses like “For all natural numbers $n$, there are infinitely many predicates $P^{1}$, $P^{2}$, and so on, of arity $n$.” So I have formulated principles for pure type systems that are structurally similar. Here is an example. Let $S=\{\ast,\Box\}\subseteq C$ be the set of sorts. Then consider the principles below. (For brevity, in what follows, I omit additional clauses guaranteeing that each constant/variable gets associated with a unique pseudo-expression.)
Constants. For every sort $\mathfrak{s}$ and every pseudo-expression $\phi$ such that $\phi\mathbin{:}\mathfrak{s}$ is an expression, there are infinitely many constants $\kappa_{1}$, $\kappa_{2}$, and so on, such that $\kappa_{1}\mathbin{:}\phi$, $\kappa_{2}\mathbin{:}\phi$, and so on, are expressions.
Variables. For every sort $\mathfrak{s}$ and every pseudo-expression $\phi$ such that $\phi\mathbin{:}\mathfrak{s}$ is an expression, there are infinitely many variables $\nu_{1}$, $\nu_{2}$, and so on, such that $\nu_{1}\mathbin{:}\phi$, $\nu_{2}\mathbin{:}\phi$, and so on, are expressions.
Two Questions
Consistency is often defined, in pure type systems, like this: a pure type system is consistent just in case the type $\bot$ is not inhabited, where $\bot$ is usually taken to be something like $\Pi x\mathbin{:}\ast.x$. Call this the ‘standard definition’ of consistency.
But of course, given the principles Constants and Variables, $\bot$ is trivially inhabited. For as can be proved using the other rules of certain pure type systems, $(\Pi x\mathbin{:}\ast.x)\mathbin{:}\ast$ is an expression (can be derived from the empty typing context). Since $\ast$ is a sort, Constants implies that there are infinitely many constants $\kappa_{1}$, $\kappa_{2}$, and so on, such that $\kappa_{1}\mathbin{:}(\Pi x\mathbin{:}\ast.x)$, $\kappa_{2}\mathbin{:}(\Pi x\mathbin{:}\ast.x)$, and so on, are expressions. And analogously for Variables.
So my first question is: do I have that right? If principles like Constants and Variables are used in a presentation of pure type systems, will that trivially violate the standard definition of consistency?
My second question concerns the fact that, for my audience, trivially violating the standard definition of consistency isn't actually a bad thing. My audience cares more about using pure type systems to formulate logical principles that are terms with proposition type (again, for brevity, I can't explain why…it is based on a different interpretation of the Curry–Howard correspondence from the standard interpretation…this is part of what makes my presentational task difficult). Those principles need to be consistent, but just in the following sense: given a collection of terms with proposition type, and given a collection of inference rules among those terms specifically, there is no way to derive a contradiction. This other definition of consistency — call it the ‘second definition’ — is, of course, different from the standard definition given above.
So my second question is: when higher-order logical principles — i.e. terms of proposition type which invoke higher-order quantification, etc. — are formulated using the pure type systems in the $\lambda$-cube, are the resulting formal systems consistent in the second sense? For instance, are there collections of higher-order logical principles, formulated in the calculus of constructions, which (i) formalize things like “Every term, of every type, is self-identical” in a single sentence, (ii) include lots of other standard classical axioms and inference rules, and (iii) are consistent in the sense of the second definition?
