An unknown process is generating a sequence of symbols, drawn from an alphabet, A. Given an initial segment of the sequence, how can one predict the next symbol? Ray Solomonoff’s theory of inductive reasoning rests on the idea that a useful estimate of a sequence’s true probability of being outputted by the unknown process is provided by its algorithmic probability (its probability of being outputted by a species of probabilistic Turing machine). However algorithmic probability is a “semimeasure”: i.e., the (...) sum, over all x∈A, of the conditional algorithmic probabilities of the next symbol being x, may be less than 1. Prevailing wisdom has it that algorithmic probability must be normalized, to eradicate this semimeasure property, before it can yield acceptable probability estimates. This paper argues, to the contrary, that the semimeasure property contributes substantially to the power and scope of an algorithmic-probability-based theory of induction, and that normalization is unnecessary. (shrink)

The framework of Solomonoff prediction assigns prior probability to hypotheses inversely proportional to their Kolmogorov complexity. There are two well-known problems. First, the Solomonoff prior is relative to a choice of Universal Turing machine. Second, the Solomonoff prior is not computable. However, there are responses to both problems. Different Solomonoff priors converge with more and more data. Further, there are computable approximations to the Solomonoff prior. I argue that there is a tension between these two (...) responses. This is because computable approximations to Solomonoff prediction do not always converge. (shrink)

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 (...) class='Hi'>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)

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)

Algorithmic information theory gives an idealized notion of compressibility that is often presented as an objective measure of simplicity. It is suggested at times that Solomonoff prediction, or algorithmic information theory in a predictive setting, can deliver an argument to justify Occam’s razor. This article explicates the relevant argument and, by converting it into a Bayesian framework, reveals why it has no such justificatory force. The supposed simplicity concept is better perceived as a specific inductive assumption, the assumption of (...) effectiveness. It is this assumption that is the characterizing element of Solomonoff prediction and wherein its philosophical interest lies. (shrink)

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)

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)

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)

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)

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)

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)

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)

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)

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.

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

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

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)

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)

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.

We define a generic notion of cut that applies to many first-order theories. We prove a generic cut elimination theorem showing that the cut elimination property holds for all theories having a so-called pre-model. As a corollary, we retrieve cut elimination for several axiomatic theories, including Church's simple type theory.

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)

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.

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)

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 [gallier], general results (due to Coppo, Dezani and Veneri) relating properties of pure lambda terms and their typability in some systems with conjunctive types are proved in a uniform way by using the reducibility method.This paper gives a very short proof of the same results (actually, one of them is a bit stronger) using purely arithmetical methods.

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)

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.

This paper points out an error of Parigot’s proof of strong normalization of second order classical natural deduction by the CPS-translation, discusses erasing-continuation of the CPS-translation, and corrects that proof by using the notion of augmentations.

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)

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)

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)

ellucci, C., Existential instantiation and normalization in sequent natural deduction, Annals of Pure and Applied Logic 58 111–148. A sequent conclusion natural deduction system is introduced in which classical logic is treated per se, not as a special case of intuitionistic logic. The system includes an existential instantiation rule and involves restrictions on the discharge rules. Contrary to the standard formula conclusion natural deduction systems for classical logic, its normal derivations satisfy both the subformula property and the separation property (...) and allow to establish a version of the midsequent theorem and Herbrand's theorem. (shrink)

At one point Rawls thought that “a normalization of interests attributed to the parties” is “common to social contract doctrines.” Normalization has a great appeal: once we specify the normalized perspective, we can generate strong and definite principles of justice. Public reasoning is restricted to those who reason from the eligible, normalized, perspective; those who fall outside the “normal” are to be dismissed as unreasonable, unjust, or illiberal. As Rawls’s political liberalism project developed he increasingly relaxed his (...) class='Hi'>normalization assumptions, allowing room for not only different conceptions of the good, but of justice. This paper explores the post-Rawlsian movement in public reason to maximally relax, or even abandon, normalizing assumptions, drawing on a maximal diversity of normative perspectives in public justification. The public reason project is at a critical juncture. Are we to look back, defending Rawls’s substantive conclusions by devising new defenses of normalization, circling the wagons around the cherished two principles? Or are we to seek to fulfill the promise of public reason as providing a common public and moral world in the midst of diversity? (shrink)