, Assume without loss of generality that x does not appear in ?, nor in ?, ?, ?. By hypothesis (? ??xA) ? ?xA ? . If ? ??xA has a neutral cut-free proof then so does the sequent ? (?t/x)?A) Since ?(t/x)A = (?t/x)?A, we have (? ?((t/x)A)) ? A ?+(t ? /x) , which is equal to (t/x)A ? by Proposition 3.6. Otherwise, Definition 3.3 ensures that for any d, including t ?, A)) ? (t/x)A ?
, ? We first show that [?xA] is an upper bound of the set { Consider some term t, and a context ? ? Let ? be an assignment, ? be a substitution and ? a ?-adapted context. Assume without loss of generality that x does not appear in ? nor in ? Since ?(t/x)A = (?t/x)?A, we have by hypothesis (? (?t/x)(?A)) ? (t/x)A ? , which is equal to A ?+C i ] be an upper bound of { Let ? be an assignment and ? be a substitution, let ? be ?-adapted and assume, without loss of generality, We can choose c = [C], since we need the intersection of the upper bounds
, Then, since ?A is A-adapted, we have (?A ?C) ? C ? In particular, by Proposition 3.5, this sequent has a cut-free proof. Since x does not appear in C nor in ?, we can apply an ?-elimination rule between a proof of this sequent and the neutral cut-free proof of ? ?x?A, yielding a neutral cut-free proof of ? ?C. Hence (? ?C) ? C ? . Otherwise, by Definition 3.3, ? ?x?A is such that for some term t and element d, (? ? A) ? A ? , calling ? = ?
, Resolution in type theory, The Journal of Symbolic Logic, vol.34, issue.03, pp.414-432, 1971.
DOI : 10.1073/pnas.49.6.828
, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199
, Completeness and cut elimination in Church's intuitionistic theory of types, Journal of Logic and Computation, vol.15, pp.821-854, 2005.
, Truth Values Algebras and Proof Normalization, TYPES, pp.110-124, 2006.
DOI : 10.1007/978-3-540-74464-1_8
, Hol-lambda-sigma: an intentional first-order expression of higher-order logic, Mathematical Structures in Computer Science, vol.11, pp.1-25, 2001.
URL : https://hal.archives-ouvertes.fr/hal-01199524
, Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506
, A Simple Proof That Super-Consistency Implies Cut Elimination, RTA, pp.93-106, 2007.
DOI : 10.1007/978-3-540-73449-9_9
URL : https://hal.archives-ouvertes.fr/hal-00793008
, Abstract, The Journal of Symbolic Logic, vol.87, issue.04, pp.1289-1316, 2003.
DOI : 10.1007/BFb0037116
, Une extension de l'interprétation de Gödeì a l'analyse et son applicationàapplication`applicationà l'´ elimination des coupures dans l'analyse et la théorie des types, Proceedings of the Second Scandinavian Logic Symposium of Studies in Logic and the Foundations of Mathematics, pp.63-92, 1970.
, A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms, CSL, pp.169-183, 2008.
DOI : 10.1007/978-3-540-87531-4_14
, Completeness and Cut-elimination in the Intuitionistic Theory of Types--Part 2, Journal of Logic and Computation, vol.20, issue.2, pp.597-602, 2010.
DOI : 10.1093/logcom/exp076
URL : https://hal.archives-ouvertes.fr/hal-00917868
, A uniform semantic proof for cut-elimination and completeness of various first and higher order logics, Theoretical Computer Science, vol.281, issue.1-2, pp.471-498, 2002.
DOI : 10.1016/S0304-3975(02)00024-5
, Hauptsatz for higher order logic, The Journal of Symbolic Logic, vol.25, issue.03, pp.452-457, 1968.
DOI : 10.1090/S0002-9904-1966-11611-7
, Syntactical and semantical properties of simple type theory, The Journal of Symbolic Logic, vol.15, issue.04, pp.305-326, 1960.
DOI : 10.1007/BF01969991
, A nonconstructive proof of Gentzen's Hauptsatz for second order predicate logic, Bulletin of the American Mathematical Society, vol.72, issue.6, pp.980-983, 1966.
DOI : 10.1090/S0002-9904-1966-11611-7
, A proof of cut-elimination theorem in simple type-theory, Journal of the Mathematical Society of Japan, vol.19, issue.4, pp.399-410, 1967.
DOI : 10.2969/jmsj/01940399