An extended type system with lambda-typed lambda-expressions
2020
We present the system $\mathtt{d}$, an extended type system with lambda-typed
lambda-expressions. It is related to type systems originating from the Automath
project. $\mathtt{d}$ extends existing lambda-typed systems by an existential
abstraction operator as well as propositional operators. $\beta$-reduction is
extended to also normalize negated expressions using a subset of the laws of
classical negation, hence $\mathtt{d}$ is normalizing both proofs and formulas
which are handled uniformly as functional expressions. $\mathtt{d}$ is using a
reflexive type axiom for a constant $\tau$ to which no function can be typed.
Some properties are shown including confluence, subject reduction, uniqueness
of types, strong normalization, and consistency. We illustrate how, when using
$\mathtt{d}$, due to its limited logical strength, additional axioms must be
added both for negation and for the mathematical structures whose deductions
are to be formalized.
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
0
References
0
Citations
NaN
KQI