Vincent Demange
email: vincent.demange@loria.fr

Pedagogical lambda-cube: the λ 2 case

Keywords: typed lambda-calculus, calculus of constructions, pedagogical formal systems, mathematical logic, negationless mathematics, constructive mathematics. 2

In pedagogical formal systems one needs to systematically give examples of hypotheses made. This main characteristic is not the only one needed, and a formal definition of pedagogical sub-systems of the Calculus of Constructions (CC) has already been stated. Here we give such a pedagogical sub-system of CC corresponding to the second-order pedagogical λ-calculus of Colson and Michel. It thus illustrates the appropriateness of the formal definition, and opens the study to stronger systems of the λ-cube, for which CC is the most expressive representative. In addition we study the type-checking problem for the formalisms of those pedagogical calculi of second-order.

Introduction

The Poincaré criterion The main feature of pedagogical formal systems is to always require the user to give examples of used hypotheses. This need for systematic exemplification has lead to the terminology of pedagogical formal systems, because it is the formal counterpart of the usual informal teaching practice consisting of giving examples of newly introduced notions. The necessity of such a constraint was already observed by Poincaré [START_REF] Poincaré | Dernières pensées[END_REF] in the case of definitions by postulates: "A definition by postulate has value only when the existence of the object defined has been proved [...] by means of examples [...].". Since every set of hypotheses made on some objects (e.g. propositions or λ-terms) can be seen as a set of definitions by postulates, in the following when for a formal system every set of used hypotheses can be exemplified we will say it meets the Poincaré criterion.

Formal pedagogy More formally, for instance in propositional natural deduction systems -studied by Colson and Michel up to the propositional second-order calculus in [START_REF] Colson | Pedagogical natural deduction systems: the propositional case[END_REF][START_REF] Colson | Pedagogical Second-order Propositional Calculi[END_REF]-whenever one wants to use the set of formulas ∆ as hypotheses she must give a substitution σ (the examples) from propositional variables to formulas such that ⊢σ(A) for each A ∈ ∆. Through the propositions-as-types correspondence [START_REF] Howard | The formulas-as-types notion of construction[END_REF] this requirement extends to type systems -second-order λ-calculus studied by Colson and Michel in [START_REF] Colson | Pedagogical second-order λ-calculus[END_REF]: a typing environment x 1 : A 1 , . . . , x n : A n can be exemplified if there are terms t i and a substitution σ from type variables to types such that ⊢t i : σ(A i ).

1 From a logical point of view and in an intuitionist framework, this pedagogical constraint does not allow the use of negation and reasoning by contradiction: it is no more possible to assume a formula A that will reveal to be a contradiction since no instance of this formula can be proved. It then agrees with the negationless mathematics advocated by Griss as a refinement of intuitionism [START_REF] Griss | Negationless intuitionistic mathematics[END_REF][START_REF] Griss | Negationless intuitionistic mathematics II[END_REF][START_REF] Griss | Negationless intuitionistic mathematics III[END_REF][START_REF] Griss | Negationless intuitionistic mathematics IVa, IVb[END_REF].

From a computational point of view, it means that for every type at least one of its instances has to be inhabited by a term. This last property leads to the notion of usefulness of λ-terms in pedagogical type systems: every function f of type A → B can be applied to a term u of type A when A is closed.

Overview of the article In this article, we will focus on the extension of these results to the type systems of the Barendregt's λ-cube [START_REF] Barendregt | Lambda calculi with types, volume 2 of Handbook of Logic in Computer Science[END_REF]. Indeed those systems have logical and computational meaning, and the most powerful is the Calculus of Constructions (CC) of Coquand [START_REF] Coquand | Une théorie des constructions[END_REF] for which a formal study of pedagogy has already been investigated by Colson and Demange in [START_REF] Colson | Investigations on a pedagogical calculus of constructions[END_REF]. First the formalism of CC being more explicit, the Poincaré criterion become: if an environment x 1 : A 1 , . . . , x n : A n is well-formed1 then there are terms t i such that ⊢t i : A i [x 1 , . . . , x i-1 ← t 1 , . . . , t i-1 ] where [ • ← • ] is the usual substitution from variables to terms. The conclusion of the investigation was a complete formal definition of a pedagogical subsystem of CC (see def. 10): the formal system has to (i) be a subsystem of CC; (ii) verify subject reduction; (iii) meet the Poincaré criterion; (iv) and meet the converse of the Poincaré criterion. The converse of the Poincaré criterion is needed to ensure expressiveness: in [START_REF] Colson | Investigations on a pedagogical calculus of constructions[END_REF] a system CC r satisfying (i), (ii) and (iii) but not (iv) has been exhibited with a good computational power but strong logical limitations. Also in [START_REF] Colson | Pedagogical Second-order Propositional Calculi[END_REF] a weakly pedagogical second-order calculus P s -Prop 2 has been stated for which a type system can be obtained satisfying (i), (iii) and (iv) but not (ii).

At the end of the study about pedagogical CC, it was suggested that it is possible to build a pedagogical subsystem of CC in the precise sense of the previous definition, corresponding to the pedagogical second-order λ-calculus P-Prop 2 of [START_REF] Colson | Pedagogical second-order λ-calculus[END_REF]. This construction is the main subject of this present paper, the difficulties were mainly due to a difference in formalism, the one of P-Prop 2 -and of Girard's System F [START_REF] Girard | Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur[END_REF]-being more liberal than the one of CC, and the need to stick to the definition. Especially the (i) of the previous definition does not allow the addition of constant symbols (initial examples) to the calculus, which was the case in P-Prop 2 .

Outline of the article In section 2 we recall the usual notations, definitions and well-known results about the calculus of constructions (CC) and its subsystem of second order λ 2 . In sections 3, 4, 5 we define and study pedagogical subsystems of CC of second order: first with explicit and total examples (also called motivations) λ 2 e , then with total motivations λ 2 t and finally with partial motivations λ 2 p . Each is obtained from the previous by relaxing some constraints, the last one fully satisfying the definition of pedagogical subsystem of CC. Then in section 6 we link those systems with the previously stated pedagogical second order λ-calculus P-Prop 2 of [START_REF] Colson | Pedagogical second-order λ-calculus[END_REF]. We end in section 7 by showing the undecidabilty of type checking for all those type systems. Finally we conclude in section 8 by suggesting a formalism to recover type checking in pedagogical formal systems, and open the study toward more expressive systems of the λ-cube based on the current work.

Related works Obviously the works on pedagogical formal systems previously mentioned are relevant: the minimal propositional calculus over →, ∧ and ∨ has been studied in [START_REF] Colson | Pedagogical natural deduction systems: the propositional case[END_REF]; the second order propositional calculus in [START_REF] Colson | Pedagogical Second-order Propositional Calculi[END_REF]; the second-order λ-calculus in [START_REF] Colson | Pedagogical second-order λ-calculus[END_REF]; and an investigation on the whole Calculus of Constructions in [START_REF] Colson | Investigations on a pedagogical calculus of constructions[END_REF]. A great overview of those works can be found in the introduction of [START_REF] Colson | Investigations on a pedagogical calculus of constructions[END_REF], to which we can add the following unmentioned and unpublished2 result of Michel in [START_REF] Michel | Systèmes formels et systèmes fonctionnels pédagogiques[END_REF]: every λ-term of the second-order λ-calculus admit a continuation passing style translation that can be typed in the pedagogical second-order λ-calculus, ensuring the preservation of programs.

Also in an intuitionistic framework, which is the case here, pedagogical mathematics are linked with the negationless mathematics philosophy. The idea of negationless mathematics appeared in the middle of the last century when Griss expressed it as a step further of the intuitionistic philosophy of Brouwer. Indeed, in intuitionistic mathematics, a proof of a negative statement ¬A impose to assume A in order to obtain a contradiction. But assuming A is no intuitive method for Griss since it will reveal to be an impossible construction. First works of Griss [START_REF] Griss | Negationless intuitionistic mathematics[END_REF][START_REF] Griss | Negationless intuitionistic mathematics II[END_REF][START_REF] Griss | Negationless intuitionistic mathematics III[END_REF][START_REF] Griss | Negationless intuitionistic mathematics IVa, IVb[END_REF] constitute an informal outline of a geometry, an arithmetic, a set theory and an analysis without negation. Heyting [START_REF] Heyting | Griss and his negationless intuitionistic mathematics[END_REF] and Franchella [START_REF] Franchella | Brouwer and Griss on intuitionistic negation[END_REF] summarize differences of viewpoint about intuitionism of Brouwer and that of Griss. Some formal developments of the Griss desiderata has been proposed, from which we can cite those of Vredenduin [START_REF] Vredenduin | The logic of negationless mathematics[END_REF], Gilmore [START_REF] Gilmore | The effect of Griss' criticism of the intuitionistic logic on deductive theories formalized within the intuitionistic logic[END_REF], Valpola [START_REF] Valpola | Ein system der negationlosen Logik mit ausschliesslich realisierbaren Prädicaten[END_REF], Nelson [START_REF] Nelson | Non-Null Implication[END_REF][START_REF] Nelson | A complete negationless system[END_REF], Minichiello [START_REF] Kent | An extension of negationless logic[END_REF], López-Escobar [START_REF] López-Escobar | Constructions and negationless logic[END_REF][START_REF] López-Escobar | Elementary interpretations of negationless arithmetic[END_REF], Mezhlumbekova [START_REF] Mezhlumbekova | Deductive capabilities of negationless intuitionistic arithmetic[END_REF] and more recently of Krivtsov [START_REF] Victor | A Negationless Interpretation of Intuitionistic Theories[END_REF][START_REF] Victor | A Negationless Interpretation of Intuitionistic Theories[END_REF], dealing with negationless predicate logic and arithmetic in natural deduction systems or in sequent calculus. One of the main ideas is the introduction of a quantified implication A( x) → x B( x) which is interpreted in intuitionistic logic by ∀ x A( x) → B( x) ∧ ∃ xA( x). Mints [START_REF] Mints | Notes on Constructive Negation[END_REF] provides a good overview of those works. and u, v, A, B are raw terms. S(u) is the set of sub-terms of u, containing u. For brevity, in the following terms will refer to raw terms.

≡ is the syntactical equality of terms modulo renaming of bound variables3 . We note by β the usual beta-reduction relation between terms; * β its reflexive and transitive closure; and = β its equivalence closure. A term u is in normal form if it is not reducible, i.e. there is no term t such that u β t. If all possible reductions from a term u lead to a normal form, then the term u is said to be strongly normalizing.

V(t) is the set of free variables of t. If V(t) = ∅ then t is said to be closed. The usual capture avoiding substitution of u for x in t is noted t[x ← u ]; and t[x 1 , . . . , x n ← u 1 , . . . , u n ] is the simultaneous substitution of u 1 for x 1 , u 2 for x 2 , etc. in t. When dealing with substitutions as mathematical objects, we will use list symbolism: [ ] is the empty substitution, and if σ is a substitution then σ::(x → a) is a new substitution mapping all variables y = x to σ(y) and x to a. The application of a substitution is extended from variables to terms in the usual way: if σ ≡ (x 1 → u 1 ):: . . . ::

(x n → u n ) then σ(t) = t[x 1 , . . . , x n ← u 1 , . . . , u n ].
To shorten notations, we might use a vector symbolism: t denotes a sequence of terms t 1 , . . . , t n ; and

∀ x A .B denotes ∀x A1 1 . . . ∀x An n .B. As usual, A → B is short for ∀x A .B when x does not appear in V(B).
An environment is a finite list of associations variable-term. The empty environment is noted [ ] or omitted, otherwise it is of the form x 1 : A 1 , . . . , x n : A n , or Γ, Γ ′ where Γ and Γ ′ are environments. The domain of an environment is the finite set of its variables: dom(x

1 : A 1 , . . . , x n : A n ) = {x 1 , . . . , x n }. Substitutions can be applied to environments: (x 1 : A 1 , . . . , x n : A n )[y ← u ] ≡ x 1 : A 1 [y ← u ], . . . , x n : A n [y ← u ]. Γ ′ ≡ x 1 : A 1 , . . . , x i : A i is an initial segment of Γ ≡ x 1 : A 1 , . . . , x n : A n when i ≤ n, abbreviated by Γ ′ Γ.
Similarly for substitutions σ ′ σ. We will also write Γ ≤i or Γ <i for the first i-th (resp. i -1-th) elements of Γ, similarly with σ ≤i or σ <i .

In CC there are two kinds of judgements: Γ wf c means that the environment Γ is syntactically well-formed, and Γ ⊢ c t : A expresses that the term t is of type A in the environment Γ.

