1
$\begingroup$

From Calculus Of Constructions :

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?

$\endgroup$
8
  • $\begingroup$ The first one corresponds to the Axiom rule of Sequent Calculus: $A \vdash A$. $\endgroup$ Jul 1, 2021 at 10:09
  • $\begingroup$ 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$. $\endgroup$ Jul 1, 2021 at 10:17
  • 2
    $\begingroup$ 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. $\endgroup$ Jul 1, 2021 at 10:21
  • 1
    $\begingroup$ @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? $\endgroup$
    – MCCCS
    Jul 1, 2021 at 10:57
  • 1
    $\begingroup$ 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) $\endgroup$
    – Potato44
    Jul 1, 2021 at 11:18

1 Answer 1

2
$\begingroup$

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)$.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .