Judgment Forms

Martin-Löf type theory has four basic forms of judgments and is a considerably more complicated system than first-order logic. One reason is that more information is carried around in the derivations due to the identification of propositions and types. Another reason is that the syntax is more involved. For instance, the well-formed formulas (types) have to be generated simultaneously with the provably true formulas (inhabited types).
The four forms of categorical judgment are

[ltr]⊢Atype⊢Atype[/ltr], meaning that [ltr]AA[/ltr] is a well-formed type,
[ltr]⊢a:A⊢a:A[/ltr], meaning that [ltr]aa[/ltr] has type [ltr]AA[/ltr],
[ltr]⊢A=A[size=13]′⊢A=A′[/ltr][/size], meaning that [ltr]AA[/ltr] and [ltr]A[size=13]′A′[/ltr][/size] are equal types,
[ltr]⊢a=a[size=13]′:A⊢a=a′:A[/ltr][/size], meaning that [ltr]aa[/ltr] and [ltr]a[size=13]′a′[/ltr][/size] are equal elements of type [ltr]AA[/ltr].

In general, a judgment is hypothetical, that is, it is made in a context [ltr]ΓΓ[/ltr], that is, a list [ltr]x[size=13]1:A1,…,xn:Anx1:A1,…,xn:An[/ltr] of variables which may occur free in the judgment together with their respective types. Note that the types in a context can depend on variables of earlier types. For example, [ltr]AnAn[/ltr] can depend on [ltr]x1:A1,…,xn−1:An−1x1:A1,…,xn−1:An−1[/ltr]. The four forms of hypothetical judgments are[/size]

[ltr]Γ⊢AtypeΓ⊢Atype[/ltr], meaning that [ltr]AA[/ltr] is a well-formed type in the context [ltr]ΓΓ[/ltr],
[ltr]Γ⊢a:AΓ⊢a:A[/ltr], meaning that [ltr]aa[/ltr] has type [ltr]AA[/ltr] in context [ltr]ΓΓ[/ltr],
[ltr]Γ⊢A=A[size=13]′Γ⊢A=A′[/ltr][/size], meaning that [ltr]AA[/ltr] and [ltr]A[size=13]′A′[/ltr][/size] are equal types in the context [ltr]ΓΓ[/ltr],
[ltr]Γ⊢a=a[size=13]′:AΓ⊢a=a′:A[/ltr][/size], meaning that [ltr]aa[/ltr] and [ltr]a[size=13]′a′[/ltr][/size] are equal elements of type [ltr]AA[/ltr] in the context [ltr]ΓΓ[/ltr].

Under the proposition as types interpretation

[ltr]⊢a:A(2)(2)⊢a:A[/ltr]

can be understood as the judgment that [ltr]aa[/ltr] is a proof-object for the proposition [ltr]AA[/ltr]. When suppressing this object we get a judgment corresponding to the one in ordinary first-order logic (see above):

[ltr]⊢Atrue.(3)(3)⊢Atrue.[/ltr]

Remark 3.1. Martin-Löf (1994) argues that Kant’s analytic judgment a priori and synthetic judgment a priori can be exemplified, in the realm of logic, by ([analytic]) and ([synthetic]) respectively. In the analytic judgment ([analytic]) everything that is needed to make the judgment evident is explicit. For its synthetic version ([synthetic]) a possibly complicated proof construction [ltr]aa[/ltr] needs to be provided to make it evident. This understanding of analyticity and syntheticity has the surprising consequence that “the logical laws in their usual formulation are all synthetic.” Martin-Löf (1994: 95). His analysis further gives:

اقتباس :: “ […] the logic of analytic judgments, that is, the logic for deriving judgments of the two analytic forms, is complete and decidable, whereas the logic of synthetic judgments is incomplete and undecidable, as was shown by Gödel.” Martin-Löf (1994: 97).