Implicitly, Γ ⊢ c A : κ signifies that there is κ ∈ {Prop, Type} such that this previous statement holds. Γ ⊢ c A 1 : A 2 : . . . : A n is the contraction of Γ ⊢ c A 1 : A 2 , etc. and Γ ⊢ c A n-1 : A n . If the contraction appears as a premise of a rule it denotes n -1 premises, and as a conclusion of a rule it expands to n -1 possible conclusions (i.e. n -1 rules).

Rules of CC are presented in fig. 1: close presentations can be found in [START_REF] Coquand | An analysis of girard's paradox[END_REF], with well formed judgements; in [START_REF] Bunder | Variants of the Basic Calculus of Constructions[END_REF] avoiding weakening rule; or [START_REF] Barendregt | Lambda calculi with types, volume 2 of Handbook of Logic in Computer Science[END_REF] presenting usual properties of CC. Removing some rules of CC we obtain λ 2 of fig. 2, a subsystem corresponding to the polymorphic λ-calculus also known as the system F of Girard-Reynolds [START_REF] Girard | Le lambda-calcul du second ordre[END_REF][START_REF] Reynolds | Towards a theory of type structure[END_REF]. Notice that the raw-terms stay the same.

As usual a derivation of a judgement is a finite tree rooted by the judgement and where leafs are instances of inference rules without premise. A sub-derivation is then a sub-tree, and a strict sub-derivation is a sub-tree which is not the whole tree.

(c-env 1 ) [ ] wf c Γ ⊢ c A : κ x ∈ dom(Γ) (c-env 2 ) Γ, x : A wf c Γ wf c (c-ax) Γ ⊢ c Prop : Type Γ, x : A, Γ ′ wf c (c-var) Γ, x : A, Γ ′ ⊢ c x : A Γ, x : A ⊢ c u : B : κ (c-abs) Γ ⊢ c λx A .u : ∀x A .B Γ ⊢ c u : ∀x A .B Γ ⊢ c v : A (c-app) Γ ⊢ c u v : B[x ← v ] Γ, x : A ⊢ c B : κ (c-prod) Γ ⊢ c ∀x A .B : κ Γ ⊢ c t : A Γ ⊢ c A ′ : κ A = β A ′ (c-conv) Γ ⊢ c t : A ′
where κ stands for Prop or for Type.

Figure 1: Inference rules of CC.

(env 1 ) [ ] wf 2 Γ ⊢ 2 A : κ x ∈ dom(Γ) (env 2 ) Γ, x : A wf 2 Γ wf 2 (ax) Γ ⊢ 2 Prop : Type Γ, x : A, Γ ′ wf

Properties of CC

In the sequel we shall need the following well-known results about CC and λ 2 (omitted proofs can be found in [START_REF] Barendregt | Lambda calculi with types, volume 2 of Handbook of Logic in Computer Science[END_REF]). Starred relations refer to both CC and λ 2 , meaning that the property holds in both systems.

Property 1 (free variables)

(i) If x 1 : A 1 , . . . , x n : A n wf ⋆ or x 1 : A 1 , . . . , x n : A n ⊢ ⋆ w : C then for all i, V(A i+1 ) ⊆ {x 1 , .
. . , x i } and x i ≡ x j for all i = j;

(ii) If x 1 : A 1 , . . . , x n : A n ⊢ ⋆ w : C then in addition V(w, C) ⊆ {x 1 , . . . , x n }.
Property 2 If Γ wf ⋆ or Γ ⊢ ⋆ w : C then Type ∈ S(Γ) and Type ∈ S(w).

Property 3 (environments validity)

(i) if Γ wf ⋆
, then for all environments Γ ′ Γ, Γ ′ wf ⋆ is a sub-derivation;

(ii) if Γ ⊢ ⋆ w : C, then for all environments Γ ′ Γ, Γ ′ wf ⋆ is a strict sub-derivation.

Property 4 (environment types validity) If x 1 : A 1 , . . . , x n : A n wf ⋆ , then for all i there is κ such that x 1 : A 1 , . . . , x i : Proof by case analysis on the last used rule. (i) (var) Impossible case because Type can not be in the environment (prop. 2).

A i ⊢ ⋆ A i+1 : κ is a strict sub-derivation. Property 5 (type uniqueness) If Γ ⊢ 2 w : C and Γ ⊢ 2 w : C ′ then C ≡ C ′ . Property 6 (type correctness) If Γ ⊢ ⋆ w : C then C ≡ Type or Γ ⊢ ⋆ C : κ.
(app) There are two cases:

⊢ ⋆ t 1 : A 1 ⊢ ⋆ t 2 : A 2 [x 1 ← t 1 ] . . . ⊢ ⋆ t n : A n [x 1 , . . . , x n-1 ← t 1 , . . . , t n-1 ]
3 Total and explicit motivations

Usually the current state of a proof is indicated by a sequent Γ ⊢t : A meaning that "t is a proof of A under the assumptions Γ". In the pedagogical practice we also need examples of the hypotheses of Γ which we can make explicit using enhanced sequents of the form Γ ⊢ σ t : A meaning "t is a proof of A under the assumptions Γ exemplified by σ" where σ is a substitution from the variables of Γ to terms. In the same way we switch from judgements Γ wf to Γ wf σ . Each assumption/variable of Γ has to be examplified by σ, hence the total and explicit motivations system λ 2 e of fig. 3. Making the examples/motivations explicit have at least two benefits. First it allows to better reflect the practice of pedagogical mathematics by using a global example during a proof. Second it simplifies and specifies the statements about the formalism: we can act on the motivations and then appreciate the constraints they impose or they are subject to.

System definition

We extend the raw terms with the two constants o and ⊤. Inference rules of λ 2 e are presented on fig. 3. The (prod) rule of λ 2 is constrained as (e-prod) in λ 2 e in order to avoid empty types as soon as possible (e.g. ∀A Prop .A). Indeed those empty types can not be examplified, and allowing to manipulate them could break the subject reduction property (see [START_REF] Colson | Pedagogical Second-order Propositional Calculi[END_REF]) or the Poincaré criterion if we introduce them into environments. The added constraint then requires that the formed type to be compatible with the current motivation σ, namely that the instance σ(∀x A .B) be inhabited.

Also the additional (second) premise of the rule (e-env 2 ) should not be considered as a constraint: the term a is already contained in the derivation of the first premise

(e-env 1 ) [ ] wf 2e [ ] Γ ⊢ 2e σ A : κ ⊢ 2e [ ] a : σ(A) x ∈ dom(Γ) (e-env 2 )
Γ, x : A wf

Γ ⊢ 2e σ λx A .u : ∀x A .B Γ ⊢ 2e σ u : ∀x A .B Γ ⊢ 2e σ v : A (e-app) Γ ⊢ 2e σ u v : B[x ← v ] Γ, x : A ⊢ 2e σ::(x → a) B : Prop ⊢ 2e [ ] t : σ(∀x A .B) (e-prod)
Γ ⊢ (see lem. 17). This last fact is important for explicit motivations systems: if Γ ⊢ 2e σ A : κ does not permit us to build an example a of σ(A) then it means the motivabilty, and consequently the usability, of the type A has not been tested soon enough.

Remark 11

Substitutions and environments related by wf 2e or ⊢ 2e match: they have the same size, and to each variable of the environment correspond a raw term at the same position in the substitution (see lem. 13).

The constants o and ⊤, the initial examples, are mandatory to begin derivations: otherwise one would only be allowed to derive [ ] wf 2e [ ] and ⊢ 2e [ ] Prop : Type.

In this section we show that λ 2 e almost satisfies the required properties of a pedagogical subsystem of CC: indeed in λ 2 e judgements and raw-terms are modified with respect to those of λ 2 and then CC.

Preliminary results

The properties 1, 2, 3, 4, 5, 6, 8, 9 are still valid for λ 2 e , modulo the addition of the corresponding explicit motivations.

Theorem 12 (λ 2 e is a subsystem of λ 2 ) (i) if Γ wf 2e σ , then Γ wf 2 ; (ii) if Γ ⊢ 2e σ w : C, then Γ ⊢ 2 w : C.
Proof immediate by structural induction on the derivation: it is enough to "forget" explicit motivations and to interpret in λ 2 the constants o and ⊤ of λ 2 e by, respectively, λA Prop .λx A .x and ∀A Prop .A → A.

Lemma 13 If x

1 : A 1 , . . . , x n : A n wf 2e σ or x 1 : A 1 , . . . , x n : A n ⊢ 2e
σ w : C where σ ≡ (y 1 → t 1 ):: . . . ::(y m → t m ) then m = n, and for all i x i ≡ y i and t i is closed. Proof by case analysis on the last used rule, similar to the proof for λ 2 (prop. 7): to show that a derivation is impossible for λ 2 e , it is enough to notice that λ 2 e is a subsystem of λ 2 (thm. 12) and that the corresponding derivation is already impossible in λ 2 . Proof by structural induction on the derivation of x 1 : A 1 , . . . , x n : A n wf 2e σ :

Lemma 14 (generation) If Γ ⊢ 2e σ t : T then one of these cases holds: (i) if t ≡ o, then T ≡ ⊤; (ii) if t ≡ ⊤, then T ≡ Prop; (iii) if t ≡ Prop, then T ≡ Type; (iv) if t ≡ x, then there is (x : A) ∈ Γ with T ≡ A; (v) if t ≡ λx A .u,

Results concerning pedagogy

(e-env2)

Γ ⊢ 2e σ A : κ ⊢ 2e [ ] a : σ(A) x ∈ dom(Γ) Γ, x : A wf 2e σ::(x → a) From Γ ⊢ 2e σ A : κ we know that Γ wf 2e σ is a strict sub-derivation (prop. 3), hence by induction hypothesis, with Γ := y 1 : B 1 , . . . , y n : B n , we have ⊢ 2e [ ] σ(y i ) : σ(B i ) are strict sub-derivations of Γ ⊢ 2e σ A : κ.
The second premise allows us to conclude for x.

Lemma 17 If Γ ⊢ 2e σ C : κ, then there is a term t such that ⊢ 2e [ ] t : σ(C).
Proof by structural induction on the derivation. The only rules to consider are (e-ax), (e-prod) and (e-var) (lem. 15), and only the (e-var) case is non-trivial:

(e-var)

Γ, x : Prop, Γ ′ wf 2e σ Γ, x : Prop, Γ ′ ⊢ 2e σ x : Prop By the Poincaré criterion (thm. 16) applied to the premise, ⊢ 2e [ ] σ(x) : Prop is a strict sub-derivation. Hence by induction hypothesis there is a term t such that ⊢ 2e [ ] t : σ(x).

Lemma 18 (weakening)

If Γ ⊢ 2e σ w : C, Γ ′ wf 2e σ ′ , Γ ⊆ Γ ′ and σ ⊆ σ ′ , then Γ ′ ⊢ 2e σ ′ w : C.
Proof by structural induction on the derivation:

(e-abs) Γ, x : A ⊢ 2e σ::(x → a) u : B : Prop Γ ⊢ 2e σ λx A .u : ∀x A .B Let Γ ′ wf 2e σ ′ with Γ ⊆ Γ ′ and σ ⊆ σ ′ .
From one premise we have that Γ ⊢ 2e σ A : κ is a sub-derivation (prop. 3, 4), on which we can apply induction hypothesis to get Γ ′ ⊢ 2e σ ′ A : κ and since also ⊢ (e-prod) Just as for the (e-abs) rule to be able to apply induction hypothesis.

Lemma 19 If ⊢ 2e [ ] w : C : κ and z ∈ dom(Γ) then: (i) if Γ[z ← w ] wf 2e σ then z : C, Γ wf 2e (z → w)::σ ; (ii) if Γ[z ← w ] ⊢ 2e σ D[z ← w ] : κ ′ then z : C, Γ ⊢ 2e (z → w)::σ D : κ ′ .
Proof by structural induction on the derivation: (i)

(e-env1) From ⊢ 2e [ ] w : C : κ by (e-env 2 ) we have z : C wf 2e [(z → w)]
.

(e-env2) (ii) The case where D ≡ z can be processed in the following way: (z → w)::σ z : C. Also C ≡ κ ′ by type uniqueness (prop. 5) since:

