A proof of normalization for a classical system of Peano Arithmetic formulated in natural deduction is given. The classical rule of the system is the rule for indirect proof restricted to atomic formulas. This rule does not, due to the restriction, interfere with the standard detour conversions. The convertible detours, numerical inductions and instances of indirect proof concluding falsity are reduced in a way that decreases a vector assigned to the derivation. By interpreting the expressions of the vectors as ordinals (...) each derivation is assigned an ordinal less than ɛ0. The vector assignment, which proves termination of the procedure, originates in a normalization proof for Gödel’s T by Howard. (shrink)

We prove the strong normalization of full classical natural deduction by using a translation into the simply typed λμ-calculus. We also extend Mendler’s result on recursive equations to this system.

In the present paper, we prove the normalization theorem and the consistency of the first-order classical logic with disjunctive syllogism. First, we propose the natural deduction system SCD for classical propositional logic having rules for conjunction, implication, negation, and disjunction. The rules for disjunctive syllogism are regarded as the rules for disjunction. After we prove the normalization theorem and the consistency of SCD, we extend SCD to the system SPCD for the first-order classical logic with disjunctive syllogism. It can be (...) shown that SPCD is conservative extension to SCD. Then, the normalization theorem and the consistency of SPCD are given. (shrink)

We extend Barbanera and Berardi's symmetric lambda calculus [2] to second-order classical propositional logic and prove its strong normalization.

A major problem for interpersonal aggregation is how to compare utility across individuals; a major problem for decision-making under normative uncertainty is the formally analogous problem of how to compare choice-worthiness across theories. We introduce and study a class of methods, which we call statistical normalization methods, for making interpersonal comparisons of utility and intertheoretic comparisons of choice-worthiness. We argue against the statistical normalization methods that have been proposed in the literature. We argue, instead, in favor of normalization of variance: (...) we claim that this is the account that most plausibly gives all individuals or theories ‘equal say’. To this end, we provide two proofs that variance normalization has desirable properties that all other normalization methods lack, though we also show how different assumptions could lead one to axiomatize alternative statistical normalization methods. (shrink)

