×
David, René; Nour, Karim

A short proof of the strong normalization of classical natural deduction with disjunction. (English) Zbl 1066.03056

J. Symb. Log. 68, No. 4, 1277-1288 (2003).
The authors give “a direct proof of the strong normalization of the cut-elimination procedure for full propositional classical logic”. By ‘full classical’ they mean to take all connectives as primitives; and by ‘direct’: no reduction to known cases, or a frontal attack. The work is carried out in the format of the \(\lambda\mu\)-calculus, which is capable of referring to subterms directly. The main result is a proof of the strong normalization property: every reduction of a typed term terminates in a finite number of steps. The chief task is, of course, to show that this property is preserved under substituition. This is, indeed, a travail, as always. In carrying out the inductive proof, the authors enlarge the format, with an explanation of its necessity, This paper is written very clearly. The authors explain the context, aims, difficulties, strategies, etc. very well.
Reviewer: M. Yasuhara (Princeton)

Cited in 12 Documents

MSC:

03F05 Cut-elimination and normal-form theorems
03B05 Classical propositional logic
03B40 Combinatory logic and lambda calculus
68N18 Functional programming and lambda calculus

Keywords:

strong normalization; \(\lambda\mu\)-calculus; classical propositional logic
PDF BibTeX XML Cite
\textit{R. David} and \textit{K. Nour}, J. Symb. Log. 68, No. 4, 1277--1288 (2003; Zbl 1066.03056)
Full Text: DOI arXiv Euclid
  • logo of hbz
  • logo of WorldCat

References:

[1] Y. Andou Church-Rosser property of a simple reduction for full first-order classical natural deduction , Annals of Pure and Applied Logic , vol. 119 (2003), pp. 225–237. · Zbl 1016.03006
[2] F. Barbanera and S. Berardi A symmetric lambda calculus for “classical” program extraction , Proceedings of theoretical aspects of computer software, tacs ’94 (M. Hagiya and J.C. Mitchell, editors), Lecture Notes in Computer Science, vol. 789, Springer Verlag,1994, pp. 495–515. · Zbl 0942.03506
[3] E. T. Bittar Strong Normalisation Proofs for Cut-Elimination in Gentzen’s Sequent Calculi , Logic, algebra and computer science , vol. 46, Banach Center Publications,1999, pp. 179–225. · Zbl 0945.03083
[4] R. Constable and C. Murthy Finding computational content in classical proofs , Logical frameworks (G. Huet and G. Plotkin, editors), Cambridge University Press,1991, pp. 341–362. · Zbl 0754.03040
[5] R. David Normalization without reducibility , Annals of Pure and Applied Logic , vol. 107 (2001), pp. 121–130. · Zbl 0966.03015
[6] R. David and B. Guillaume Strong normalization of the typed \(\lambda_ws\) -calculus, Accepted in the CSL’03 colloquium.
[7] R. David and K. Nour A short proof of the strong normalization of the simply typed \(\l \m\) -calculus, Schedae Informaticae , vol. 12 (2003), · Zbl 1066.03056
[8] P. de Groote On the strong normalization of natural deduction with permutation-conversions , In 10th International Conference on Typed Lambda Calculi and Applications, TLCA ’95 , Lecture Notes in Computer Science, vol. 902, Springer Verlag,1995, pp. 201–205. · Zbl 0981.03027
[9] J.-Y. Girard A new constructive logic: classical logic , Mathematical Structures in Computer Science , vol. 1 (1991), pp. 255–296. · Zbl 0752.03027
[10] F. Joachimski and R. Matthes Short proofs of normalization for the simply-typed \(\lambda\) -calculus, permutative conversions and Gödel’s \(T\), Archive for Mathematical Logic , vol. 42 (2003), pp. 59–87. · Zbl 1025.03010
[11] J.-L. Krivine Classical logic, storage operators and 2nd order lambda-calculus , Annals of Pure and Applied Logic , vol. 68 (1994), pp. 53–78. · Zbl 0814.03009
[12] J.J. Levy Reductions correctes et optimales dans le lambda-calcul , Ph.D. thesis , Paris 7,1978.
[13] C.R. Murthy An evaluation semantics for classical proofs , Proceedings of the sixth annual IEEE symposium on logic in computer science,1991, pp. 96–107.
[14] K. Nour and K. Saber A semantical proof of the strong normalization theorem of full propositionnal classical natural deduction , Manuscript,2003.
[15] M. Parigot \(\lambda\mu\) -calculus: An algorithmic interpretation of classical natural deduction, Logic programming and automated reasoning ( St. Petersburg, 1992), Lecture Notes in Computer Science, vol. 624, Springer Verlag,1992, pp. 190–201. · Zbl 0925.03092
[16] D. Prawitz Natural deduction. A proof-theoretical study , Almqvist & Wiksell, Stockholm,1965. · Zbl 0173.00205
[17] D. Pym and E. Ritter On the semantics of classical disjunction , Journal of Pure and Applied Algebra , · Zbl 0981.03018
[18] N. J. Rehof and M. H. Sorensen The \(\lambda_\Delta\) -calculus, Proceedings of the international symposium on theoretical aspects of computer software, TACS ’94, Lecture Notes in Computer Science, vol. 789, Springer Verlag,1994, pp. 516–542. · Zbl 0942.03512
[19] E. Ritter, D. Pym, and L. Wallen On the intuitionistic force of classical search , Theoretical Computer Science , vol. 232 (2000), pp. 299–333. · Zbl 0952.03007
[20] J. Seldin On the proof theory of the intermediate logic MH , Journal of Symbolic Logic, vol. 51 (1986), no. 3, pp. 626–647. JSTOR: · Zbl 0639.03022
[21] G. Stalmarck Normalization theorems for full first order classical natural deduction , Journal of Symbolic Logic, vol. 56 (1991), no. 1, pp. 129–149. JSTOR: · Zbl 0735.03028
[22] D. van Daalen The language theory of automath , Ph.D. thesis , Eindhoven,1977. · Zbl 0352.68105
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.