Γ[z ← w ] ⊢ 2e σ A[z ← w ] : κ ′′ ⊢ 2e [ ] a : σ(A[z ← w ]) x ∈ dom(Γ[z ← w ]) Γ[z ← w ], x : A[z ← w ] wf
From Γ[z ← w ] ⊢ 2e σ D[z ← w ] : κ ′ it follows that Γ[z ← w ] wf 2e σ is a strict sub-derivation (prop.
• we have Γ[z ← w ] ⊢ 2e
σ w : κ ′ by hypothesis;

• from ⊢ 2e [ ] w : C we get Γ[z ← w ] ⊢ 2e
σ w : C by weakening (lem. 18). Let us now deal with the cases where D ≡ z, we only need to consider the rules (e-ax), (e-var) and (e-prod) (lem. 15):

(e-ax) Γ[z ← w ] wf 2e σ Γ[z ← w ] ⊢ 2e σ ⊤ : Prop with D[z ← w ] ≡ ⊤ and D ≡ z, hence D ≡ ⊤.
By induction hypothesis z : C, Γ wf 2e (z → w)::σ and then using the (e-ax) rule we have z : C, Γ ⊢ 2e (z → w)::σ ⊤ : Prop. We do the same for Γ[z ← w ] ⊢ 2e σ Prop : Type.

(e-var)

Γ[z ← w ], x : κ ′ , Γ ′ [z ← w ] wf 2e σ::(x → t)::σ ′ Γ[z ← w ], x : κ ′ , Γ ′ [z ← w ] ⊢ 2e σ::(x → t)::σ ′ x : κ ′ with D[z ← w ] ≡ x and D ≡ z, hence D ≡ x.
The induction hypothesis gives z : C, Γ, x : κ ′ , Γ ′ wf 2e (z → w)::σ::(x → t)::σ ′ then the (e-var) rule finishes the proof.

(e-prod)

Γ[z ← w ], x : A[z ← w ] ⊢ 2e σ::a B[z ← w ] : Prop ⊢ 2e [ ] t : σ((∀x A .B)[z ← w ]) Γ[z ← w ] ⊢ 2e σ ∀x A[z←w ] .B[z ← w ] : Prop By induction hypothesis z : C, Γ, x : A ⊢

Theorem 20 (λ 2

e meets the converse of the Poincaré criterion)

If ⊢ 2e [ ] t 1 : A 1 : κ 1 . . . ⊢ 2e [ ] t n : A n [x 1 , . . . , x n-1 ← t 1 , .
. . , t n-1 ] : κ n (with the x i pairwise distinct), then

x 1 : A 1 , x 2 : A 2 , . . . , x n : A n wf 2e (x1 → t1)::(x2 → t2):: . . . ::(xn → tn)
Proof by induction on n:

By hypothesis ⊢ 2e [ ] A n [x 1 , . . . , x n-1 ← t 1 , . . . , t n-1 ] : κ n which can be rewritten to ⊢ 2e [ ] A n [x 1 , . . . , x n-2 ← t 1 , . . . , t n-2 ][x n-1 ← t n-1
] : κ n since the x i are pairwise distinct and the t i are closed (lem. 13). We can then generalize over x n-1 (lem. [START_REF] Griss | Negationless intuitionistic mathematics IVa, IVb[END_REF]) since we have

⊢ 2e [ ] t n-1 : A n-1 [x 1 , . . . , x n-2 ← t 1 , . . . , t n-2 ] : κ n-1 in order to obtain x n-1 : A n-1 [x 1 , .., x n-2 ← t 1 , .., t n-2 ] ⊢ 2e (xn-1 → tn-1) A n [x 1 , .., x n-2 ← t 1 , .., t n-2 ] : κ n .
Proceeding the same, we generalize over the variables from x n-2 to x 1 to finally obtain

x 1 : A 1 , . . . , x n-1 : A n-1 ⊢ 2e (x1 → t1):: . . . ::(xn-1 → tn-1) A n : κ n . Now since also ⊢ 2e [ ] t n : A n [x 1 , . . . , x n-1 ← t 1 , . . . , t n-1 ]
then by (e-env 2 ) we finally get the result.

Lemma 21

(i) If z : C, Γ wf 2e (z → c)::σ then Γ[z ← c ] wf 2e σ ; (ii) If z : C, Γ ⊢ 2e (z → c)::σ w : D then Γ[z ← c ] ⊢ 2e σ w[z ← c ] : D[z ← c ].
Proof by structural induction on the derivation:

z : C, Γ ⊢ 2e (z → c)::σ u : ∀x A .B z : C, Γ ⊢ 2e (z → c)::σ v : A z : C, Γ ⊢ 2e (z → c)::σ u v : B[x ← v ] By induction hypothesis, both Γ[z ← c ] ⊢ 2e σ u[z ← c ] : ∀x A[z←c ] .B[z ← c ] and Γ[z ← c ] ⊢ 2e σ v[z ← c ] : A[z ← c ].
Hence applying the (e-app) rule on those we have Γ

[z ← c ] ⊢ 2e σ u[z ← c ] v[z ← c ] : B[z ← c ][x ← v[z ← c ] ], but since c is closed (lem. 13) then B[z ← c ][x ← v[z ← c ] ] ≡ B[x ← v ][z ← c ]. (e-prod) z : C, Γ, x : A ⊢ 2e (z → c)::σ::(x → a) B : Prop ⊢ 2e [ ] t : (z → c)::σ(∀x A .B) z : C, Γ ⊢ 2e (z → c)::σ ∀x A .B : Prop By induction hypothesis Γ[z ← c ], x : A[z ← c ] ⊢ 2e σ::(x → a) B[z ← c ] : Prop. And (z → c)::σ(∀x A .B) ≡ σ((∀x A .B)[z ← c ]) since c is closed and z ∈ dom(σ) (lem. 13). Therefore ⊢ 2e [ ] t : σ(∀x A[z←c ] .B[z ← c ]
) and the (e-prod) rule allows us to conclude.

Lemma 22 If Γ ⊢ 2e σ w : C then ⊢ 2e [ ] σ(w) : σ(C).
Proof by induction on the size of the environment: Let Γ := x 1 : A 1 , . . . , x n : A n and σ := (x 1 → t 1 ):: . . . ::(x n → t n ). We have

⊢ 2e [ ] w[x 1 ← t 1 ] . . . [x n ← t n ] : C[x 1 ← t 1 ] . . . [x n ← t n ]
after n substitutions of the motivations (lem. 21). And since the t i are closed and the x i are pairwise distinct (lem. 13) then w[

x 1 ← t 1 ] . . . [x n ← t n ] ≡ w[x 1 , . . . , x n ← t 1 , . . . , t n ] ≡ σ(w) and C[x 1 ← t 1 ] . . . [x n ← t n ] ≡ C[x 1 , . . . , x n ← t 1 , . . . , t n ] ≡ σ(C). Lemma 23 If Γ, z : C, Γ ′ ⊢ 2e σ w : D and z ∈ V(Γ ′ , w), then z ∈ V(D).
Proof immediate by structural induction on the derivation.

Lemma 24 (strengthening)

(i) If Γ, z : C, Γ ′ wf 2e σ::(z → c)::σ ′ and z ∈ V(Γ ′ ), then Γ, Γ ′ wf 2e σ::σ ′ ; (ii) If Γ, z : C, Γ ′ ⊢ 2e σ::(z → c)::σ ′ w : D and z ∈ V(Γ ′ , w), then Γ, Γ ′ ⊢ 2e σ::σ ′ w : D.
Proof by structural induction on the derivation, similar to [26, lem. 3.2.9]. The only non-immediate case is the following one:

(e-abs)

Γ, z : C, Γ ′ , x : A ⊢ 2e σ::(z → c)::σ ′ ::(x → a) u : B : Prop Γ, z : C, Γ ′ ⊢ 2e σ::(z → c)::σ ′ λx A .u : ∀x A .B with z ∈ V(Γ ′ , λx A .u).
We have z ∈ V(Γ ′ , A, u), therefore also z ∈ V(B) (lem. 23). We can then apply the induction hypothesis to get Γ, Γ ′ , x : A ⊢ 2e Proof Let Γ ≡ x 1 : A 1 , . . . , x n : A n and σ ≡ (x 1 → a 1 ):: . . . ::(x n → a n ). By the Poincaré criterion (thm. 16) we have the derivations

⊢ 2e [ ] a 1 : A 1 ⊢ 2e [ ] a 2 : A 2 [x 1 ← a 1 ] . . . ⊢ 2e [ ] a n : A n [x 1 , . . . , x n-1 ← a 1 , . . . , a n-1 ]
and since for all i x 1 :

A 1 , . . . , x i-1 : A i-1 ⊢ 2e σ<i A i : κ i (prop. 4) then by substitutions (lem. 22) ⊢ 2e [ ] A i [x 1 , . . . , x i-1 ← a 1 , . . . , a i-1 ] : κ i .
The result then follows by applying the converse of the Poincaré criterion (thm. 20) on:

⊢ 2e [ ] a 1 : A 1 : κ 1 . . . ⊢ 2e [ ] a n : A n [x 1 , . . . , x n-1 ← a 1 , . . . , a n-1 ] : κ n ⊢ 2e [ ] c : C[x 1 , . . . ,
Γ ⊢ 2e σ f i : C i → D i Γ ⊢ 2e σ g i : D i → C i and Γ ⊢ 2e σ C i : Prop Γ ⊢ 2e σ D i : Prop then there is a term w ′ such that Γ ⊢ 2e σ w ′ : E[z 1 , . . . , z n ← D 1 , . . . , D n ] : Prop.
Proof by induction on the raw term E (generalize [6, lem. 14]):

Let us first notice that if E ≡ z i , then w ′ := f i w suits. Now let us deal with the cases when E is different from all the z i . We proceed by case analysis on the last used rule producing Γ ⊢ 2e

σ E[z 1 , . . . , z n ← C 1 , . . . , C n ] : Prop, which limits the analysis to three rules (lem. 15):

(e-ax) In this case E ≡ ⊤ and then w ′ := w suits.

(e-var) In this case E ≡ y is a variable different from the z i and then w ′ := w suits. [START_REF] Colson | Pedagogical natural deduction systems: the propositional case[END_REF], we distinguish two cases depending on κ:

(e-prod) Let F [ z ← C ] abbreviates F [z 1 , . . . , z n ← C 1 , . . . , C n ]: Γ, x : A[ z ← C ] ⊢ 2e σ::(x → a) B[ z ← C ] : Prop ⊢ 2e [ ] t : σ(∀x A[ z← C ] .B[ z ← C ]) Γ ⊢ 2e σ ∀x A[ z← C ] .B[ z ← C ] : Prop Since Γ ⊢ 2e σ A[ z ← C ] : κ (prop. 3,
• κ ≡ Type: then A[ z ← C ] ≡ Prop (lem. 15). If A ≡ z i then Γ ⊢ 2e σ C i :
Type, which is not allowed by type uniqueness (prop. 5). Necessarily A ≡ z i for all i and then A ≡ Prop. The rule can then be rewritten in the following simpler way: Γ, x : Prop ⊢

⊢ 2e [ ] σ(f i ) : σ(C i ) → σ(D i ) ⊢ 2e [ ] σ(C i ) : Prop ⊢ 2e [ ] σ(g i ) : σ(D i ) → σ(C i ) ⊢ 2e [ ] σ(D i ) : Prop
and also (prop. 3, 8 and lem. 22):

⊢ 2e [ ] σ(y i ) : Prop ⊢ 2e [ ] λz σ(yi) .z : σ(y i ) → σ(y i )
we can then apply the induction hypothesis on A to build a term a ′ such that

⊢ 2e [ ] a ′ : A[ z, y ← σ( D), σ( y) ] : Prop, namely ⊢ 2e [ ] a ′ : σ(A[ z ← D ]) : Prop. And since Γ wf 2e σ (prop. 3), we then have Γ, x : A[ z ← D ] wf 2e σ::(x → a ′ ) (lem. 26).
Therefore by (e-var) we have Γ, 4, lem. 14, 15). Hence the induction hypothesis gives a term u such that Γ, x :

x : A[ z ← D ] ⊢ 2e σ::(x → a ′ ) x : A[ z ← D ] and also Γ, x : A[ z ← D ] ⊢ 2e σ::(x → a ′ ) A[ z ← D ] : Prop (prop.
A[ z ← D ] ⊢ 2e σ::(x → a ′ ) u : A[ z ← C ] : Prop.
By weakening (lem. 18) on the hypothesis and using the (e-app) rule we get Γ, x : ). Since the σ(y i ) and the σ ′ (y i ) are all closed (lem. 13), we then have terms f i and

A[ z ← D ] ⊢
g i such that ⊢ 2e [ ] f i : σ ′ (y i ) → σ(y i ) and ⊢ 2e [ ] g i : σ(y i ) → σ ′ (y i ) (lem. 28
). Hence replacing the equivalents (lem. 27) there is a term

t ′ such that ⊢ 2e [ ] t ′ : (∀x A .B)[y 1 , . . . , y m ← σ ′ (y 1 ), . . . , σ ′ (y m ) ], namely ⊢ 2e [ ] t ′ : σ ′ (∀x A .B).
We are then allowed to conclude using the (e-prod) rule. Proof by structural induction on the first derivation:

(e-env2) immediate by the induction hypothesis on the first premise followed by (eenv 2 ) and lem. 17.

(e-var) There are three cases depending on the position in the environment of the extracted variable: before y, being y or after y. They are solved as usual using the induction hypothesis, see [ (e-app) As previously, since the induction hypothesis applied to the two premises gives two substitutions ρ ′ and ρ ′′ potentially different, we chose one (lem. 29) and deduce the result by the rule (e-app). Proof by structural induction on the derivation followed by case analysis on the definition of β , similar to the one of [7, prop. 7] or [1, thm. 5.2.15]:

(e-abs) Γ, x : A ⊢ 2e σ::(x → a) u : B : Prop Γ ⊢ 2e
σ λx A .u : ∀x A .B A being in normal form (prop. 9), only the case u β u ′ can happen: it is trivially solved using the induction hypothesis on the first premise.

(e-app)

Γ ⊢ 2e σ u : ∀x A .B Γ ⊢ 2e σ v : A Γ ⊢ 2e σ u v : B[x ← v ]
There are three cases:

• u β u ′ : trivial using the induction hypothesis on the first premise and (e-app).

• v β v ′ : there are three more cases (prop. 6):

• A ≡ Type: impossible (prop. 6, 2);

• Γ ⊢ 2e σ A : Type: then A ≡ Prop (lem. 15) hence v is not reducible (prop. 9); • Γ ⊢ 2e σ A : Prop: then A ≡ Prop (lem. 14) and then x ∈ V(B) (prop. 8) hence we have

B[x ← v ′ ] ≡ B ≡ B[x ← v ],
and it is enough to apply the induction hypothesis on the second premise followed by (e-app).

• u ≡ λx C .w and u v β w[x ← v ]: generation (lem. 14) gives Γ, x : A ⊢ 2e σ w : B and by substitution (lem. 30) we have the result.

(e-prod) A term of type Prop is not reducible (prop. 9). Proof by structural induction on the derivation (similar to prop. 6): for the (e-abs) rule, the previous lemma 25 immediately gives us the result.

Theorem 33 (λ 2

e is a pseudo pedagogical sub-system of CC)

λ 2 e satisfies the following properties: (i) λ 2 e is a sub-system of CC; (ii) If Γ ⊢ 2e σ t : C and t β t ′ , then Γ ⊢ 2e σ t ′ : C. (iii) x 1 : A 1 , .., x n : A n wf 2e (x1 → t1)::..::(xn → tn) if and only if x 1 : A 1 , .., x n : A n wf c and

⊢ 2e [ ] t 1 : A 1 ⊢ 2e [ ] t 2 : A 2 [x 1 ← t 1 ] . . . ⊢ 2e [ ] t n : A n [x 1 , . . . , x n-1 ← t 1 , . . . , t n-1 ] Proof (i) λ 2
e is a sub-system of λ 2 (thm. 12), itself a sub-system of CC. (ii) It is exactly the statement of the theorem 31. (iii) ⇒ It is exactly the statement of the theorem 16.

⇐ From ⊢ 2e [ ] t i : A i [x 1 , . . . , x i-1 ←

Total motivations

In λ 2 e examples has to be maintained during the whole proof: all premisses of rules use the same motivation. But we have seen that motivations can be exchanged (lem. 29): if Γ ⊢ 2e σ w : C and Γ wf 2e σ ′ then Γ ⊢ 2e σ ′ w : C. Hence we relax this constraint in the system λ 2 t (fig. 4) and allow for different motivations to be used during sub-proofs. We then make the motivations implicit but still require them to completely exemplifies environments when needed. Leaving enhanced judgements leads us a step closer to a real pedagogical subsystem of CC (additional constants are maintained).

System definition

The following definitions of motivations of an environment or a type depend on the formal system λ 2 t (fig. 4). To solve the apparent circularity, we can break those definitions in two parts: first a convenient abbreviation needed for the definition of the system; and second an effective definition once the inference rules of the system have been stated.

Definition 34 (Motivation of an environment) A substitution σ motivates an environment Γ ≡ x

1 : A 1 , . . . , x n : A n , abbreviated σ mot Γ, if for all i ⊢ 2t σ(x i ) : σ(A i ).
Definition 35 (Motivation of a type) A substitution σ motivate a type C relatively to an environment Γ, abbreviated σ mot Γ C if (i) σ mot Γ and (ii) there is a term t such that ⊢ 2t t : σ(C).

Depending on the context, σ mot Γ will denote the derivations ⊢ 2t σ(x i ) : σ(A i ), or the fact that the environment Γ can be motivated by σ. The same applies for the σ mot Γ C notation too.

(t-env 1 ) [ ] wf 2t Γ ⊢ 2t A : κ x ∈ dom(Γ) (t-env 2 ) Γ, x : A wf 2t Γ wf 2t (t-ax) Γ ⊢ 2t o : ⊤ : Prop : Type Γ, x : A, Γ ′ wf 2t (t-var) Γ, x : A, Γ ′ ⊢ 2t x : A Γ, x : A ⊢ 2t u : B : Prop (t-abs) Γ ⊢ 2t λx A .u : ∀x A .B Γ ⊢ 2t u : ∀x A .B Γ ⊢ 2t v : A (t-app) Γ ⊢ 2t u v : B[x ← v ] Γ, x : A ⊢ 2t B : Prop σ mot Γ ∀x A .B (t-prod) Γ ⊢ 2t ∀x A .B : Prop Figure 4: Inference rules of λ 2 t .

Results

The properties 1, 3, 4 are still valid for λ 2 t .

Theorem 36 (λ 2 t is a subsystem of λ 2 ) (i) if Γ wf 2t then Γ wf 2 ;

(ii) if Γ ⊢ 2t w : C then Γ ⊢ 2 w : C.

Lemma 37 (see lem. 15)

(i) If Γ ⊢ 2t C : Type then C ≡ Prop and the last rule of the derivation is (t-ax);

(ii) If Γ ⊢ 2t C : Prop then the last rule of the derivation is (t-ax), (t-var) or (t-prod).

Lemma 38 (λ 2 e is a sub-system of λ 2 t ) For every substitution σ:

(i) if Γ wf 2e σ then Γ wf 2t ; (ii) if Γ ⊢ 2e σ w : C then Γ ⊢ 2t w : C.
Proof by structural induction on the derivation. Every cases but (e-prod) are immediate: since we forget the explicit motivation, the rules are the same (or more constrained in the case of e-env 2 ) in λ 2 e .

(e-prod)

Γ, x : A ⊢ Lemma 39 (λ 2 t is a sub-system of λ 2 e ) (i) if Γ wf 2t then there is a substitution σ such that Γ wf

2e σ ; (ii) if Γ ⊢ 2t w : C then there is a substitution σ such that Γ ⊢ 2e σ w : C.
Proof by structural induction on the derivation:

(t-env2) Γ ⊢ 2t A : κ x ∈ dom(Γ) Γ, x : A wf 2t
By induction hypothesis we have a substitution σ ′ such that Γ ⊢ 2e σ ′ A : κ, and then (lem. 17) there is a term a such that ⊢ 2e [ ] a : σ ′ (A). Hence by (e-env 2 ) we obtain the result with σ := σ ′ ::(x → a). is a sub-derivation on which we can apply (HI) to obtain ⊢ 2e [ ] t : σ(∀x A .B). Finally the (e-prod) rule gives the result.

Theorem 40 (λ 2 t is a pseudo pedagogical sub-system of CC) λ 2 t satisfies the following properties:

(i) λ 2 t is a sub-system of CC; (ii) If Γ ⊢ 2t t : C and t β t ′ then Γ ⊢ 2t t ′ : C. (iii) x 1 : A 1 , . . . , x n : A n wf
2t if and only if x 1 : A 1 , . . . , x n : A n wf c and there are terms t 1 , . . . , t n such that

⊢ 2t t 1 : A 1 ⊢ 2t t 2 : A 2 [x 1 ← t 1 ] . . . ⊢ 2t t n : A n [x 1 , . . . , x n-1 ← t 1 , . . . , t n-1 ] Proof (i) λ 2
t is a sub-system of λ 2 (thm. 36) itself a sub-system of CC. (ii) From Γ ⊢ 2t t : C we have a substitution σ such that Γ ⊢ 2e σ t : C (lem. 39) and since

t β t ′ , then Γ ⊢ 2e σ t ′ : C (thm. 33) hence Γ ⊢ 2t t ′ : C (lem. 38). (iii) ⇒ From x 1 : A 1 , . . . , x n : A n wf 2t we have x 1 : A 1 , . . . , x n : A n wf 2e σ (lem. 39), hence x 1 : A 1 , . . . , x n : A n wf c and ⊢ 2e [ ] σ(x i+1 ) : σ(A i+1 ) (thm. 33) and finally ⊢ 2t σ(x i+1 ) : σ(A i+1 ) (lem. 38).
⇐ Similarly we move back and forth from λ 2 t to λ 2 e (lem. 38, 39).

Partial motivations

In [START_REF] Colson | Investigations on a pedagogical calculus of constructions[END_REF] we designed CC r a subsystem of CC able to derive λA Prop .λx A .x of type ∀A Prop .A → A, those two terms acting as initial examples like the constants o and ⊤ do for λ 2 e and λ 2 t (and P-Prop 2 of [START_REF] Colson | Pedagogical second-order λ-calculus[END_REF]). In CC r the (c-prod) rule of CC is constrained such that every occurrences of the formed type ∀x A .B has to be inhabited. In λ 2 e and λ 2 t only one occurrence need to be inhabited, but it has lead us to use motivations dealing with all the possible variables of the type to be motivated, namely all the variables of the environments, making the motivations total. In order to recover this behaviour of CC r and remove the need for additional constants, we can make the motivations partial, that is allowing them to act on some variables of the environments.

System definition

As for λ 2 t the following definitions of partial motivation of an environment or a type refer to the formal system λ 2 p (fig. 5) and the apparent circularity can be circumvented in the same way.

Definition 41 (Application of a partial motivation)

The application of the substitution σ to the environment Γ, whose result is an environment abbreviated by σ(Γ), is recursively defined as:

σ([ ]) := [ ] σ(Γ, x : A) := σ(Γ) if x ∈ dom(σ) σ(Γ), x : σ(A) otherwise
Definition 42 (Partial motivation of an environment) A substitution σ partially motivates the environment Γ ≡ x

1 : A 1 , . . . , x n : A n , abbreviated σ mot Γ, if for all i x i ∈ dom(σ) ⇒ σ(Γ <i ) ⊢ 2p σ(x i ) : σ(A i ).
Definition 43 (Partial motivation of a type) A substitution σ partially motivates a type C relatively to an environment Γ, abbreviated σ mot Γ C if (i) σ mot Γ and (ii) there is a term t such that σ(Γ) ⊢ 2p t : σ(C).

Depending on the context, σ mot Γ will denote the previous derivations, or the fact that the environment Γ can be partially motivated by σ. The same applies for the σ mot Γ C notation.

Example 44 σ := [x 2 → t 2 , x 4 → t 4 ] partially motivates the type C relatively to Γ := x 1 : A 1 , . . . , x 5 : A 5 if:

(i) x 1 : A 1 ⊢ 2p t 2 : A 2 and x 1 : A 1 , x 3 : A 3 [x 2 ← t 2 ] ⊢ 2p t 4 : A 4 [x 2 ← t 2 ]; (ii) there is t such that x 1 : A 1 , x 3 : A 3 [x 2 ← t 2 ], x 5 : A 5 [x 2 , x 4 ← t 2 , t 4 ] ⊢ 2p t : σ(C).

Remark 45

When dom(Γ) ⊆ dom(σ) we have the total motivation definition of λ 2 t . When dom(σ) = ∅ the behaviour of CC r is recovered.

For every environment Γ, [ ] mot Γ holds. However, for a type C, we of course do not always have [ ] mot Γ C.

(p-env 1 ) [ ] wf 2p Γ ⊢ 2p A : κ x ∈ dom(Γ) (p-env 2 ) Γ, x : A wf 2p Γ wf 2p (p-ax) Γ ⊢ 2p Prop : Type Γ, x : A, Γ ′ wf 2p (p-var) Γ, x : A, Γ ′ ⊢ 2p x : A Γ, x : A ⊢ 2p u : B : Prop (p-abs) Γ ⊢ 2p λx A .u : ∀x A .B Γ ⊢ 2p u : ∀x A .B Γ ⊢ 2p v : A (p-app) Γ ⊢ 2p u v : B[x ← v ] Γ, x : A ⊢ 2p B : Prop σ mot Γ ∀x A .B (p-prod) Γ ⊢ 2p ∀x A .B : Prop

Results

In this section, we will identify the constants o and ⊤ of the previous systems λ Proof immediate by using an empty motivation whenever the (p-prod) rule is used (similar to the proof for CC r in [3, sec. 3.4]) .

Theorem 47 (λ 2 p is a subsystem of λ 2 ) (i) if Γ wf 2p then Γ wf 2 ; (ii) if Γ ⊢ 2p w : C then Γ ⊢ 2 w : C.
Proof immediate by structural induction on the derivation.

Lemma 48 (λ 2 t is a subsystem of λ 2 p ) (i) if Γ wf 2t then Γ wf 2p ; (ii) if Γ ⊢ 2t w : C then Γ ⊢ 2p w : C.
Proof immediate by structural induction on the derivation:

• the (t-ax) case is done in the previous lemma 46;

• for the (t-prod) case, applying the induction hypothesis on all the derivations of σ mot Γ ∀x A .B is enough to obtain σ mot Γ ∀x A .B and to conclude using (p-prod).

In order to prove the converse of the previous lemma, namely that λ 2 p is a subsystem of λ 2 t , we will need to complete partial motivation to make them total. Therefore there is a need to define the substitution resulting of the composition of two substitutions:

Definition 49 (Composition of substitutions) σ ⊙ ρ is the composition substitution of the two substitutions σ and ρ defined by:

σ ⊙ ρ := ρ σ ::σ\ dom(ρ)
where [ ] σ := [ ] ((y → v)::τ ) σ := (y → σ(v))::τ σ and σ\ dom(ρ) is σ where all (x → v) such that x ∈ dom(ρ) are removed.

Lemma 50 For every raw term t and substitutions σ and ρ we have

σ⊙ρ(t) ≡ σ(ρ(t)). Moreover dom(σ ⊙ ρ) = dom(σ) ∪ dom(ρ).
Proof immediate by induction on the raw term t.

Lemma 51 (λ 2 p is a subsystem of λ 2 t ) (i) if Γ wf 2p then Γ wf 2t ; (ii) if Γ ⊢ 2p w : C then Γ ⊢ 2t w : C.
Proof by structural induction on the derivation:

(p-prod)

⊢ 2p t 1 : A 1 ⊢ 2p t 2 : A 2 [x 1 ← t 1 ] . . . ⊢ 2p t n : A n [x 1 , . . . , x n-1 ← t 1 , . . . , t n-1 ]
Proof (i) holds since λ 2 p is a sub-system of λ 2 (thm. 47) itself a sub-system of CC. For (ii) and (iii) it is enough to notice that λ 2 t are λ 2 p equivalent (lem. 48, 51) in order to import the results of the former (thm. 40) into the later.

Let us emphasize that λ 2 p is a pedagogical sub-system of CC in the sense of the formal definition given at the beginning (def. 10).

Pedagogical system F λ 2

p is a pedagogical subsystem of CC, syntactically equivalent to the systems λ 2 e and λ 2 t (lem. [START_REF] Vredenduin | The logic of negationless mathematics[END_REF]39,48,51). In this section we link those systems with the second order pedagogical λ-calculus P-Prop 2 of [START_REF] Colson | Pedagogical second-order λ-calculus[END_REF]. First we recall the system P-Prop 2 , then we show that it is equivalent to λ 2 t . Definition 55 (Substitutions of P-Prop 2 ) A substitution of P-Prop 2 is an application from type variables to types. The application of a substitution σ to a type A, defined in the usual way, is noted σ • A. A constant substitution but in a finite number of points α 1 , . . . , α n , associated respectively to the types

System definition

⊢ pf σ • ∆ (P-Ax) ∆ ⊢ pf o : ⊤ x : F ∈ ∆ ⊢ pf σ • ∆ (P-Hyp) ∆ ⊢ pf x : F ∆, x : A ⊢ pf u : B (→ i ) ∆ ⊢ pf λx A .u : A→B ∆ ⊢ pf u : A→B ∆ ⊢ pf v : A (→e) ∆ ⊢ pf u v : B ∆ ⊢ pf u : B α ∈ V(∆) (∀ i ) ∆ ⊢ pf Λα.u : ∀α.B ∆ ⊢ pf u : ∀α.B ⊢ pf σ • V (P-∀e) ∆ ⊢ pf u V : [α ← V ] • B
V 1 , . . . , V n , is noted [α 1 , . . . , α n ← V 1 , . . . , V n ].
Definition 56 (Contexts of P-Prop 2 ) A context ∆ of P-Prop 2 is a finite set of couples x : A where x is a term variable and A a type. Moreover if x : A and x : B are into the set ∆ then A = B. The context {x 1 : A 1 , . . . , x n : A n } is abbreviated to x 1 : A 1 , . . . , x n : A n . The set of free variables of a context ∆ = x 1 : A 1 , . . . , x n : A n , noted V(∆), is defined the usual way as the union of the V(A i ).

The following definitions of motivation refer to the formal system P-Prop 2 (fig. 6):

Definition 57 (Motivations of P-Prop 2 ) A substitution σ of P-Prop 2 motivates a type A, noted ⊢ pf σ Remark 58 In P-Prop 2 , and unlike λ 2 t , substitutions and contexts are set based, terms and types are disjoint, and a motivated type is not necessarily closed. Also since types are not built into the system P-Prop 2 every rules introducing new types need to be constrained (see fig. 6). Lemma 63 (exchange in (t-app) As previously, depending on the type of x we have two cases:

Results

λ 2 t ) If y ∈ V(D) then: (i) If Γ, y : C, z : D, Γ ′ wf 2t then Γ, z : D, y : C, Γ ′ wf 2t ; (ii) If Γ, y : C, z : D, Γ ′ ⊢ 2t w : E then Γ, z : D, y : C, Γ ′ ⊢ 2t w : E.
[[∆]] ⊢ 2t [[u]] : [[A→B]] [[∆]] ⊢ 2t [[v]] : [[A]] [[∆]] ⊢ 2t [[u v]] : [[B]] [[∆]] ⊢ 2t [[u]] : [[∀x.B]] [[∆]] ⊢ 2t [[v]] : Prop [[∆]] ⊢ 2t [[u v]] : [[B]][x ← [[v]] ]
The induction hypothesis and the (→ e ) and (∀ e ) rules (respectively) solve them.

(t-prod) Once again, depending on the type of x we have to deal with two cases:

•

[[∆]], x : [[A]] ⊢ 2t [[B]] : Prop σ mot [[∆]] [[A→B]] [[∆]] ⊢ 2t [[A→B]] : Prop where ∆ ≡ y 1 : D 1 , . . . , y n : D n .
By the definition of σ mot

[[∆]] [[A→B]],
we have:

• terms t i such that ⊢ 2t t i : [[D i ]][ α ← E ]
where α are the free variables of the D i and then the E j are such that ⊢ 2t E j : Prop (prop. 8). We then have terms

E ′ j and t ′ i such that [[E ′ j ]] ≡ E j and [[t ′ i ]] ≡ t i (cor. 74). Therefore ⊢ 2t [[t ′ i ]] : [[D i ]][ α ← [[E ′ ]] ] namely ⊢ 2t [[t ′ i ]] : [[[ α ← E ′ ] • D i ]] (lem. 61). The induction hypothesis gives ⊢ pf t ′ i : [ α ← E ′ ] • D i namely ⊢ pf ρ • D i where ρ := [ α ← E ′ ]. • and a term u such that ⊢ 2t u : [[A→B]][ α ← E ] which by the same way leads us to ⊢ pf ρ • (A→B). • [[∆]], x : Prop ⊢ 2t [[B]] : Prop σ mot [[∆]] [[∀x.B]] [[∆]] ⊢ 2t [[∀x.

Type checking

In this section we show that for all the pedagogical type systems of second-order presented so far the so-called type-checking problem is not decidable. We use the fact that the type inhabitation problem for Prop 2 is not decidable. Prop 2 is P-Prop 2 without the constraints, also known as System F such as presented in [START_REF] Girard | Proofs and types[END_REF].

Definition 78 (Type inhabitation) For a given formal system, the type inhabitation problem is:

input: a context (or an environment) Γ, and a type A;

output: "true" if there is a term t such that Γ ⊢ ⋆ t : A, and "false" otherwise.

Property 79 The type inhabitation problem for Prop 2 can be reduced to the type inhabitation problem for P-Prop 2 : for every ∆ and A there is t such that ∆ ⊢ f t : A if and only if there is t ′ such that ∆ γ ⊢ pf t ′ : A γ , where γ is a translation from formulas of Prop 2 to formulas of P-Prop 2 .

Proof A (constructive) proof can be found in [START_REF] Colson | Pedagogical Second-order Propositional Calculi[END_REF] about formal systems corresponding to the type systems Prop 2 and P-Prop 2 . The translation γ , inspired by the A-translation of [START_REF] Friedman | Classically and intuitionistically provably recursive functions[END_REF], consists in replacing every occurrences of type variables α by α ∨ γ where γ is a fresh type variable.

Property 80 Type inhabitation for Prop 2 is undecidable.

Proof by Urzyczyn in [START_REF] Pawe L Urzyczyn | Inhabitation in typed lambda-calculi (a syntactic approach)[END_REF].

Lemma 81 Type inhabitation for P-Prop 2 is undecidable.

Proof by contradiction. Assume that type inhabitation for P-Prop 2 can be decided by an algorithm D: D(∆, A) = true if and only if there is a term t such that ∆ ⊢ pf t : A.

We can then build an algorithm D ′ able to decide the problem of type inhabitation for Prop 2 : D ′ (∆, A) := D(∆ γ , A γ ). Indeed:

D ′ (∆, A) = true iff D(∆ γ , A γ ) = true iff there is t ′ such that ∆ γ ⊢ pf t ′ : A γ iff there is t such that ∆ ⊢ f t : A (prop. 79)
But we noticed that the type inhabitation for Prop 2 is undecidable (prop. 80).

Definition 82 (Type checking) For a given type system, the problem of type checking is:

input: a context (or an environment) Γ, a term t and a type A;

output: "true" if there is a derivation of Γ ⊢ ⋆ t : A, and "false" otherwise.

Lemma 83 The type inhabitation problem for P-Prop ⇐ Conversely from ⊢ pf t ′ : ∀ α.∆→A using (∀ e ) we have ⊢ pf t ′ α : ∆→A since the α are motivable ⊤, and then by weakening we have ∆ ⊢ pf t ′ α : ∆→A and finally using (→ e ) we obtain ∆ ⊢ pf t ′ α ∆ : A, namely t := t ′ α ∆ fits. Weakening for P-Prop 2 has been proved in [6, prop. 21] if the introduced formula can be motivated: here the formulas of ∆ are all motivable by the trivial substitution τ since they appear as sub-formulas in ∀ α.∆→A (prop. 70).

Theorem 85 The type checking problem for λ 2 t is undecidable.

Proof by contradiction. Let us assume that the type checking problem for λ 2 t can be decided by an algorithm D: D(Γ, t, A) = true if and only if Γ ⊢ 2t t : A. We can then build an algorithm D ′ to decide the type inhabitation problem for P-Prop iff there is t such that ⊢ pf t : ∀ α.∆→A (lem. 83) iff there is t ′ such that ∆ ⊢ pf t ′ : A (lem. 84)

But the type inhabitation problem for P-Prop 2 is undecidable (lem. 81).

Corollary 86 The type checking problem for λ 2 p is undecidable.

Proof is an immediate consequence of the equivalence of λ 2 t and λ 2 p (lem. 38, 39).

Definition 87 (Type checking with explicit motivations)

For a given type system with explicit motivations, the type checking problem for explicit motivations is the following:

input: a context (or environment) Γ, a substitution σ, a term t and a type A;

output: "true" if there is a derivation of Γ ⊢ ⋆ σ t : A, and "false" otherwise.

Theorem 88 The type checking problem for λ 2 e is undecidable.

Proof by contradiction. Let us assume that the type checking problem for λ 2 e can be decided by an algorithm D: D(Γ, σ, t, A) = true if and only if Γ ⊢ 2e σ t : A. We can then build an algorithm D ′ to decide the type checking problem for λ 2 t :

D ′ (Γ,

Conclusion

In this paper, we have given an example of the formal definition of pedagogical subsystem of the Calculus of Constructions of [START_REF] Colson | Investigations on a pedagogical calculus of constructions[END_REF] that we called λ 2 p , corresponding precisely to the pedagogical second-order λ-calculus of Colson and Michel [START_REF] Colson | Pedagogical second-order λ-calculus[END_REF]. Moreover the formalism of CC used in the definition allows for an homogeneous description of various type systems. For instance the introduced constraints for the second-order necessarily need to be transferred to higher orders pedagogical calculi; conversely once a pedagogical Calculus of Constructions will be obtained, pedagogical versions of the λ-cube systems should appear by deletion of some rules and simplification of associated constraints. Furthermore a pedagogical Calculus of Constructions can open the study toward pedagogical pure type systems [START_REF] Barendregt | Lambda calculi with types, volume 2 of Handbook of Logic in Computer Science[END_REF]. Thus we believe the objective of giving a uniform formal handling of the study of formal pedagogy has been reached.

During the building of our system λ 2 p we uncovered a formalism making explicit into the judgements the needed motivations, λ 2 e . This kind of formalism seems to be natural for expressing pedagogical calculi. Also it allows to state more precise and intuitive meta-mathematical properties about these systems. However we have shown it does not carry enough useful information to consider an implementation, especially because the type-checking is still undecidable.

As a conclusion, we suggest a simple solution to this problem: let us annotate types with terms to ensure their motivability, just like the typed λ-calculus annotate pure λ-terms with types to ensure their normalization. As an example we give modified rules (env 2 ) and (prod) implementing this (term annotation is at the bottom of types):

Property 7 (i) If Γ ⊢ 2 C

 72 : Type then C ≡ Prop and the last used rule is (ax); (ii) If Γ ⊢ 2 C : Prop then the last used rule is (var) or (prod).

  2e

  σ o : ⊤ : Prop : Type Γ, x : A, Γ ′ wf 2e σ (e-var) Γ, x : A, Γ ′ ⊢ 2e σ x : A Γ, x : A ⊢ 2e σ::(x → a) u : B : Prop (e-abs)

2eσFigure 3 :

 3 Figure 3: Inference rules of λ 2 e .

  then there are B and a such that Γ, x : A ⊢ 2e σ::(x → a) u : B : Prop is a strict sub-derivation with T ≡ ∀x A .B; (vi) if t ≡ u v, then there are A and B such that Γ ⊢ 2 u : ∀x A .B and Γ ⊢ 2 v : A are strict sub-derivations with T ≡ B[x ← v ]; (vii) if t ≡ ∀x A .B, then there are a and t such that Γ, x : A ⊢ 2e σ::(x → a) B : Prop and ⊢ 2e [ ] t : σ(∀x A .B) are strict sub-derivations with T ≡ Prop. Lemma 15 (i) If Γ ⊢ 2e σ C : Type then C ≡ Prop and the last derivation rule is (e-ax); (ii) If Γ ⊢ 2e σ C : Prop then the last derivation rule is (e-ax) or (e-var) or (e-prod).

Theorem 16 (λ 2 e

 2 meets the Poincaré criterion) If x 1 : A 1 , . . . , x n : A n wf 2e σ , then for all i ⊢ 2e [ ] σ(x i ) : σ(A i ) are strict sub-derivations.

  2e [ ] a : σ(A) (thm. 16) hence ⊢ 2e [ ] a : σ ′ (A) then finally by the rule (e-env 2 ) we have Γ ′ , x : A wf 2e σ ′ ::(x → a) . The induction hypothesis applied on the premises gives Γ ′ , x : A ⊢ 2e σ ′ ::(x → a) u : B : Prop and the (e-abs) rule finishes the proof.

  2e

  σ::(x → a) By induction hypothesis z : C, Γ ⊢ 2e (z → w)::σ A : κ ′′ and also the second premise can be rewritten as ⊢ 2e [ ] a : (z → w)::σ(A) since w is closed and z ∈ dom(σ) (lem. 13), then by (e-env 2 ) we get the result.

  3), then by induction hypothesis z : C, Γ wf 2e (z → w)::σ and using the (e-var) rule z : C, Γ ⊢ 2e

  2e (z → w)::σ::(x → a) B : Prop, moreover the second premise can be rewritten to ⊢ 2e [ ] t : (z → w)::σ(∀x A .B) hence the result by (e-prod).

  (e-var) z : C, Γ wf 2e (z → c)::σ z : C, Γ ⊢ 2e (z → c)::σ z : C is the only non-trivial case. By induction hypothesis, we have Γ[z ← c ] wf 2e σ . And ⊢ 2e [ ] c : C by the Poincaré criterion (thm. 16), hence by weakening (lem. 18) we finally obtain Γ[z ← c ] ⊢ 2e σ c : C.

  σ::σ ′ ::(x → a) u : B : Prop and by (e-abs) the result. Lemma 25 If Γ, x : A ⊢ 2e σ::(x → a) u : B : Prop, then Γ ⊢ 2e σ λx A .u : ∀x A .B : Prop. Proof By (e-abs) on the hypotheses we have Γ ⊢ 2e σ λx A .u : ∀x A .B, so we obtain ⊢ 2e [ ] σ(λx A .u) : σ(∀x A .B) (lem. 22) which allows us to apply the (e-prod) and conclude. Lemma 26 If Γ wf 2e σ and ⊢ 2e [ ] c : σ(C) : κ with z ∈ dom(Γ), then Γ, z : C wf 2e σ::(z → c) .

2e σ :

 σ :(x → a) B[ z ← C ] : Prop ⊢ 2e [ ] t : σ(∀x Prop .B[ z ← C ]) Γ ⊢ 2e σ ∀x Prop .B[ z ← C ] : Prop Weakening (lem. 18) with Γ, x : Prop wf 2e σ::(x → a) (prop. 3) on the derivations Γ ⊢ 2e σ w : ∀x Prop .B[ z ← C ] : Prop, we get Γ, x : Prop ⊢ 2e σ::(x → a) w : ∀x Prop .B[ z ← C ] : Prop. Then using (e-var) and (e-app): Γ, x : Prop ⊢ 2e σ::(x → a) w x : B[ z ← C ]. Now since Γ, x : Prop ⊢ 2e σ::(x → a) B[ z ← C ] : Prop then by induction hypothesis there is a term u such that Γ, x : Prop ⊢ 2e σ::(x → a) u : B[ z ← D ] : Prop. Hence Γ ⊢ 2e σ λx Prop .u : ∀x Prop .B[ z ← D ] : Prop (lem. 25), namely w ′ := λx Prop .u suits. • κ ≡ Prop: then A[ z ← C ] ≡ Prop (lem. 14) and x ∈ V(B[ z ← C ]) (prop. 8). From the first premise, we get ⊢ 2e [ ] a : σ(A[ z ← C ]) : Prop (thm. 16 and lem. 22) which can be rewritten to ⊢ 2e [ ] a : A[ z, y ← σ( C), σ( y) ] : Prop with y denoting the free variables of A[ z ← C ]. Now since we have (lem. 22):

  2e σ::(x → a ′ ) w u : B[ z ← C ] and from the first premise Γ, x : A[ z ← C ] ⊢ 2e σ::(x → a) B[ z ← C ] : Prop, then by strengthening (lem. 24) we can remove x from the environment, and by weakening (lem. 18) with x : A[ z ← D ] we get Γ, x : A[ z ← D ] ⊢ 2e σ::(x → a ′ ) B[ z ← C ] : Prop. Hence by induction hypothesis we have a term v such that Γ, x : A[ z ← D ] ⊢ 2e σ::(x → a ′ ) v : B[ z ← D ] : Prop and finally Γ ⊢ 2e σ λx A[ z← D ] .v : A[ z ← D ] → B[ z ← D ] : Prop (lem. 25). Lemma 28 If Γ ⊢ 2e σ C : Prop, Γ ⊢ 2e σ D : Prop with C and D closed, then there are two terms f and g such that Γ ⊢ 2e σ f : C → D : Prop and Γ ⊢ 2e σ g : D → C : Prop. Proof Since C and D are closed, then by strengthening (lem. 24) ⊢ 2e [ ] C : Prop and ⊢ 2e [ ] D : Prop and there are terms u and v such that ⊢ 2e [ ] u : C : Prop and ⊢ 2e [ ] v : D : Prop (lem. 17). By (e-env 2 ) z : C wf 2e (z → u) and z : D wf 2e (z → v) . Weakening (lem. 18) then gives z : C ⊢ 2e (z → u) v : D : Prop and z : D ⊢ 2e (z → v) u : C : Prop. Simultaneous use of the (e-abs) and (e-prod) rules (lem. 25) gives ⊢ 2e [ ] λz C .v : C → D : Prop and ⊢ 2e [ ] λz D .u : D → C : Prop. Finally by weakening (lem. 18) with Γ wf 2e σ (prop. 3) we obtain Γ ⊢ 2e σ λz C .v : C → D : Prop and Γ ⊢ 2e σ λz D .u : D → C : Prop. Lemma 29 (motivations exchange) If Γ ⊢ 2e σ w : C and Γ wf 2e σ ′ , then Γ ⊢ 2e σ ′ w : C. Proof by structural induction on the derivation of Γ ⊢ 2e σ w : C: (e-abs) Γ, x : A ⊢ 2e σ::(x → a) u : B : Prop Γ ⊢ 2e σ λx A .u : ∀x A .B Since Γ ⊢ 2e σ A : κ is a strict sub-derivation (prop. 3, 4), then by induction hypothesis Γ ⊢ 2e σ ′ A : κ. Hence we get a ′ such that Γ, x : A wf 2e σ ′ ::(x → a ′ ) (lem. 17 and (e-env 2 )). Now we can apply the induction hypothesis on the premises followed by an application of the (e-abs) rule to obtain the result.

  (e-prod) Γ, x : A ⊢ 2e σ::(x → a) B : Prop ⊢ 2e [ ] t : σ(∀x A .B) Γ ⊢ 2e σ ∀x A .B : Prop As previously, we can start to show that Γ, x : A wf 2e σ ′ ::(x → a ′ ) for some a ′ . Hence by induction hypothesis Γ, x : A ⊢ 2e σ ′ ::(x → a ′ ) B : Prop. We can rewrite the second premise as ⊢ 2e [ ] t : (∀x A .B)[y 1 , . . . , y m ← σ(y 1 ), . . . , σ(y m ) ] where the y i are the free variables of ∀x A .B. Furthermore (y i : Prop) ∈ Γ (prop. 8), then also ⊢ 2e [ ] σ(y i ) : Prop and ⊢ 2e [ ] σ ′ (y i ) : Prop (thm. 16

Lemma 30 (

 30 substitution lemma) (i) If Γ, y : C, Γ ′ wf 2e σ::(y → c)::σ ′ and Γ ⊢ 2e σ w : C, then there is a substitution ρ such that Γ, Γ ′ [y ← w ] wf 2e σ::ρ ; (ii) If Γ, y : C, Γ ′ ⊢ 2e σ::(y → c)::σ ′ d : D and Γ ⊢ 2e σ w : C, then there is a substitution ρ such that Γ, Γ ′ [y ← w ] ⊢ 2e σ::ρ d[y ← w ] : D[y ← w ].

  (e-abs) Γ, y : C, Γ ′ , x : A ⊢ 2e σ::(y → c)::σ ′ ::(x → a) u : B : Prop Γ, y : C, Γ ′ ⊢ 2e σ::(y → c)::σ ′ λx A .u : ∀x A .B Induction hypothesis on the premises gives two substitutions ρ ′ and ρ ′′ such thatΓ, Γ ′ [y ← w ], x : A[y ← w ] ⊢ 2e σ::ρ ′ ::(x → a ′ ) u[y ← w ] : B[y ← w ] Γ, Γ ′ [y ← w ], x : A[y ← w ] ⊢2e σ::ρ ′′ ::(x → a ′′ ) B[y ← w ] : Prop And we can exchange the motivation of the second one (lem. 29 and prop. 3) to obtain Γ, Γ ′ [y ← w ], x : A[y ← w ] ⊢ 2e σ::ρ ′ ::(x → a ′ ) B[y ← w ] : Prop Finally we get the result by applying the rule (e-abs) with ρ := ρ ′ .

  (e-prod) Γ, y : C, Γ ′ , x : A ⊢ 2e σ::(y → c)::σ ′ ::(x → a) B : Prop ⊢ 2e [ ] t : σ::(y → c)::σ ′ (∀x A .B) Γ, y : C, Γ ′ ⊢ 2e σ::(y → c)::σ ′ ∀x A .B : Prop First, by induction hypothesis, we have a substitution ρ ′ and a term a ′ such that Γ, Γ ′ [y ← w ], x : A[y ← w ] ⊢ 2e σ::ρ ′ ::(x → a ′ ) B[y ← w ] : Prop And transferring the motivation to the conclusion (lem. 22) and the second premise ⊢ 2e [ ] t : σ::(y → c)::σ ′ (∀x A .B) : Prop ( * ) Second since all free variable z of ∀x A .B are of type Prop (prop. 8) then: • when z ≡ y: the Poincaré criterion (thm. 16) on the previous well-formed environments (prop. 3) gives us ⊢ 2e [ ] σ::(y → c)::σ ′ (z) : Prop and ⊢ 2e [ ] σ::ρ ′ (z) : Prop; • when z ≡ y: the Poincaré criterion (thm. 16) and the transfer of the motivation to the conclusion (lem. 22) gives us ⊢ 2e [ ] σ::(y → c)::σ ′ (z) : Prop and ⊢ 2e [ ] σ(w) : Prop. Since all those types are closed (prop. 1) they are equivalent (lem. 28), and we can then freely exchange them (lem. 27) in ( * ) to build a term t ′ such that ⊢ 2e [ ] t ′ : σ::(y → σ(w))::ρ ′ (∀x A .B) : Prop i.e. ⊢ 2e [ ] t ′ : σ::ρ ′ ((∀x A .B)[y ← w ]) : Prop which allows us to conclude using (e-prod). Theorem 31 (subject reduction) If Γ ⊢ 2e σ t : C and t β t ′ , then Γ ⊢ 2e σ t ′ : C.

Lemma 32 (

 32 type correctness, see prop. 6) If Γ ⊢ 2e σ w : C then C ≡ Type or there is κ such that Γ ⊢ 2e σ C : κ.

2e σ :

 σ :(x → a) B : Prop ⊢ 2e [ ] t : σ(∀x A .B) Γ ⊢ 2e σ ∀x A .B : Prop with Γ ≡ y 1 : D 1 , . . . , y n : D n . By the first premise we have the sub-derivation Γ wf 2e σ (prop. 3) and the Poincaré criterion (thm. 16) gives ⊢ 2e [ ] σ(y i ) : σ(D i ) as strict sub-derivations, on which we can apply induction hypothesis to obtain ⊢ 2t σ(y i ) : σ(D i ), namely σ mot Γ. Moreover, induction hypothesis applied on the second premise gives us ⊢ 2t t : σ(∀x A .B) and we then get σ mot Γ ∀x A .B. The induction hypothesis applied on the first premise and the (t-prod) rule allow us to conclude.

  (t-abs) Γ, x : A ⊢ 2t u : B : Prop Γ ⊢ 2t λx A .u : ∀x A .B By induction hypothesis we have Γ, x : A ⊢ 2e σ1::(x → a1) u : B for a substitution σ 1 and a term a 1 , and also Γ, x : A ⊢ 2e σ2::(x → a2) B : Prop for σ 2 and a 2 . Hence by exchange of motivations (prop. 3 and lem. 29) we also have Γ, x : A ⊢ 2e σ1::(x → a1) B : Prop and finally the result by (e-abs).

  (t-app) Performed as for (t-abs).

  (t-prod) Γ, x : A ⊢ 2t B : Prop σ mot Γ ∀x A .B Γ ⊢ 2t ∀x A .B : Prop In the following, (IH) will be the name of the induction hypothesis, which is applicable to every strict sub-derivation of Γ ⊢ 2t ∀x A .B : Prop. Let Γ ≡ y 1 : D 1 , . . . , y n : D n . First we show by induction on i that ∀i y 1 : D 1 , . . . , y i : D i wf 2e σ ≤i • i = 0: by (e-env 1 ) we have [ ] wf 2e [ ] . • Assume y 1 : D 1 , . . . , y i : D i wf 2e σ ≤i (IHi) By the definition of σ mot Γ ∀x A .B we have ⊢ 2t σ(y i+1 ) : σ(D i+1 ) as a subderivation, on which we can apply (IH) to obtain ⊢ 2e [ ] σ(y i+1 ) : σ(D i+1 ). Since y 1 : D 1 , . . . , y i : D i ⊢ 2t D i+1 : κ is a sub-derivation of the first premise (prop. 3, 4), using the induction hypothesis (IH) we can build a substitution ρ such that y 1 : D 1 , . . . , y i : D i ⊢ 2e ρ D i+1 : κ, hence by motivations exchange (lem. 29) using (IHi) y 1 : D 1 , . . . , y i : D i ⊢ 2e σ ≤i D i+1 : κ. We then transfer the motivation to the conclusion (lem. 22) to obtain ⊢ 2e [ ] σ ≤i (D i+1 ) : κ. Finally since y 1 : D 1 , . . . , y i : D i wf 2e σ ≤i (IHi) and ⊢ 2e [ ] σ(y i+1 ) : σ ≤i (D i+1 ) : κ, then y 1 : D 1 , . . . , y i : D i , y i+1 : D i+1 wf 2e σ ≤i+1 (lem. 26) which closes this sub-proof. Now, when i = n, we have Γ wf 2e σ . The induction hypothesis (IH) applied to the first premise gives ρ and a ′ such that Γ, x : A ⊢ 2e ρ::(x → a ′ ) B : Prop. Hence Γ ⊢ 2e ρ A : κ (prop. 3, 4), so Γ ⊢ 2e σ A : κ by exchange of motivations (lem. 29), and there is a such that ⊢ 2e [ ] a : σ(A) (lem. 17). Using (e-env 2 ) we have Γ, x : A wf 2e σ::(x → a) . By exchange of motivations (lem. 29) we then get Γ, x : A ⊢ 2e σ::(x → a) B : Prop. The definition of σ mot Γ ∀x A .B implies the existence of t such that ⊢ 2t t : σ(∀x A .B)

Figure 5 :

 5 Figure 5: Inference rules of λ 2 p .

2 e and λ 2 t

 2 to their definitions in λ 2 p , namely o := λA Prop .λx A .x and ⊤ := ∀A Prop .A → A. Lemma 46 We have the following derived rules: Γ wf 2p Γ ⊢ 2p o : ⊤ : Prop : Type

Figure 6 :

 6 Figure 6: Inference rules of P-Prop 2 .

Definition 59 (

 59 Translation from P-Prop 2 to λ 2 t ) Since y ∈ V(D) by strengthening (lem. 24) on the first premise we get Γ ⊢ 2e σ D : κ then ⊢ 2e [ ] d : σ(D) (lem. 22). Hence by (e-env 2 ) we have Γ, z : D wf 2e σ::(z → d) . From the first premise we deduce Γ ⊢ 2e σ C : κ (prop. 4), which we can weaken (lem. 18) to obtain a derivation of Γ, z : D ⊢ 2e σ::(z → d) C : κ. Since ⊢ 2e [ ] c : σ(C) (thm. 16) and z ∈ V(C) (lem. 13) then also ⊢ 2e [ ] c : σ::(z → d)(C), and by (e-env 2 ) we finally obtain the result Γ, z : D, y : C wf 2e σ::(z → d)::(y → c) .

2 :

 2 D ′ (∆, A) := D([ ], [[∀ α.∆→A]], Prop) with α the free variables of ∆ and A. Indeed: D ′ (∆, A) = true iff D([ ], [[∀ α.∆→A]], Prop) = true iff ⊢ 2t [[∀ α.∆→A]] : Prop

• A ≡σ

 A Type and t ≡ Prop:D ′ (Γ, t, A) = true iff D([ ], [ ], ∀Γ.⊤, Prop) = true iff there is σ Γ wf 2eσ iff there is σ Γ ⊢ 2e Prop : Type ((e-ax) and prop. 3) iff Γ ⊢ 2t Prop : Type (lem. 38, 39) • A ≡ Type and t ≡ Prop: D ′ (Γ, t, A) = false and Γ ⊢ 2t t : Type (lem. 15).

• A ≡

 A Prop and t ≡ Prop: D ′ (Γ, t, A) = false and Γ ⊢ 2t Prop : Prop (lem.[START_REF] Girard | Le lambda-calcul du second ordre[END_REF]

Γ

  σ ⊢A a : κ x ∈ dom(Γ)(env 2 ) Γ σ , x : A a wf Γ σ , x : A a ⊢B b : Prop ⊢t : σ(∀x Aa .B b ) (prod) Γ σ ⊢(∀x Aa .B b ) t : PropIn such a formalism, terms should contain the needed information to allow the rebuild of the derivation and then type-checking.

  Type: hence Γ ⊢ 2 ∀x A . Type : κ (prop. 6), which is impossible (prop. 2). (ii) (app) We have Γ ⊢ 2 ∀x A .B : κ (prop. 6) which has to be obtained by the (prod) rule, hence Γ, x : A ⊢ 2 B : Prop. From B[x ← v ] ≡ Prop we have two cases: Prop: the second premise is then Γ ⊢ 2 Prop : A obtained by the (ax) rule, hence A ≡ Type which is impossible (prop. 2); Prop: then Γ, x : A ⊢ 2 Prop : Prop which is impossible. If Γ ⊢ 2 w : C or Γ ⊢ 2 C : κ or Γ wf 2 where Γ ≡ x 1 : A 1 , . . . , x n : A n then C and the A i are in normal form. if Γ wf 2 or Γ ⊢ 2 C : κ with Γ ≡ x 1 : A 1 , . . . , x n : A n then λ does not appear in C nor in any A i , proved by structural induction on the derivation; • every reducible raw term u contains the symbol λ, proved by induction on the usual inductive definition of u β u ′ . CC ⋆ is a subsystem of CC: Γ wf ⋆ implies Γ wf c , and Γ ⊢ ⋆ t : C implies Γ ⊢ c t : C. (ii) CC ⋆ satisfies subject reduction: if Γ ⊢ ⋆ t : C and t β t ′ then Γ ⊢ ⋆ t ′ : C. (iii) CC ⋆ meets the Poincaré criterion and its converse: x 1 : A 1 , . . . , x n : A n wf ⋆ if and only if x 1 : A 1 , . . . , x n : A n wf c and there are terms t 1 , . . . , t n such that

	Property 9 Proof The proof can be split in two simple steps:
	Definition 10 (pedagogical subsystem of CC)
	CC ⋆ is a pedagogical subsystem of CC if:
	(i)
	Property 8 If Γ ⊢ 2 C : Prop then for all x ∈ V(C), (x : Prop) ∈ Γ.
	Proof by structural induction on the derivation: we only need to consider the rules
	(var) and (prod) (prop. 7).

• B ≡ x and v ≡ Type: which is impossible (prop. 2);

• B ≡ • B ≡ x and v ≡ • B ≡ •

  t 1 , . . . , t i-1 ] and since A i ≡ Type because x 1 : A 1 , . . . , x n : A n wf c and t i ≡ Type (prop. 2), thanks to type correctness (lem. 32) we have ⊢ 2e [ ] A i [x 1 , . . . , x i-1 ← t 1 , . . . , t i-1 ] : κ i and we can then apply the theorem 20 to obtain the result.

  Γ, x : A ⊢ 2p B : Prop σ mot Γ ∀x A .B Γ ⊢ 2p ∀x A .B : Prop with Γ ≡ y 1 : D 1 , . . . , y n : D n .By the definition of σ mot Γ ∀x A .B, we have a term t such that σ(Γ) ⊢ 2p t : σ(∀x A .B)We then have ρ ⊙ σ mot Γ ∀x A .B since:• if y i ∈ dom(σ), by the definition of σ mot Γ ∀x A .B we have σ(Γ <i ) ⊢ 2p σ(y i ) : σ(D i )is a sub-derivation, and then by induction hypothesis σ(Γ <i ) ⊢ 2t σ(y i ) : σ(D i ).Hence there is ρ ′ such that σ(Γ <i ) ⊢ if y i ∈ dom(σ) then y i ∈ dom(σ(Γ)), and then from ( * ) using the Poincaré criterion (thm. 16 and prop. 3) ⊢ 2e [ ] ρ(y i ) : ρ(σ(D i )), namely, since y i ∈ dom(σ), ⊢ 2e [ ] ρ(σ(y i )) : ρ(σ(D i )). Hence ⊢ 2t ρ ⊙ σ(y i ) : ρ ⊙ σ(D i ) (lem.38, 50). ⊢ 2p t : C and t β t ′ , then Γ ⊢ 2p t ′ : C. (iii) x 1 : A 1 , . . . , x n : A n wf 2p if and only if x 1 : A 1 , . . . , x n : A n wf c and there are terms t 1 , . . . , t n such that

	• finally from ( * ), transferring the motivation to the conclusion (lem. 22) we have
	⊢ 2e [ ] ρ(t) : ρ(σ(∀x A .B)). Hence ⊢ 2t ρ(t) : ρ ⊙ σ(∀x A .B) (lem. 38, 50).
	Thus the induction hypothesis applied to the first premise gives Γ, x : A ⊢ 2t B : Prop
	and the (t-prod) allows to conclude.
	Theorem 52 (λ 2 p is a pedagogical sub-system of CC)
	λ 2 p satisfies the following properties: (i) λ 2 p is a subsystem of CC;
	(ii) If Γ
	is a sub-derivation, and then by induction hypothesis σ(Γ) ⊢ 2t t : σ(∀x A .B). Hence
	there is a substitution ρ (lem. 39) such that
	σ(Γ) ⊢ 2e ρ t : σ(∀x A .B)	( * )
	2e ρ ′ σ(y i ) : σ(D i ) (lem. 39) and then by exchange
	of motivations (lem. 29 and prop. 3) σ(Γ <i ) ⊢ 2e ρ<i σ(y i ) : σ(D i ). Then transferring
	the motivation to the conclusion (lem. 22) ⊢ 2e [ ] ρ(σ(y i )) : ρ(σ(D i )) and then also
	⊢ 2t ρ ⊙ σ(y i ) : ρ ⊙ σ(D i ) (lem. 38, 50).

•

  Definition 53 (Types of P-Prop 2 ) Types of P-Prop 2 are built according to the following rules: (i) ⊤ is a type; (ii) types variables α, β, γ, . . . are types; (iii) if A and B are types then A→B is a type; (iv) if α is a type variable and A a type then ∀α.A is a type. The finite set of free variables of a type A, noted V(A), is defined in the usual way. A a type and t a term then λx A .t is a term; (iv) if α is a type variable and t a term then Λα.t is a term; (v) if t and u are terms then t u is a term; (vi) if t is a term and U a type then t U is a term.

	Definition 54 (Terms of P-Prop 2 ) Terms of P-Prop 2 are built according to the
	following rules: (i) o is a term; (ii) term variables x, y, z, . . . are terms; (iii) if x is a
	term variable,

  • A, if there is a term t such that ⊢ pf t : σ • A. By extension, a substitution σ motivate a context ∆ = x 1 : A 1 , . . . , x n : A n , noted ⊢ pf σ • ∆, if for all i we have ⊢ pf σ • A i .

  Lemma 64 If Γ ⊢ 2t w : C then we can split Γ in two environments Γ 1 and Γ 2 such that: (i) Γ is a permutation of Γ 1 , Γ 2 ; (ii) Γ 1 , Γ 2 ⊢ 2t w : C; (iii) for all y : D ∈ Γ 1 , D ≡ Prop; (iv) for all y : D ∈ Γ 2 , D ≡ Prop.

	Proof immediate (lem. 62) since λ 2 t and λ 2 e are equivalents (lem. 38, 39).

  Corollary 77 We can embed the second order propositional calculus Prop 2 and λ 2 in the calculi λ 2 e , λ 2 t and λ 2 p . Proof The next property 79 recalls an embedding from Prop 2 to P-Prop 2 , which is enough because we can embed P-Prop 2 in λ 2 t (thm. 76), λ 2 t being equivalent to λ 2 e and λ 2 p (lem. 38, 39, 48, 51). Also λ 2 and Prop 2 are two different formalizations of the same calculus (can be shown similarly as what we did for λ 2 t and P-Prop 2 ).

	Proof (lem. 71), and then [[∆]] ⊢ 2t [[w]] : [[C]] (lem. 72). ⇒ From ∆ ⊢ pf w : C, we build a derivation using only τ as motivation
	⇐ It is exactly the (iii) of lemma 75 above.

B]] : Prop Solved as previously. Theorem 76 ∆ ⊢ pf w : C if and only if [[∆]] ⊢ 2t [[w]] : [[C]].

  2 with an empty context can be reduced to the type checking problem for λ2 t with an empty context: for every type A there is t such that ⊢ pf t : A with A closed if and only if ⊢ 2t [[A]] : Prop. ⊢ 2t [[A]] : κ. But κ ≡ Type because otherwise [[A]] ≡ Prop (lem. 37) which is not possible by the definition of [[•]], hence κ ≡ Prop. ⇐ From ⊢ 2t [[A]] : Prop we can build a term a such that ⊢ 2t a : [[A]] (lem. 17, 38, 39). But a is the image of a term t by [[•]] (cor. 74), i.e. [[t]] ≡ a, hence ⊢ 2t [[t]] : [[A]] and finally ⊢ f t : A (thm. 76). 84 The type inhabitation problem for P-Prop 2 can be reduced to the type inhabitation problem for P-Prop 2 with an empty context: for every type A there is t such that ∆ ⊢ pf t : A if and only if there is t ′ such that ⊢ pf t ′ : ∀ α.∆→A, where ∀ α.∆→A is closed, α are the free variables of ∆ and A, and ∆→A denotes B 1 → . . . →B n →A with ∆ = {y 1 : B 1 , . . . , y n : B n }. t : A we have ⊢ pf λ∆.t : ∆→A using (→ i ) and then ⊢ pf Λ α.λ∆.t : ∀ α.∆→A using (∀ i ). So t ′ := Λ α.λ∆.t fits.

	Proof correctness (lem. 67) Lemma Proof ⇒ From ⊢ pf t : A we can deduce ⊢ 2t [[t]] : [[A]] (thm. 76), and by type ⇒ From ∆ ⊢

pf

  ], [ ], ∀Γ.⊤, Prop) if A ≡ Type and t ≡ Prop false if A ≡ Type and t ≡ Prop false if A ≡ Prop and t ≡ Prop D([ ], [ ], ∀Γ.∀z t .⊤, Prop) if A ≡ Prop and t ≡ Prop D([ ], [ ], λΓ.t, ∀Γ.A) otherwise with λΓ.A ≡ λy B1 1 . . . . .λy Bn n .A if Γ ≡ y 1 : B 1 , . . . , y n : B n , and similarly for ∀Γ.A. First we show that D([ ], [ ], ∀Γ.⊤, Prop) = true there is σ such that Γ wf 2e σ : ⇒ From ⊢ 2e [ ] ∀Γ.⊤ : Prop by generation (lem. 14) we obtain a substitution σ such that Γ ⊢ 2e σ ⊤ : κ, and finally (prop. 3) Γ wf 2e σ . ⇐ From Γ wf 2e σ using (e-ax) we have Γ ⊢ 2e σ o : ⊤ : Prop and then using (e-abs) and (e-prod) (lem. 25) ⊢ 2e [ ] λΓ.o : ∀Γ.⊤ : Prop, so D([ ], [ ], ∀Γ.⊤, Prop) = true. Now we can show that D ′ (Γ, t, A) = true iff Γ ⊢ 2t t : A:

		       	D([
	t, A) :=	      

  ′ (Γ, t, A) = true iff D([ ], [ ], λΓ.t, ∀Γ.A) = true iff ⊢ 2e [ ] λΓ.t : ∀Γ.A iff ⊢

	2e σ t : κ iff there is σ Γ ⊢ 2e σ t : Prop iff Γ ⊢ 2t t : Prop	(prop. 4, lem. 17, (e-env 2 )) (lem. 15) (lem. 38, 39)
	2e [ ] λΓ.t : ∀Γ.A : κ ′ iff ⊢ 2e [ ] λΓ.t : ∀Γ.A : Prop iff there is σ Γ ⊢ 2e σ t : A : Prop (lem. 14, 25) (lem. 32) (lem. 15) iff Γ ⊢ 2t t : A (lem. 38, 39)
	But the type checking problem for λ 2 t is undecidable (thm. 85).

• A ≡ Prop and t ≡ Prop: D ′ (Γ, t, A) = true iff D([ ], [ ], ∀Γ.∀z t .⊤, Prop) = true iff there are σ and w Γ, z : t wf 2e σ::(z → w)

iff there is σ Γ ⊢

• A ≡ κ: D

The well-formedness of environments Γ are formal judgements in CC written Γ wf .

Actually a stronger but non-constructive result concerning the preservation of programs that can be typed in the λµ-calculus of Parigot[START_REF] Parigot | λµ-calculus: An Algorithmic Interpretation of Classical Natural Deduction[END_REF] is present in[START_REF] Colson | Pedagogical second-order λ-calculus[END_REF].

As in[START_REF] Coquand | Metamathematical investigations of a calculus of constructions[END_REF], we assume De Bruijn indexes for bound variables and identifiers for free variables. So there is no need for α-conversion notion which is implicit.

(var) Γ, x : A, Γ ′ ⊢ 2 x : A Γ, x : A ⊢ 2 u : B : Prop (abs) Γ ⊢ 2 λx A .u : ∀x A .B Γ ⊢ 2 u : ∀x A .B Γ ⊢ 2 v : A (app) Γ ⊢ 2 u v : B[x ← v ] Γ, x : A ⊢ 2 B : Prop (prod) Γ ⊢ 2 ∀x A .B : PropFigure 2: Inference rules of λ 2 .

Proof Let Γ ≡ x 1 : A 1 , . . . , x n : A n . Since we have x 1 : A 1 , . . . , x i : A i ⊢ 2t A i+1 : κ (prop. 4): either κ ≡ Type and then A i+1 ≡ Prop (lem. 37); or κ ≡ Prop and then A i+1 ≡ Prop (lem. [START_REF] Girard | Le lambda-calcul du second ordre[END_REF]39). We can then put all the x i : A i where A i ≡ Prop in front of the environment (lem. 63) to constitute the Γ 1 part, the others constituting the Γ 2 part.

Remark 65 The elements of Γ 1 can appear in any order (lem. 63). The same holds also for Γ 2 since the A i only depend on the variables x j : Prop of Γ 1 (prop. 8 and lem. 39).

In the following, we will assume that the Γ 1 part of Γ in judgements Γ wf 2t or Γ ⊢ 2t w : C is implicit and then we will omit mentioning it. It can be reconstituted by putting in it every free variables of Γ, w and C. This is allowed by the properties of strengthening (lem. 24) and weakening (lem. 18) permitting us to add and remove elements of type Prop into Γ.

Those observations allow for a simpler definition of the translation of contexts of P-Prop 2 to environments of λ 2 t :

Definition 66 (Translation of a context of P-Prop 2 )

The translation of a context of P-Prop 2 to an environment of λ 2 t is defined by:

Proof immediate: it already holds for λ Definition 69 (Universal trivial motivation) The universal trivial motivation τ is the constant substitution associating ⊤ to every type variable.

Property 70 If ∆ ⊢ pf u : F then for every sub-type G of ∆, F we have ⊢ pf τ • G.

Proof in [6, thm. 19].

Lemma 71 If ∆ ⊢ pf u : F then there is a derivation of ∆ ⊢ pf u : F using only the trivial motivation τ in the premise of the rules (P-Ax), (P-Hyp) and (P-∀ e ).

Proof by structural induction on the derivation. For each of the three rules, every motivated formulas appear as a sub-type of the conclusion sequent. Thus they are also motivable by τ (prop. 70). We can then replace everywhere the premise

Lemma 72 If ∆ ⊢ pf w : C is a derivation using only the trivial motivation τ , then

Proof by structural induction on the derivation:

By hypothesis we have some terms t i such that ⊢ pf t i : τ

It is enough to apply the induction hypothesis to the two premises and use (t-app).

By induction hypothesis we have [[∆]] ⊢ 2t [[u]] : [[B]

]. There are two cases depending on whether α ∈ V (B) or not:

• α ∈ V(B): then α : Prop is in the hidden implicit part of the translated environment, and since it does not appear in V(∆) it does not appear either in V([[∆]]). We can then bubble up α : Prop in head position by successive permutations (lem. 63) to obtain

].

• α ∈ V(B): then α does not appear in the hidden part of the environment, and we can then add α : Prop to [[∆]] by weakening (lem. [START_REF] Griss | Negationless intuitionistic mathematics III[END_REF][START_REF] Vredenduin | The logic of negationless mathematics[END_REF]39) to obtain

In both cases we also have

] : Prop (lem. 68) and (t-abs) allows us to conclude.

As for (P-Ax) and (P-Hyp), from ⊢ pf τ Thus by weakening we also have

] : Prop and then using the (t-app) rule

Lemma 73 If Γ ⊢ 2t w : C and w ≡ Prop then there is a term or a type w

Proof by structural induction on the derivation:

) is a sub-derivation, we are faced to two cases:

• if κ ≡ Type, then A ≡ Prop (lem. 37) and in this case w ′ := Λx.u ′ fits;

• if κ ≡ Prop, then A ≡ Prop, and we can apply the induction hypothesis to get a term

The induction hypothesis gives us a term

We have to consider two cases in the sub-derivation Γ ⊢ 2t A : κ:

• if κ ≡ Type, then A ≡ Prop (lem. 37) and in this case w ′ := ∀x.B ′ fits;

• if κ ≡ Prop, then A ≡ Prop and then x ∈ V(B) (prop. 8), and the induction hypothesis gives us a term

) we can distinguish two cases:

• if κ ≡ Type, then D i+1 ≡ Prop (lem. 37);

• if κ ≡ Prop, then D i+1 ≡ Prop and the lemma 73 finishes the proof.

(ii) This is exactly the lemma 73.

(iii) We have three cases (lem. 67):

• C ≡ Type: then the implication is valid by vacuity; Lemma 75

Proof by structural induction on the derivation:

With ρ the empty substitution, we have trivially ⊢ pf ρ • ∅.

(t-env2)

There are two cases: Each case can be easily solved using the induction hypothesis on the first premise and the (→ i ) and (∀ i ) rules (respectively).