Bilateralists hold that the meanings of the connectives are determined by rules of inference for their use in deductive reasoning with asserted and denied formulas. This paper presents two bilateral connectives comparable to Prior's tonk, for which, unlike for tonk, there are reduction steps for the removal of maximal formulas arising from introducing and eliminating formulas with those connectives as main operators. Adding either of them to bilateral classical logic results in an incoherent system. One way around this problem is (...) to count formulas as maximal that are the conclusion of reductio and major premise of an elimination rule and to require their removability from deductions. The main part of the paper consists in a proof of a normalisation theorem for bilateral logic. The closing sections address philosophical concerns whether the proof provides a satisfactory solution to the problem at hand and confronts bilateralists with the dilemma that a bilateral notion of stability sits uneasily with the core bilateral thesis. (shrink)

This paper considers a formalisation of classical logic using general introduction rules and general elimination rules. It proposes a definition of ‘maximal formula’, ‘segment’ and ‘maximal segment’ suitable to the system, and gives reduction procedures for them. It is then shown that deductions in the system convert into normal form, i.e. deductions that contain neither maximal formulas nor maximal segments, and that deductions in normal form satisfy the subformula property. Tarski’s Rule is treated as a general introduction rule for implication. (...) The general introduction rule for negation has a similar form. Maximal formulas with implication or negation as main operator require reduction procedures of a more intricate kind not present in normalisation for intuitionist logic. (shrink)

This paper studies a formalisation of intuitionistic logic by Negri and von Plato which has general introduction and elimination rules. The philosophical importance of the system is expounded. Definitions of ‘maximal formula’, ‘segment’ and ‘maximal segment’ suitable to the system are formulated and corresponding reduction procedures for maximal formulas and permutative reduction procedures for maximal segments given. Alternatives to the main method used are also considered. It is shown that deductions in the system convert into normal form and that deductions (...) in normal form have the subformula property. (shrink)

This brief note corrects an error in one of the reduction steps in my paper 'Normalisation for Bilateral Classical Logic with some Philosophical Remarks' published in the Journal of Applied Logics 8/2 (2021): 531-556.

An exploration of the governmental policy, prison works, and its attendant recidivism provides the general opening. The 1944 Education Act is then taken as furnishing the medical model of personal handicap and deficiency which informed special education at an early stage. The Warnock Report's attempt to shift considerations to educational grounds is examined with a particular focus upon the ensuing definition of special needs and its legacy in legislation following the 1981 Act to the present. Foucault's concept of normalisation is (...) the basis for analysis of the normative elements in the main features of the national curriculum and testing. This latter together with aspects of the 1988 Education Reform Act are examined with regard to their impact upon special educational needs. The conclusions are that 'education works' and the rediscovery of the medical model of personal deficiency. (shrink)

This note corrects an error in my paper 'Normalisation and Subformula Property for a System of Classical Logic with Tarski's Rule' (Archive for Mathematical Logic 61 (2022): 105-129, DOI 10.1007/s00153-021-00775-6): Theorem 2 is mistaken, and so is a corollary drawn from it as well as a corollary that was concluded by the same mistake. Luckily this does not affect the main result of the paper.

The question of finding a suitable formal account of meaning for the logical signs has troubled many philosophers and logicians since the early days of formal logic, whenever it is even recognised as a problem. Here I attempt to show how two operational approaches to the problem can still be shown to be ‘technically’ equivalent, despite having emerged from two different readings of a single philosophical account, and being essentially distinct with respect to the rôle of ‘will’ in the mathematical (...) activity: on the one hand, the ‘semantics of use’, my own reformulation of P. Martin‐Löf's Intuitionistic Type Theory canonical‐values based semantics by taking the normalisation rules as the key semantical device; and, on the other hand, J. Hintikka's Game‐Theoretical Semantics, where the meaning of logical signs is given via semantical games. The philosophical account from which both emerge is precisely Wittgenstein's later account of propositions, where the notion of ‘language‐games’ is introduced as a key semantical device. Observing that the normalisation rules seem to be able to formalise the explanation of the consequences one can draw from a proposition,3 thus showing the function/purpose/usefulness of its main connective in the calculus of language, it seems reasonable to advocate that such a meta‐mathematical device can be a semantically useful notion which would lead to a more reasonable account of the problem of formulating the meaning of logical constants. (shrink)

In a recent paper del Valle-Inclan and Schlöder argue that bilateral calculi call for their own notion of proof-theoretic harmony, distinct from the usual (or ‘unilateral’) ones. They then put forward a specifically bilateral criterion of harmony, and present a harmonious bilateral calculus for classical logic. In this paper, I show how del Valle-Inclan and Schlöder’s criterion of harmony suggests a notion of normal form for bilateral systems, and prove normalisation for two (harmonious) bilateral calculi for classical logic, HB1 and (...) HB2. The resulting normal derivations have the usual desirable features, like the separation and subformula properties. HB1-normal form turns out to be strictly stronger that the notion of normal form proposed by Nils Kürbis, and HB2-normal form is neither stronger nor weaker than a similar proposal by Marcello D’Agostino, Dov Gabbay, and Sanjay Modgyl. (shrink)

