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
Typed predicate logic or logic over type theory can be represented in the language of natural deduction as a two-layered type theory consisting of a layer of propositions represented by the judgment , over a layer of types represented by the judgment . A predicate on a type in typed predicate logic is simply a proposition in the context of a variable of , .
One could add additional logical operations to the proposition layer, such as rules for false, true, conjunction, disjunction, implication, universal quantifier, and existential quantifier, as well as additional rules to the type layer, such as rules for propositional equality.
The type layer could either be a simple type theory or dependent type theory, examples of the former include ZFC and fully formal ETCS, while the latter includes the SEAR, as well as presentations of dependent type theory which use propositional equality instead of judgmental equality for definitional equality and conversional equality.
Typed predicate logic is used in many type theories, including simplicial type theory and cubical type theory, where the main dependent type theory is built over a typed predicate logic.
Typed predicate logic is a type theory which consists of two layers, a layer for types and a layer for propositions.
We have the basic judgement forms of the type layer:
And the basic judgement forms of the proposition layer:
As well as context judgments:
Contexts are defined by the following rules:
The structural rules in logic over type theory include the variable rules, the weakening rules, and the substitution rule.
The variable rules states that we may derive a typing judgment or a true proposition judgment if the typing judgment or true proposition judgment is in the context already:
Let be any arbitrary judgment. Then we have the following rules:
The weakening rules:
The substitution rule:
The weakening and substitution rules are admissible rules: they do not need to be explicitly included in the type theory as they could be proven by induction on the structure of all possible derivations.
Sometimes, typed predicate logic comes with a notion of equality on all the types, propositional equality, and the theory then becomes typed predicate logic with equality.
Propositional equality of types and terms is formed by the following rules:
Propositional equality has its own structural rules: reflexivity, symmetry, transitivity, the principle of substitution, and the variable conversion rule.
Principle of substitution of propositionally equal terms:
Variable conversion rule:
In any typed predicate logic with equality, we could formally define the single assignment operator used in definitions in the theory itself.
We add the following judgments to the theory:
The single assignment operator has its own structural rules: type formation, term introduction, and equality reflection.
Formation and equality reflection rules for type definition:
Introduction and equality reflection rules for term definition:
Last revised on December 19, 2022 at 17:49:02. See the history of this page for a list of all contributions to it.