N. Sergei, . Artemov-&-rosalie, and . Iemhoff, From de Jongh's theorem to intuitionistic logic of proofs, Dick de Jongh's Festschrift, pp.1-10, 2004.

J. Girard, P. Taylor, and Y. Lafont, Proofs and types. Cambridge tracts in theoretical computer science 7, 1989.

K. Gödel, Uber eine bisher noch nicht bentzte Erweiterung des finiten, Standpunktes. Dialectica, vol.12, pp.280-287, 1958.

R. Harrop, On disjunctions and existential statements in intuitionistic systems of logic, Mathematische Annalen, vol.132, issue.4, pp.347-361, 1956.

R. Iemhoff, A(nother) characterization of intuitionistic propositional logic, Annals of Pure and Applied Logic, vol.113, issue.1, pp.161-173, 2001.

R. Iemhoff, On the admissible rules of intuitionistic propositional logic, The Journal of Symbolic Logic, vol.66, issue.1, pp.281-294, 2001.

R. Iemhoff, Intermediate logics and Visser's rules, Notre Dame Journal of Formal Logic, vol.46, issue.1, pp.65-81, 2005.
DOI : 10.1305/ndjfl/1107220674

URL : https://doi.org/10.1305/ndjfl/1107220674

G. Kreisel and &. Putnam, Eine Unableitbarkeitsbeweismethode für den Intuitionistischen Aussagenkalkl, Archiv für mathematische Logik und Grundlagenforschung, vol.3, issue.3-4, pp.74-78, 1957.
DOI : 10.1007/bf01988049

. Paulrozì, Admissible and Derivable Rules in Intuitionistic Logic, Mathematical Structures in Computer Science, vol.3, issue.2, pp.129-136, 1993.

, Lectures on the Curry-Howard isomorphism. Studies in Logic and the Foundations of Mathematics 149, pp.8001-8002, 2006.

A. Visser, Substitutions of ? 0 1-sentences: explorations between intuitionistic propositional logic and intuitionistic arithmetic, vol.114, pp.227-271, 2002.

A. Lemma, Let ? ? V t : A for t in normal form, and t not ?neutral: ? Implication: if A = B ? C

, Disjunction: if A = B ?C, then t is an injection

, ? Conjunction: if A = B ?C

, ? (ax) t is a variable in ? ?. By definition of ? ? , the type of t is an implication

, ? (? I ) t is an abstraction, and we conclude

?. (?-e-)-and-t-=-s-u-with-?-?-s-:-b-?-c, Because t is in normal form, s cannot be an abstraction. By i.h., s is either a variable in ? ? or is ?neutral

, Then hop[x.inj i t | | y.s 1 | y.s 2 ]? = hop[x.inj i (t? ) | | y.s 1 ? | y.s 2 ? ] ? s i ? {? x.t? /y}. We conclude because s i ? {? x.t? /y} = (s i {? x.t/y})?. /y}. By renaming, x, y ? fv(? ), dom(? ). Then hop[x.W efq t | | y.s 1 | y.s 2 ]? = hop[x.W efq t? | | y.s 1 ? | y.s 2 ? ] for some SN context W. We have hop, ? hop[x.inj i t | | y.s 1 | y.s 2 ] ? s i {? x.t/y}. By renaming, x, y ? fv(? ), dom(? )

B. Lemma, If ? t : A and ? ? ?, then t? ? A

, Let us now proceed by cases on the rules of inference: (? I ) Assume that for all ? ? ?, x : A, t? ? B; we need to prove that for all ? ? ?, (? x.t)? ? A ? B. Let ? ? ?, and by renaming x ? dom(? ) ? fv(? ). Then (? x.t)? = ? x.t?. By Definition B.5(2), ? x.t? ? A ? B iff for all s ? A, t? {s/x} ? B, Proof. By induction on the type derivation. The base case is the axiom, and instantiated variables belong to the corresponding denotations by the definition of ?

, Note that (t s)? = (t? )(s? ). By i.h. t? ? A ? B, and therefore by Definition B.5(2), either:-t? SN n ? Ne: then (t? )(s? ) ? * SN n(s? ) since s? ? SN (by i.h. and Lemma B.4(1)) Note that n(s? ) is neutral, and we conclude by Lemma B.4(2) and Lemma B, vol.4

(. , By the hypothesis, for every ? ? ?, t? ? ?. We need to prove that (efq t)? ? A. By Lemma B.4(1) t? ? SN, and since (efq t)? = efq (t? ), (efq t)? is a neutral term, Conclude by Lemma B, vol.4, issue.2

, A 2 : we need to prove that for every ? ? ?, <t 1 ,t 2 >? ? A 1 ? A 2. Since <t, s>? = <t? , s? >, the claim follows from Definition B.5(3) and the i, (? I ) Let ? t 1 : A 1 and ? t, vol.2

(. Let and ?. , s? ? A 1 ? A 2 for every ? ? ?. We need to prove that (proj 1 s)? ? A 1 and (proj 2 s)? ? A 2 for every ? ? ?. There are two cases:-s? SN n ? Ne: then proj i (s? ) SN proj i n and we conclude by Lemma B.4(2) and Lemma B.4(3) because that term is neutral.-u? SN <t 1 ,t 2 > for some t 1 ? A 1 and t 2 ? A 2 : therefore proj i (u? ) ? * SN proj i <t 1

(. , Let ? t : A, and by i.h. t? ? A for every ? ? ?. We show that also (inj 1 t)? ? A ? B for every ? ? ?. Note that (inj 1 t)? = inj 1 (t? ), and conclude by i

(. , This case is just a simplified version of the following argument for the Harrop rule