natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
The subformula property is a property of cut-free presentations of the sequent calculus. It says that in any derivation
any type appearing above the line is a subformula of one of the types appearing in . This makes it easy to make arguments about provability: while it is not obvious that a cut-full system that the contradiction/empty sequent is derivable, it is a corollary of the subformula property that the is not derivable because all of the rules of the cut-free calculus involve a type above the line.
This property is a formal expression of the modularity of type theoretic connectives: each connective is given by rules which involve only its arguments.
Created on January 25, 2018 at 16:23:27. See the history of this page for a list of all contributions to it.