object-language의 inference rule들을 기술하는 본인의 meta-language에서의 항과 타입은 다음과 같이 정의됨.

Term ::=

term-variable |

term-constant |

application Term Term |

abstraction term-variable Term |

substitution Term term-variable Term.

Type ::=

type-variable |

type-constant |

function Type Type.

그리고 타입-변수와 항-변수는 소문자로 시작하고, 타입-상수와 항-상수는 대문자로 시작함.

묶인 변수는 추상화를 이용해서 표현하는데, 이것만으로 충분한지는 잘 모르겠음.

그리고 formula와 term의 차이를 없앴음. formula는 Prop형의 term임.

아무튼 충분하다고 하면, t → Prop형의 람다항 M :≡ x : t → A가 있을 때,

Prop형의 항 (∀x) A가 항 ∀ M ≡ ∀ (x : t → A)에 대응하므로 ∀ : (t → Prop) → Prop이란 뜻이었음.