We give two proofs of strong normalisation for second order classical natural deduction. The first one is an adaptation of the method of reducibility candidates introduced in [9] for second order intuitionistic natural deduction; the extension to the classical case requires in particular a simplification of the notion of reducibility candidate. The second one is a reduction to the intuitionistic case, using a Kolmogorov translation.

Feminists have indicated the inadequacies of bioethical debates about human embryonic stem cell research, which have for the most part revolved around concerns about the moral status of the human embryo. Feminists have argued, for instance, that inquiry concerning the ethics and politics of human embryonic stem cell research should consider the relations of social power in which the research is embedded. My argument is that this feminist work on stem cells is itself inadequate, however, insofar as it has not (...) incorporated an analysis of disability into its considerations of the ethical and political issues that surround the phenomena. Thus, I consider claims that disability theorists and anti-disability activists have made about the research. I conclude by indicating that stem cell research must be situated within a cultural matrix that operates in the service of normalisation. (shrink)

Roderich Tumulka’s GRWf theory offers a simple, realist and relativistic solution to the measurement problem of quantum mechanics. It is achieved by the introduction of a stochastic dynamical collapse of the wavefunction. An issue with dynamical collapse theories is that they involve an amendment to the Schrodinger equation; amending the dynamics of such a tried and tested theory is seen by some as problematic. This paper proposes an alteration to GRWf that avoids the need to amend the Schrodinger equation via (...) what might be seen as a primary set of solutions to the Schrodinger equation that satisfy a normalisation condition over space and time. The traditional Born-normalised solutions are shown to be conditionalisations of these primary solutions. (shrink)

In this paper, we argue that there are reasons to believe that an implicit bias for normalcy influences what are considered medically necessary treatments in psychiatry. First, we outline two prima facie reasons to suspect that this is the case. A bias for ‘the normal’ is already documented in disability studies; it is reasonable to suspect that it affects psychiatry too, since psychiatric patients, like disabled people, are often perceived as ‘weird’ by others. Secondly, psychiatry's explicitly endorsed values of well-being (...) and function are hard to measure directly, which is why we see simpler box-ticking conceptions of recovery used in large research studies. This need not be problematic, but might lead to researchers and clinicians focusing too much on treatments that promote easy-to-measure proxies for recovery, instead of what actually matters to psychiatric patients themselves. Next, we provide examples of treatments and treatment decisions within two areas – self-injury and psychosis – which are hard to explain unless we assume that an implicit and harmful normalcy bias is at work. We conclude with some suggestions for clinicians and future research. (shrink)

Cet ouvrage offre une introduction accessible à la théorie de la démonstration : il donne les détails des preuves et comporte de nombreux exemples et exercices pour faciliter la compréhension des lecteurs. Il est également conçu pour servir d’aide à la lecture des articles fondateurs de Gerhard Gentzen. L’ouvrage introduit également aux trois principaux formalismes en usage : l’approche axiomatique des preuves, la déduction naturelle et le calcul des séquents. Il donne une démonstration claire et détaillée des résultats fondamentaux du (...) domaine : traduction de l’arithmétique classique vers l’arithmétique intuitionniste, élimination des coupures, théorème de normalisation et conduit ensuite pas à pas le lecteur vers l’exposé de la célèbre preuve de cohérence de Gentzen pour l’arithmétique de Peano du premier ordre. Il comble ainsi une importante lacune éditoriale en présentant à la fois la théorie structurelle et la théorie ordinale de la démonstration. (shrink)

This paper presents a way of formalising definite descriptions with a binary quantifier ι, where ιx[F, G] is read as ‘The F is G’. Introduction and elimination rules for ι in a system of intuitionist negative free logic are formulated. Procedures for removing maximal formulas of the form ιx[F, G] are given, and it is shown that deductions in the system can be brought into normal form.

Building on previous work by Coquand and Spiwack [T. Coquand, A. Spiwack, A proof of strong normalisation using domain theory, in: Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, LICS’06, IEEE Computer Society Press, 2006, pp. 307–316] we construct a strict domain-theoretic model for the untyped λ-calculus with pattern matching and term rewriting which has the property that a term is strongly normalising if its value is not . There are no disjointness or confluence conditions imposed (...) on the rewrite rules, and under a mild but necessary condition completeness of the method is proven. As an application, we prove strong normalisation for barrecursion in higher types combined with polymorphism and non-deterministic choice. (shrink)

Displacing the physiological model that had held sway in 19th-century medical thinking, early 20th-century hormone research promoted an understanding of the body and sexual desires in which variations in sex characteristics and non-reproductive sexual behaviours such as homosexuality were attributed to anomalies in the internal secretions produced by the testes or the ovaries. Biotypology, a new brand of medical science conceived and led by the Italian endocrinologist Nicola Pende, employed hormone research to study human types and hormone treatments to normalise (...) individuals who did not conform to accepted medical norms. Latin American medical doctors, eugenicists, and sexologists took up biotypology with enthusiasm. This article considers the case studies of Italy, Argentina, and Brazil, and analyses the work of medical doctors who adopted a biotypological mode of reasoning and employed to various extents hormone therapies in their practice. By focusing on hormone therapies that aimed to normalise secondary sexual characteristics and the sexual instinct, the article suggests that while the existence of normality was contested to the point that a number of medical scientists argued that no such thing existed, the pursuit of normality was carried out in very practical terms through the new medical technologies hormone research had introduced. (shrink)