In this paper, we explore the 2008 financial crisis in Iceland through the lens of Donaldson’s concept of normalization of questionable behavior. We study the report published by the Special Investigation Commission, an investigation initiated by the Icelandic Parliament near the end of 2008. The report provides a detailed and systematic account of the processes leading up to the crisis. Our aim is to determine the extent to which the behaviors of professionals in the Icelandic financial sector can be explained (...) as a gradual fading of moral concerns to the point that they perceived the sale of high-risk products to unassuming customers for their own short-term benefit to be morally unproblematic. In doing so, we consider both character and circumstance explanations of moral misbehavior. We expand on Donaldson’s initial description of normalization of questionable behavior by applying the concept of moral neutralization, which is defined by criminologists Sykes and Matza as the process of convincing oneself that an option that initially conflicted with one’s own moral beliefs is actually morally acceptable. We find indications that individuals in the Icelandic financial sector did engage in moral neutralization in their attempts to frame their own actions in an acceptable light. In our study, we identify one way of neutralizing away moral dissonance not captured in the original theoretical framework. Icelandic bankers justified their behavior by claiming that they did not break any relevant rules or regulations when they engaged in what were later labeled questionable activities. Our name for this kind of justification is claim of having breached no rule. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Normalization and the Welfare StateLadelle McWhorterIn Racism and Sexual Oppression in Anglo-America, I argued that as race was absorbed into biology in the nineteenth century, it was recast from a morphological typology to a function of physiological and evolutionary development (McWhorter 2009b). Racial difference became a sign of developmental difference. Racial groups represented stages of human evolution, and raced individuals were to be disciplined and managed in accordance with (...) developmental norms.Twentieth-century race was therefore a category and tool of normalization; to be raced was to be located at a particular point along a developmental curve. Some races were thought to be more or less arrested in their development, while others were merely retarded, and theorists disagreed at times about which were which. But they all agreed that the most highly developed race was the Nordic or the Anglo-Saxon. Anglo-Saxons were the norm for modern human beings— anatomically, physiologically, intellectually, and morally. There were other white races whose status was debated (Mediterraneans and Ashkenazi Jews, for example), and there were disputes over the evolutionary status of Chinese, Hindus, and Mexicans. But most theorists agreed that at the very bottom of the developmental scale we should place Celts, Negroes, and American Indians. These peoples were savages, primitives. They should be trained to the extent possible to contribute to the society that had already superseded them, but their proper destiny was to pass away into extinction as humanity advanced.These evolutionary stragglers, along with the evolutionary throwbacks that appeared sometimes among whites, were considered dangerous for two main reasons. First, a great many of them were expensive. They were shiftless, often incompetent, and frequently lawless. Because of them, it was necessary to [End Page 39] maintain police forces, prisons, poorhouses, and asylums. They were a drain on the economic advance of society, which affected its educational and technological advance and ultimately its evolutionary advance as well. Second, because they had primitive sexual urges unrestrained by reason as well as heritable defects and diseases, they threatened the bloodlines of more advanced human beings. In short, they posed a risk for the ongoing evolutionary advancement of the entire Human Race. To protect the Race, it was necessary to contain these primitives, savages, and throwbacks and to reduce their numbers through careful management of their sexuality. This, I argued in the book, was racism’s cutting edge in the early twentieth century.Since publishing the book, I have done some work on the changes in practices of racism in the wake of the Biological Synthesis—that is, the unification of biology and genetics that occurred in the 1930s through the efforts of renowned scientists such as Theodosius Dobzhansky and Ernst Mayr (McWhorter 2010a, 2010b, 2010c). As I discussed in that work, by 1950, evolutionary biology was less a study of species development than it was a study of the effects of evolutionary forces acting on and within populations. Correlatively, racial practices shifted toward management of statistically delineated populations or ethnic groups. Theorists and policymakers recognized that not all members of a given population have the same genes, meaning that old-style racism (which assumed, for example, that all Negroes were stupid) was false; some Negroes might be quite brilliant, in fact. It was not The Negro who was stupid but the population of Negroes in the aggregate that was measurably stupider than the population of Anglo-Saxons. Accordingly, normalization now occurred at the level of the population. Disciplinary practices designed for cultivating the capacities of groups of individuals were altered or replaced to focus on groups as groups, as aggregates. The point was to shift the statistical norm of the population rather than to alter the bodies or behavior of each and every individual. I have argued elsewhere (McWhorter 2009a, 5) that this merger of disciplinary normalization and population management constitutes the full flowering of what Foucault calls biopower (Foucault 1978, 140).When Lisa Guenther invited me to speak at the plenary on “Re-thinking Whiteness” that took place at the fifth annual meeting of philoSOPHIA at Vanderbilt University, she explained that although many presenters offer polished papers, it has been a... (shrink)

Children who grow up with a life‐threatening illness live and face death in a way that is foreign to those of us who have reached adulthood in relative health. The experiences that form their identities create a range of knowledge, and processes for acquiring that knowledge, quite apart from the mainstream. In the pace of its acquisition, and the depth of its content, this knowledge is hard for the rest of us to comprehend. Indeed, the primary symptom of this alternate (...) cognizance is that it sets these children apart from their families, peers, and greater communities. The child as a whole is marginalized in interpersonal relations by essentializing the child as the illness. The experience of the illness itself further isolates the child.Through firsthand observation, we find that the Hole in the Wall Gang summer camps provide a nearly unique environment for the normalization of this alternate cognizance. At camp, all those things that set them apart from the rest of the world mark them as normal members of a society. Other children share their physical qualities, have similar experiences and immediately understand their perspective on life. Small adjustments to social and physical environments have a lasting effect. A warm pool to swim in, a caring touch, an open smile—the children take the memory of these with them when they leave. They begin to understand that they are a desired part of a large and varied community. A new definition of normal is created and they are included. (shrink)

The notion of normal proof theory, and yet it has been somewhat neglected by the systems of equational logic. The intention here is then to show the normalization procedure for the equational logic of the Labelled Natural Deduction system . With this we believe we are making a step towards filling a gap in the literature on equational logic. Besides presenting a normalization procedure for the LND equational fragment, we employ a new method to prove the normalization theorems for equational (...) logic: proof transformation by rewriting, based on a algebraic calculus on the 'rewrite reasons'. (shrink)

This article utilizes the Foucauldian concepts of biopower and normalization to give an analysis of the debate surrounding the controversial administration of the HPV vaccine to adolescents. My intention is not to solve the problem, rather to utilize a Foucauldian framework to bring various facets of the issue to light, specifically the way the vaccine contributes to strategies of power in reference to how young adults develop within relationships of power. To begin, the article provides an overview of the Foucauldian (...) concepts of biopower and normalization, including how these two strategies of power were present in the administration of the smallpox vaccine in the 19th century. Next, information about HPV and the history of the current controversy in the United States is presented. Lastly, the article presents an analysis of the strategies of biopower and normalization present in the debate on HPV, including an emphasis on how the vaccination is similar to, and different from, 19th century smallpox vaccination. It also explores the way that mechanisms of disease control affect and are affected by individual subjects, in this case, adolescents. (shrink)

