nLab typed predicate logic

Redirected from "logics over type theory".

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Idea

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 PpropP \; \mathrm{prop}, over a layer of types represented by the judgment AtypeA \; \mathrm{type}. A predicate PP on a type AA in typed predicate logic is simply a proposition PP in the context of a variable of AA, x:APpropx:A \vdash P \; \mathrm{prop}.

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.

Presentation

Judgments and contexts

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:

  • ΓAtype\Gamma \vdash A\; \mathrm{type} - AA is a well-typed type in context Γ\Gamma.
  • Γa:A\Gamma \vdash a : A - aa is a well-typed term of type AA in context Γ\Gamma.

And the basic judgement forms of the proposition layer:

  • Γϕprop\Gamma \vdash \phi \; \mathrm{prop} - ϕ\phi is a well-formed proposition in context Γ\Gamma
  • Γϕtrue\Gamma \vdash \phi \; \mathrm{true} - ϕ\phi is a well-formed true proposition in context Γ\Gamma

As well as context judgments:

  • Γctx\Gamma \; \mathrm{ctx} - Γ\Gamma is a well-formed context.

Contexts are defined by the following rules:

()ctxΓctxΓAtype(Γ,a:A)ctxΓctxΓϕprop(Γ,ϕtrue)ctx\frac{}{() \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash A \; \mathrm{type}}{(\Gamma, a:A) \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash \phi \; \mathrm{prop}}{(\Gamma, \phi \; \mathrm{true}) \; \mathrm{ctx}}

Structural 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:

Γ,aA,ΔctxΓ,aA,ΔaAΓ,Ptrue,ΔctxΓ,Ptrue,ΔPtrue\frac{\Gamma, a \in A, \Delta \; \mathrm{ctx}}{\Gamma, a \in A, \Delta \vdash a \in A} \qquad \frac{\Gamma, P \; \mathrm{true}, \Delta \; \mathrm{ctx}}{\Gamma, P \; \mathrm{true}, \Delta \vdash P \; \mathrm{true}}

Let 𝒥\mathcal{J} be any arbitrary judgment. Then we have the following rules:

The weakening rules:

Γ,Δ𝒥ΓAtypeΓ,a:A,Δ𝒥Γ,Δ𝒥ΓPpropΓ,Ptrue,Δ𝒥\frac{\Gamma, \Delta \vdash \mathcal{J} \quad \Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, \Delta \vdash \mathcal{J}} \qquad \frac{\Gamma, \Delta \vdash \mathcal{J} \quad \Gamma \vdash P \; \mathrm{prop}}{\Gamma, P \; \mathrm{true}, \Delta \vdash \mathcal{J}}

The substitution rule:

Γa:AΓ,b:A,Δ𝒥Γ,Δ[a/b]𝒥[a/b]\frac{\Gamma \vdash a:A \quad \Gamma, b:A, \Delta\vdash \mathcal{J}}{\Gamma, \Delta[a/b] \vdash \mathcal{J}[a/b]}

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.

Typed predicate logic with equality

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:

ΓAtypeΓBtypeΓA=Bprop\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A = B \; \mathrm{prop}}
ΓAtypeΓa:AΓb:AΓa= Abprop\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A}{\Gamma \vdash a =_A b \; \mathrm{prop}}

Propositional equality has its own structural rules: reflexivity, symmetry, transitivity, the principle of substitution, and the variable conversion rule.

  • Reflexivity of propositional equality
ΓAtypeΓA=Atrue\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash A = A \; \mathrm{true}}
ΓAtypeΓa:AΓa= Aatrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A}{\Gamma \vdash a =_A a \; \mathrm{true}}
  • Symmetry of propositional equality
ΓAtypeΓBtypeΓA=BtrueΓB=Atrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash A = B \; \mathrm{true}}{\Gamma \vdash B = A \; \mathrm{true}}
ΓAtypeΓa:AΓb:AΓa= AbtrueΓb= Aatrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash a =_A b \; \mathrm{true}}{\Gamma \vdash b =_A a \; \mathrm{true}}
  • Transitivity of propositional equality
ΓAtypeΓBtypeΓCtypeΓA=BtrueΓB=CtrueΓA=Ctrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash A = B \; \mathrm{true} \quad \Gamma \vdash B = C \; \mathrm{true}}{\Gamma \vdash A = C \; \mathrm{true}}
ΓAtypeΓa:AΓb:AΓc:AΓa= AbtrueΓb= ActrueΓa= Actrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash c:A \quad \Gamma \vdash a =_A b \; \mathrm{true} \quad \Gamma \vdash b =_A c \; \mathrm{true}}{\Gamma \vdash a =_A c \; \mathrm{true}}
  • Principle of substitution of propositionally equal terms:

    ΓAtypeΓa:AΓb:AΓa= AbtrueΓ,x:A,ΔBtypeΓ,Δ[b/x]B[a/x]=B[b/x]true\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a : A \quad \Gamma \vdash b : A \quad \Gamma \vdash a =_A b \; \mathrm{true} \quad \Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[b/x] \vdash B[a/x] = B[b/x] \; \mathrm{true}}
    ΓAtypeΓa:AΓb:AΓa= AbtrueΓ,x:A,Δc:BΓ,Δ[b/x]c[a/x]= B[b/x]c[b/x]true\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a : A \quad \Gamma \vdash b : A \quad \Gamma \vdash a =_A b \; \mathrm{true} \quad \Gamma, x:A, \Delta \vdash c:B}{\Gamma, \Delta[b/x] \vdash c[a/x] =_{B[b/x]} c[b/x] \; \mathrm{true}}
  • Variable conversion rule:

ΓAtypeΓBtypeΓA=BtrueΓ,x:A,Δ𝒥Γ,x:B,Δ𝒥\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash A = B \; \mathrm{true} \quad \Gamma, x:A, \Delta \vdash \mathcal{J}}{\Gamma, x:B, \Delta \vdash \mathcal{J}}

Definitions

In any typed predicate logic with equality, we could formally define the single assignment operator \coloneqq used in definitions in the theory itself.

We add the following judgments to the theory:

  • ΓAAtype\Gamma \vdash A' \coloneqq A \; \mathrm{type} - AA' is defined to be the type AA in context Γ\Gamma.
  • Γaa:A\Gamma \vdash a' \coloneqq a : A - aa' is defined to be the term a:Aa:A of type AA in context Γ\Gamma.

The single assignment operator has its own structural rules: type formation, term introduction, and equality reflection.

  • Formation and equality reflection rules for type definition:

    ΓBAtypeΓBtypeΓBAtypeΓB=Atrue\frac{\Gamma \vdash B \coloneqq A \; \mathrm{type}}{\Gamma \vdash B \; \mathrm{type}} \qquad \frac{\Gamma \vdash B \coloneqq A \; \mathrm{type}}{\Gamma \vdash B = A \; \mathrm{true}}
  • Introduction and equality reflection rules for term definition:

    Γba:AΓb:AΓba:AΓb= Aatrue\frac{\Gamma \vdash b \coloneqq a:A}{\Gamma \vdash b:A} \qquad \frac{\Gamma \vdash b \coloneqq a:A}{\Gamma \vdash b =_A a \; \mathrm{true}}

Examples

 See also

Last revised on December 19, 2022 at 17:49:02. See the history of this page for a list of all contributions to it.