# Help me understand type theory notation

Does this mean, for definition environment $$\Gamma$$, for $$x$$ is of type $$A$$, and for even more definitions $$\Gamma '$$, it is assumed that there are no contradictions so adding more definitions does not change a term's type?

And is :

"If A is of type K" and "if B is of type L", all instances of type A, B are of type L. Am I missing something, how can we know that K (or A) is of type L?

• The first one corresponds to the Axiom rule of Sequent Calculus: $A \vdash A$. Jul 1, 2021 at 10:09
• The second one is the formation rule for the universal quantifier: we have the type specs for $A$ and for $B$, where the second premises states that for every $x$ in $A$ (of type $K$) we have that $B$ is of type $L$. Then also $(\forall x : A.B)$ is of type $L$. Jul 1, 2021 at 10:17
• Possible example with predicate logic: $x$ is a variable for object of a certain type $A$ and $B$ is a prop function expressing a property of objects. The right assumption states that for every value of variable $x$ the prop function $Bx$ is a meaningful proposition. Thus, also the formula $(\forall x \in A)Bx$ is a meaningful proposition. Jul 1, 2021 at 10:21
• @MauroALLEGRANZA Understood, thank you! I would accept this as answer. One last question: What is the $.$ operator as in $A.B$? Is it A's corresponding B? Jul 1, 2021 at 10:57
• No*. Are you familier with the meaning of $\forall x . B$ in predicate logic? This is like that but also specifies a type we are quantifying over. * (I could imagine someone using this notation for dependent product, but using the notation from the wikipedia article what you have wrtitten is just not part of the syntax) Jul 1, 2021 at 11:18

The first rule corresponds to the Axiom rule of Sequent Calculus: $$A \vdash A$$.

The conclusion $$x : A$$ is already part of the set of premises.

The second one is the formation rule for the universal quantifier: we have the type specifications for $$A$$ and $$B$$, where the second premise states that for every $$x \in A$$ (of type $$K$$) we have that $$B$$ is of type $$L$$. Then also $$(∀x:A.B)$$ is of type $$L$$.

For an example with predicate logic, consider a variable $$x$$ for objects of a certain type $$A$$ and consider as $$B$$ a propositional function expressing a property of these objects.

The right assumption states that for every value of variable $$x$$ the propositional function $$Bx$$ is a meaningful proposition.

With these conditions, also the formula $$(∀x: A.B)$$ is a meaningful proposition.

We may read it as: $$(∀x∈A)Bx$$ that, in predicate logic, is exactly $$∀x(Ax → Bx)$$.