Akama et al. [1] introduced a hierarchical classification of first-order formulas for a hierarchical prenex normal form theorem in semi-classical arithmetic. In this paper, we give a justification for the hierarchical classification in a general context of first-order theories. To this end, we first formalize the standard transformation procedure for prenex normalization. Then we show that the classes $$\textrm{E}_k$$ and $$\textrm{U}_k$$ introduced in [1] are exactly the classes induced by $$\Sigma _k$$ and $$\Pi _k$$ respectively via the transformation procedure in (...) any first-order theory. (shrink)

I propose that the emphasis on "authentic" norms in the ISCT literature does not encompass the possibility of community norms that facilitate and maintain corrupt behavior. To fill this gap, I build on the normalization of corruption literature to present a typology of community norms that distinguishes between authentic, behavioral, and aspirational norm types as well as between illegitimate, authentic norms and illegitimate, behavioral norms. By refining the terminology used to evaluate community norms, I propose that ISCT can be more (...) easily applied to cases of systemic corruption. (shrink)

In 2015 Dag Prawitz proposed an Ecumenical system where classical and intuitionistic logic could coexist in peace. The classical logician and the intuitionistic logician would share the universal quantifier, conjunction, negation and the constant for the absurd, but they would each have their own existential quantifier, disjunction and implication, with different meanings. Prawitz’ main idea is that these different meanings are given by a semantical framework that can be accepted by both parties. The aim of the present paper is [1] (...) to prove the normalization theorem for the propositional fragment NEp of Prawitz’ ecumenical system, and [2] to show that NEp is sound and complete with respect to a Kripke-style semantics for the language of NEp. (shrink)

In this article, we take the case of racism in contemporary Italy as a starting point for a discussion about moral responsibility for racism in cases where ignorance is involved. We focus on the issue of the normalization of racism and its contribution to different forms of ignorance to assess the extent to which these might potentially mitigate judgments of responsibility for racism, thereby grounding an Exculpatory Stance. After illustrating the phenomenon of the normalization of racism and offering an outline (...) of how the normalization of racism contributes to ignorance, we argue against the Exculpatory Stance by appealing to a socially situated variety of capacitarian approach to the epistemic condition of moral responsibility. This approach provides us with the tools to claim that the moral ignorance favored by the normalization of racism does not mitigate judgments of individual responsibility. Finally, we point out that the interdependence of individual responsibility and the social environment is such that, in addition to backward-looking individual responsibilities for racism, there are also forward-looking, both individual and shared, responsibilities to counter racism in its various manifestations and the increased risk of moral ignorance connected to its normalization. (shrink)

Once described as hermaphrodites and later as intersex people, individuals born with intersex variations are routinely subject to so-called “normalizing” medical interventions, often in childhood. Opposition to such practices has been met by attempts to discredit critics and reasserted clinical authority over the bodies of women and men with “disorders of sex development.” However, claims of clinical consensus have been selectively constructed and applied and lack evidence. Limited transparency and lack of access to justice have helped to perpetuate forced interventions. (...) At the same time, associated with the diffusion of distinct concepts of sex and gender, intersex has been constructed as a third legal sex classification, accompanied by pious hopes and unwarranted expectations of consequences. The existence of intersex has also been instrumentalized for the benefit of other, intersecting, populations. The creation of gender categories associated with intersex bodies has created profound risks: a paradoxically narrowed and normative gender binary, maintenance of medical authority over the bodies of “disordered” females and males, and claims that transgressions of social roles ascribed to a third gender are deceptive. Claims that medicalization saves intersex people from “othering,” or that legal othering saves intersex people from medicalization, are contradictory and empty rhetoric. In practice, intersex bodies remain “normalized” or eliminated by medicine, while society and the law “others” intersex identities. That is, medicine constructs intersex bodies as either female or male, while law and society construct intersex identities as neither female nor male. Australian attempts at reforms to recognize the rights of intersex people have either failed to adequately comprehend the population affected or lacked implementation. An emerging human rights consensus demands an end to social prejudice, stigma, and forced medical interventions, focusing on the right to bodily integrity and principles of self-determination. (shrink)

