Dissertation, (1999)

Daniel Durante
Universidade Federal do Rio Grande do Norte
The main objective of this PhD Thesis is to present a method of obtaining strong normalization via natural ordinal, which is applicable to natural deduction systems and typed lambda calculus. The method includes (a) the definition of a numerical assignment that associates each derivation (or lambda term) to a natural number and (b) the proof that this assignment decreases with reductions of maximal formulas (or redex). Besides, because the numerical assignment used coincide with the length of a specific sequence of reduction - the worst reduction sequence - it is the lowest upper bound on the length of reduction sequences. The main commitment of the introduced method is that it is constructive and elementary, produced only through analyzing structural and combinatorial properties of derivations and lambda terms, without appeal to any sophisticated mathematical tool. Together with the exposition of the method, it is presented a comparative study of some articles in the literature that also get strong normalization by means we can identify with the natural ordinal methods. Among them we highlight Howard[1968], which performs an ordinal analysis of Godel’s Dialectica interpretation for intuitionistic first order arithmetic. We reveal a fact about this article not noted by the author himself: a syntactic proof of strong normalization theorem for the system of typified lambda calculus λ⊃ is a consequence of its results. This would be the first strong normalization proof in the literature. (written in Portuguese)
Keywords No keywords specified (fix it)
Categories (categorize this paper)
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Translate to english
Revision history

Download options

PhilArchive copy

 PhilArchive page | Other versions
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Modal Logic: An Introduction.Brian F. Chellas - 1980 - Cambridge University Press.
Mathematical Logic.Joseph R. Shoenfield - 1967 - Reading, Mass., Addison-Wesley Pub. Co..
Basic Proof Theory.A. S. Troelstra - 2000 - Cambridge University Press.
Natural Deduction: A Proof-Theoretical Study.Richmond Thomason - 1965 - Journal of Symbolic Logic 32 (2):255-256.

View all 26 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

An Elementary Proof of Strong Normalization for Intersection Types.Valentini Silvio - 2001 - Archive for Mathematical Logic 40 (7):475-488.
Light Affine Lambda Calculus and Polynomial Time Strong Normalization.Kazushige Terui - 2007 - Archive for Mathematical Logic 46 (3-4):253-280.
Atomic Polymorphism.Fernando Ferreira & Gilda Ferreira - 2013 - Journal of Symbolic Logic 78 (1):260-274.
A Strong Normalization Result for Classical Logic.Franco Barbanera & Stefano Berardi - 1995 - Annals of Pure and Applied Logic 76 (2):99-116.
Η- Conversions of IPC Implemented in Atomic F.Gilda Ferreira - 2017 - Logic Journal of the IGPL 25 (2):115-130.
Strong Normalization Results by Translation.René David & Karim Nour - 2010 - Annals of Pure and Applied Logic 161 (9):1171-1179.


Added to PP index

Total views
106 ( #90,503 of 2,385,586 )

Recent downloads (6 months)
23 ( #32,244 of 2,385,586 )

How can I increase my downloads?


My notes