Inquiries into organisational scandals repeatedly attribute wrongdoing to the normalisation of deviance. From this perspective, the cause of harm lies not in the actions of any individual but rather in the institutionalised practices of organisations or sectors. Although an important corrective to dramatic tales of bad apples, the normalisation thesis underplays the role of management in the emergence of deviance. Drawing on literatures exploring ideas of amoral (Carroll in Bus Horiz 30(2):7–15, 1987) or ethically neutral leadership (Treviño et al. in (...) Calif Manag Rev 42(4):128–142, 2000) we seek to bring management back into the explanation of organisational wrongdoing. Amoral theorists point to management’s ethical silence, but they also describe the way in which that silence is sustained by a series of organisational characteristics. We build on this work in arguing that it is management’s deliberate focus on bottom line performance, the diffusion of responsibility and high levels of organisational identification that explain the emergence of wrongdoing. We apply these ideas to the case of the UK’s Stafford hospital which hit the headlines in 2009 when it was reported that poor standards of care had led to a mortality rate markedly above that expected for a hospital of its type. We conclude with a discussion of the circumstances which translate amoral management into unethical outcomes. (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, I will reread the history of molecular genetics from a psychoanalytical angle, analysing it as a case history. Building on the developmental theories of Freud and his followers, I will distinguish four stages, namely: (1) oedipal childhood, notably the epoch of model building (1943–1953); (2) the latency period, with a focus on the development of basic skills (1953–1989); (3) adolescence, exemplified by the Human Genome Project, with its fierce conflicts, great expectations and grandiose claims (1989–2003) and (4) (...) adulthood (2003–present) during which revolutionary research areas such as molecular biology and genomics have achieved a certain level of normalcy—have evolved into a normal science. I will indicate how a psychoanalytical assessment conducted in this manner may help us to interpret and address some of the key normative issues that have been raised with regard to molecular genetics over the years, such as ‘relevance’, ‘responsible innovation’ and ‘promise management’. (shrink)

This article is a methodological discussion of formal approaches to the question of identity of proofs from a philosophical standpoint. First, an introduction to the question of identity of proofs itself is given, followed by a brief reconstruction of the so-called normalisation thesis, proposed by Dag Prawitz in 1971, in which some of its core mathematical and conceptual traits are presented. After that, a comparison between the normalisation thesis and the more well-known Church-Turing thesis on computability is carried out in (...) three main parts: the first dedicated to highlighting some of the analogies between them; the second, their most remarkable differences; and the third, to the possible relations of dependence between the two. Based on these considerations, some concluding remarks concerning the potential of the normalisation thesis and similar approaches to the question of identity of proofs are made in the last section. (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 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)

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)

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

Al-Bassam’s The Al Hamlet Summit (2006), an adaptation of Shakespeare’s Hamlet (1603), presents a cynical comment on the political corruption in the Arab World and it constitutes from a presentist perspective, we argue, an anachronistic critique of some Arab leaders’ lapse into normalisation with the long-standing Other, the Israeli occupation. Al-Bassam captures the political corruption and Arab leaders’ liaison with Israel through the figure of Claudius, who, like Arab leaders, normalises relations with the enemies of his nation, Fortinbras and the (...) Arms Dealer. Many Arab leaders are normalising relations with Israel as a defensive mechanism against their citizens who have been protesting against dictatorial and tyrannical regimes that have conceived rottenness and corruption in the political and spiritual foundations of the states. While the waves of normalisation that have plagued the contemporary Arab scene raise the spectre of Western hegemony over Arabs, being channelled by the Trump Administration, many Arab leaders hurl to the strategy of normalisation ‘pants down’ so as to curb their citizens prospective revolutionary acts. (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.

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)

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)

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)

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.

Boycotts of various types and forms have become in recent years an increasingly common feature of political life. And yet, despite both their ubiquity and clear ethical grounding, they remain to date under-explored in academic philosophy. I examine in this article the question of the ethics of boycotting, using the academic and cultural boycott of Israel as a case study. I propose that the boycott exhibits an intriguing pattern of continuous tension between its own stated principles and its realised practices, (...) and suggest that this tension is not a dysfunction of the boycott but rather a structural feature, which emanates from its primary commitment to the idea of anti-normalisation as an ethical imperative. I explore the complex cross-linguistic political pragmatics of the notion of normalisation, and argue that the commitment to it on the part of the boycott movement, as a group actor, effectively amounts to a capricious form of arbitrary treatment of the boycotted. I then propose that the effective validation of arbitrary treatment constitutes, first, a harm in itself; and, second, that it hinders the capacity of the campaign to draw on and contribute to a general theory of the ethics of boycotting. (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)