Building on previous work by Mints, Buchholz and Schwichtenberg, a simplified version of continuous normalization for the untyped λ-calculus and Gödel’s is presented and analysed in the coalgebraic framework of non-wellfounded terms with so-called repetition constructors.The primitive recursive normalization function is uniformly continuous w.r.t. the natural metric on non-wellfounded terms. Furthermore, the number of necessary repetition constructors is locally related to the number of reduction steps needed to reach the normal form and its size.It is also shown how continuous normal (...) forms relate to derivations of strong normalizability in the typed λ-calculus and how this leads to new bounds for the sum of the height of the reduction tree and the size of the normal form.Finally, the methods are extended to an infinitary λ-calculus with ω-rule and permutative conversions and this is used to derive a strong form of normalization for an iterative version of Gödel’s system , leading to a value table semantics for number-theoretic functions. (shrink)

The article of N. Kulish "Improvement of legal normalization of church-state relations in Ukraine - an important condition of the implementation of freedom of conscience and religion by believers" analyzes the impact of legal normalization of issues of the religious education on modern believer.

Inverse probability weighting (IPW) is a general tool in survey sampling and causal inference, used in both Horvitz–Thompson estimators, which normalize by the sample size, and Hájek/self-normalized estimators, which normalize by the sum of the inverse probability weights. In this work, we study a family of IPW estimators, first proposed by Trotter and Tukey in the context of Monte Carlo problems, that are normalized by an affine combination of the sample size and a sum of inverse weights. We show how (...) selecting an estimator from this family in a data-dependent way to minimize asymptotic variance leads to an iterative procedure that converges to an estimator with connections to regression control methods. We refer to such estimators as adaptively normalized estimators. For mean estimation in survey sampling, the adaptively normalized estimator has asymptotic variance that is never worse than the Horvitz–Thompson and Hájek estimators. Going further, we show that adaptive normalization can be used to propose improvements of the augmented IPW (AIPW) estimator, average treatment effect (ATE) estimators, and policy learning objectives. Appealingly, these proposals preserve both the asymptotic efficiency of AIPW and the regret bounds for policy learning with IPW objectives, and deliver consistent finite sample improvements in simulations for all three of mean estimation, ATE estimation, and policy learning. (shrink)

Tait's proof of strong normalization for the simply typed λ-calculus is interpreted in a general model theoretical framework by means of the specification of a certain theory T and a certain model /oU of T. The argumentation is partly reduced to formal predicate logic by the application of certain derivability properties of T. The resulting version of Tait's proof is, within the same framework, systematically generalized to the Calculus of Constructions and other advanced type systems. The generalization proceeds along the (...) formal level in the sense that T is modified first and that the new theory partly dictates the subsequent transformation of /oU, which is carried out in stages. The uniform and standardized character of the argumentation contributes to its perspicuity. (shrink)

This paper proves the strong normalization of classical natural deduction with disjunction and permutative conversions, by using CPS-translation and augmentations. Using them, this paper also proves the strong normalization of classical natural deduction with general elimination rules for implication and conjunction, and their permutative conversions. This paper also proves that natural deduction can be embedded into natural deduction with general elimination rules, strictly preserving proof normalization.

Research on deviant organizational practices has demonstrated that normative and cognitive institutional forces contribute to making deviance acceptable. Data from a survey of 3,751 Chinese firms were applied to test the idea that a clearly articulated alternative identity is necessary if a firm is to resist the normalization of deviance. Widespread acceptance of delinquency in repaying loans was shown to make it more likely that a firm adopts that practice, but this normalization process is less likely for firms with a (...) stronger anti-deviance identity. (shrink)

We prove the strong normalization theorem for the natural deduction system for the constructive arithmetic TRDB (the system with Definition by Transfinite Recursion and Bar induction), which was introduced by Yasugi and Hayashi. We also establish the consistency of this system, applying the strong normalization theorem.

The usual rule used to obtain natural deduction formulations of classical logic from intuitionistic logic, namely.