The decidability of the two analytic judgments ([ltr]⊢a:A⊢a:A[/ltr] and [ltr]⊢a=b:A⊢a=b:A[/ltr]) hinges on the metamathematical properties of type theory: strong normalization and decidable type checking.
Sometimes also the following forms are explicitly considered to be judgments of the theory:

[ltr]ΓcontextΓcontext[/ltr], meaning that [ltr]ΓΓ[/ltr] is a well-formed context.
[ltr]Γ=Γ[size=13]′Γ=Γ′[/ltr][/size], meaning that [ltr]ΓΓ[/ltr] and [ltr]Γ[size=13]′Γ′[/ltr][/size] are equal contexts.

Below we shall abbreviate the judgment [ltr]Γ⊢AtypeΓ⊢Atype[/ltr] as [ltr]Γ⊢AΓ⊢A[/ltr] and [ltr]ΓcontextΓcontext[/ltr] as [ltr]Γ⊢.Γ⊢.[/ltr]

3.3 Inference Rules

When stating the rules we will use the letter [ltr]ΓΓ[/ltr] as a meta-variable ranging over contexts, [ltr]A,B,…A,B,…[/ltr]as meta-variables ranging over types, and [ltr]a,b,c,d,e,f,…a,b,c,d,e,f,…[/ltr] as meta-variables ranging over terms.
The first group of inference rules are general rules including rules of assumption, substitution, and context formation. There are also rules which express that equalities are equivalence relations. There are numerous such rules, and we only show the particularly important rule of type equality which is crucial for computation in types:

[ltr]Γ⊢a:AΓ⊢A=BΓ⊢a:BΓ⊢a:AΓ⊢A=BΓ⊢a:B[/ltr]

The remaining rules are specific to the type formers. These are classified as formation, introduction, elimination, and equality rules.

3.4 Intuitionistic Predicate Logic

We only give the rules for [ltr]ΠΠ[/ltr]. There are analogous rules for the other type formers corresponding to the logical constants of typed predicate logic.
In the following [ltr]B[x:=a]B[x:=a][/ltr] means the term obtained by substituting the term [ltr]aa[/ltr] for each free occurrence of the variable [ltr]xx[/ltr] in [ltr]BB[/ltr] (avoiding variable capture).
[ltr]ΠΠ[/ltr]-formation.

[ltr]Γ⊢AΓ,x:A⊢BΓ⊢Πx:A.BΓ⊢AΓ,x:A⊢BΓ⊢Πx:A.B[/ltr]

[ltr]ΠΠ[/ltr]-introduction.

[ltr]Γ,x:A⊢b:BΓ⊢λx.b:Πx:A.BΓ,x:A⊢b:BΓ⊢λx.b:Πx:A.B[/ltr]

[ltr]ΠΠ[/ltr]-elimination.

[ltr]Γ⊢f:Πx:A.BΓ⊢a:AΓ⊢fa:B[x:=a]Γ⊢f:Πx:A.BΓ⊢a:AΓ⊢fa:B[x:=a][/ltr]

[ltr]ΠΠ[/ltr]-equality.

[ltr]Γ,x:A⊢b:BΓ⊢a:AΓ⊢(λx.b)a=b[x:=a]:B[x:=a]Γ,x:A⊢b:BΓ⊢a:AΓ⊢(λx.b)a=b[x:=a]:B[x:=a][/ltr]

This is the rule of [ltr]ββ[/ltr]-conversion. We may also add the rule of [ltr]ηη[/ltr]-conversion:

[ltr]Γ⊢f:Πx:A.BΓ⊢λx.fx=f:Πx:A.B.Γ⊢f:Πx:A.BΓ⊢λx.fx=f:Πx:A.B.[/ltr]

Furthermore, there are congruence rules expressing that operations introduced by the formation, introduction, and elimination rules preserve equality. For example, the congruence rule for [ltr]ΠΠ[/ltr] is

[ltr]Γ⊢A=A′Γ,x:A⊢B=B′[/ltr]

Judgment Forms

3.3 Inference Rules

3.4 Intuitionistic Predicate Logic

Judgment Forms :: تعاليق

Judgment Forms