In lieu of an abstract, here is a brief excerpt of the content:Evaluation, Standards, Normalization: Historico-philosophical Formations and the Conditions of Possibility for Checklist Thought Bernadette Baker University of Wisconsin-Madison In education today a new vocabulary has emerged that is far more than just words. In the context of educational policy the setting of goals or objectives is now being subsumed under terms such as statewidestandards, child development is now being adjectivized by descriptors such as learning disability or emotionally disturbed, (...) and the evaluation ofclassroom-based performance is now being collated in aportfolio. These are more than just buzz words-at one level they are new ways of governing children and teachers, of organizing action, and of perceiving the world. What, for instance, does it tell us about ourselves when first-grade students Mikey, Enrique, Waldo, orDonal are introduced to visitors to the school by labels such as LD, ED, ADD, ADHD, and so forth, rather thanby their name? What does it tell us about ourselves when we say a curriculum or program of study is in line with the standards established somewhere else? And what story do we think is being narratedin the documentation of a child's performance in portfolio form across a semester or year? In consideringwhyterms suchasstandards, child development, or even evaluation have such contemporary currency I am necessarily drawn into a study of the timespaces in which they did not have such currency at all. This paper maps four moves into a moment that I think of as a rather long present-day-a present that is not simply this morning, yesterday, or the daybefore, but one that links the subjectivities ofthose now living in educational workto those made available about one hundred years ago. The four moves that I analyze here can be thought of as conditions of possibility for the operation of contemporary educational mies of reasoning, especially those that have formed around the resurgent popularity of"checklist thought" in reform efforts. The four moves collectively historicize how notions of standards, child development, and evaluation can pop up as commonsensical tropes through which to gather and degather action in the educational field. The first ofthese moves is that which flows from the operation ofan ideal to the operation of a norm. The second move is that which flows between the advent of statistics and the advent of eugenics. The third move is that which flows between the appearance ofnovels and fiction and the novel ficticityoffacts. And the fourth move is that which flows from the fictions of child development narratives to the stories that standards tell us. Collectively, these historico-philosophical moves will enable reconsideration of what we think evaluation, standards, and norms for child development actually narrate, lending food for thought to the specificityoftheir uptake in music education. From Ideal to Norm One way inwhichto examinethe shift from a seventeenth-century concept of the ideal to the nineteenth-century concept of the norm is by telling a story that was told in the early twentieth century. At this time when the educational field was formalizing, there was great care taken to record discussions held at conferences. When conferenceproceedings werepublished, theywere usually structured so that the presenter's paper©Philosophy ofMusic Education ReviewlO, no. 1 (Fall, 2002): 92-101. Bernadette Baker 93 was followed by a transcript of the conversation held after it. Like today, in the discussion time, audience members asked questions or made comments. Unlike today, the names of such participating audience members were typed into the proceedings and their specific questions or comments were written up as part ofreporting on the paper presented. In a discussion held at a conference in 1 905 on the topic of methods for training children labeledas feebleminded, apresenterhadspokenof the positive uses of a vegetable garden in the disciplining of feebleminded girls. The audience members relayed their own versions of experimenting with gardening and gathering, some complaining oftoo little space and others indicating the effects of having too many fields from which to gather. Dr. Dunlap was one such participant, indicatingimplicitlytheeffectsofhavingtoo many choices. In the spirit ofthe hunter/gatherer dichotomy, thegirlslabeledas feeblemindedatthe institutionwhereDr. Dunlap worked weresentout to pick com. The following story emerged. Dr. Dunlap: Our girls go out under an attendant and gather vegetables... (shrink)

The author suggests to look at media research from a historical perspective and compare the projects of the “golden period”, that is, the 1990s – early 2000s, with the works of recent years. After preliminary contextual explanations, choosing for a more detailed presentation projects of S. Zielinski and J. Parikka, the author shows how the tasks of media studies and their methodology change during the transition from large-scale panoramas claiming to build a new history from the perspectives of media to (...) often fragmented and situational analyses of components of chosen media (for example, the translation of color dispersion into the chemical language of a photograph of a distant star). This was the way by which archaeology, attentive to geological time, turned into archival work being done for “commercial use or machine learning”. This is how the radical approaches to media research characteristic of the first media theorists are leveled, because scientists publishing their works since the second half of the 2010s contribute to the normalization of media theory by bringing it to the long-discussed topics of other disciplines, such as cognitive functions or theories of signs. At the same time, media theory of recent years is being largely politicized, adopting governmental instructions and reducing the “variantology” and multiplicity of media that were developed earlier. (shrink)

A normalizable natural deduction formulation, with subformula property, of the implicative fragment of classical logic is presented. A traditional notion of normal deduction is adapted and the corresponding weak normalization theorem is proved. An embedding of the classical logic into the intuitionistic logic, restricted on propositional implicational language, is described as well. We believe that this multiple-conclusion approach places the classical logic in the same plane with the intuitionistic logic, from the proof-theoretical viewpoint.

Less salient, lower contrast disks appear to be more numerous than more salient, higher contrast disks when intermingled in equal numbers into the same display, but they are equal in perceived numerosity when segregated into different displays. Comparative judgements indicate that the apparent numerosity of the lower contrast disks is unaffected by being intermingled with high contrast disks, whereas the high contrast disks are reduced in numerosity by being intermingled with the low contrast ones. Here, we report that this illusion (...) also occurs for absolute judgements of the numerosities of displays of from 20 to 80 disks. A model based on luminance-difference contrast normalization explains the illusory loss of high-contrast items along with veridical perception of the low-contrast ones. The model correctly predicts that perceived numerosity is linearly related to the square-root of the number of disks, with the extent of the illusion depending on an attentionally-weighted function of contrast and assimilation. (shrink)

An Introduction to Proof Theory provides an accessible introduction to the theory of proofs, with details of proofs worked out and examples and exercises to aid the reader's understanding. It also serves as a companion to reading the original pathbreaking articles by Gerhard Gentzen. The first half covers topics in structural proof theory, including the Gödel-Gentzen translation of classical into intuitionistic logic, natural deduction and the normalization theorems, the sequent calculus, including cut-elimination and mid-sequent theorems, and various applications of these (...) results. The second half examines ordinal proof theory, specifically Gentzen's consistency proof for first-order Peano Arithmetic. The theory of ordinal notations and other elements of ordinal theory are developed from scratch, and no knowledge of set theory is presumed. The proof methods needed to establish proof-theoretic results, especially proof by induction, are introduced in stages throughout the text. Mancosu, Galvan, and Zach's introduction will provide a solid foundation for those looking to understand this central area of mathematical logic and the philosophy of mathematics. (shrink)

Resumo: O objetivo deste texto é refletir sobre a produção de anormalidades. de um ponto de vista histórico-hermenêutico. Partindo do marco teórico proposto por Michel Foucault, será possível ver como o binômio normalidade-anormalidade, seja de modo disciplinar, seja biopolítico, serve à produção de indivíduos mediante relações de saber-poder. Nesses termos, observa-se como se dá a produção de anormalidades na obra de Foucault. Na segunda seção, verifica-se como a discussão sobre o biopoder pode ser utilizada no intuito de problematizar situações e (...) casos ocorridos neste continente. Trata-se de relacionar a produção de anormalidades com o desenvolvimento do Higienismo na América Latina, dando a perceber algumas estratégias adotadas na normalização e produção de corpos higiênicos. (shrink)

Inductive characterizations of the sets of terms, the subset of strongly normalizing terms and normal forms are studied in order to reprove weak and strong normalization for the simply-typed λ-calculus and for an extension by sum types with permutative conversions. The analogous treatment of a new system with generalized applications inspired by generalized elimination rules in natural deduction, advocated by von Plato, shows the flexibility of the approach which does not use the strong computability/candidate style à la Tait and Girard. (...) It is also shown that the extension of the system with permutative conversions by η-rules is still strongly normalizing, and likewise for an extension of the system of generalized applications by a rule of ``immediate simplification''. By introducing an infinitely branching inductive rule the method even extends to Gödel's T. (shrink)

Gentzen writes in the published version of his doctoral thesis Untersuchungen über das logische Schliessen that he was able to prove the normalization theorem only for intuitionistic natural deduction, but not for classical. To cover the latter, he developed classical sequent calculus and proved a corresponding theorem, the famous cut elimination result. Its proof was organized so that a cut elimination result for an intuitionistic sequent calculus came out as a special case, namely the one in which the sequents have (...) at most one formula in the right, succedent part. Thus, there was no need for a direct proof of normalization for intuitionistic natural deduction. The only traces of such a proof in the published thesis are some convertibilities, such as when an implication introduction is followed by an implication elimination [1934–35, II.5.13]. It remained to Dag Prawitz in 1965 to work out a proof of normalization. Another, less known proof was given also in 1965 by Andres Raggio.We found in February 2005 an early handwritten version of Gentzen's thesis, with exactly the above title, but with rather different contents: Most remarkably, it contains a detailed proof of normalization for what became the standard system of natural deduction. The manuscript is located in the Paul Bernays collection at the ETH-Zurichwith the signum Hs. 974: 271. Bernays must have gotten it well before the time of his being expelled from Göttingen on the basis of the racial laws in April 1933. (shrink)

A simple proof is given of the property that the set of strongly normalizing lambda terms coincides with the set of lambda terms typable in certain intersection type assignment systems.