The notions of permutable and weak-permutable convergence of a series|$\sum _{n=1}^{\infty }a_{n}$|of real numbers are introduced. Classically, these two notions are equivalent, and, by Riemann’s two main theorems on the convergence of series, a convergent series is permutably convergent if and only if it is absolutely convergent. Working within Bishop-style constructive mathematics, we prove that Ishihara’s principle BD-|$\mathbb {N}$|implies that every permutably convergent series is absolutely convergent. Since there are models of constructive mathematics in which the Riemann permutation theorem for (...) series holds but BD-|$\mathbb{N}$|does not, the best we can hope for as a partial converse to our first theorem is that the absolute convergence of series with a permutability property classically equivalent to that of Riemann implies BD-|$\mathbb {N}$|. We show that this is the case when the property is weak-permutable convergence. (shrink)

Driven by the question, 'What is the computational content of a (formal) proof?', this book studies fundamental interactions between proof theory and computability. It provides a unique self-contained text for advanced students and researchers in mathematical logic and computer science. Part I covers basic proof theory, computability and Gödel's theorems. Part II studies and classifies provable recursion in classical systems, from fragments of Peano arithmetic up to Π11-CA0. Ordinal analysis and the (Schwichtenberg-Wainer) subrecursive hierarchies play a central role and (...) are used in proving the 'modified finite Ramsey' and 'extended Kruskal' independence results for PA and Π11-CA0. Part III develops the theoretical underpinnings of the first author's proof assistant MINLOG. Three chapters cover higher-type computability via information systems, a constructive theory TCF of computable functionals, realizability, Dialectica interpretation, computationally significant quantifiers and connectives and polytime complexity in a two-sorted, higher-type arithmetic with linear logic. (shrink)

Let A be a formula without implications, and Γ consist of formulas containing disjunction and falsity only negatively and implication only positively. Orevkov and Nadathur proved that classical derivability of A from Γ implies intuitionistic derivability, by a transformation of derivations in sequent calculi. We give a new proof of this result , where the input data are natural deduction proofs in long normal form involving stability axioms for relations; the proof gives a quadratic algorithm to remove the stability axioms. (...) This can be of interest for computational uses of classical proofs. (shrink)

From a classical proof that the gcd of natural numbers a1 and a2 is a linear combination of the two, we extract by Gödel's Dialectica interpretation an algorithm computing the coefficients. The proof uses the minimum principle. We show generally how well-founded recursion can be used to Dialectica interpret well-founded induction, which is needed in the proof of the minimum principle. In the special case of the example above it turns out that we obtain a reasonable extracted term, representing an (...) algorithm close to Euclid's. (shrink)

Buchholz presented a method to build notation systems for infinite sequent-style derivations, analogous to well-known systems of notation for ordinals. The essential feature is that from a notation one can read off by a primitive recursive function its n th predecessor and, e.g. the last rule applied. Here we extend the method to the more general setting of infinite terms, in order to make it applicable in other proof-theoretic contexts as well as in recursion theory. As examples, we use the (...) method to 1. give a new proof of a well-known trade-off theorem , which says that detours through higher types can be eliminated by the use of transfinite recursion along higher ordinals, and 2. construct a continuous normalization operator with an explicit modulus of continuity. (shrink)

Consider the problem which set V of propositional variables suffices for whenever, where, and ⊢c and ⊢i denote derivability in classical and intuitionistic implicational logic, respectively. We give a direct proof that stability for the final propositional variable of the (implicational) formula A is sufficient; as a corollary one obtains Glivenko's theorem. Conversely, using Glivenko's theorem one can give an alternative proof of our result. As an alternative to stability we then consider the Peirce formula. It is an easy consequence (...) of the result above that adding a single instance of the Peirce formula suffices to move from classical to intuitionistic derivability. Finally we consider the question whether one could do the same for minimal logic. Given a classical derivation of a propositional formula not involving ⊥, which instances of the Peirce formula suffice as additional premises to ensure derivability in minimal logic? We define a set of such Peirce formulas, and show that in general an unbounded number of them is necessary. (shrink)

Several properties of monotone functionals (MF) and monotone majorizable functionals (MMF) used in the earlier work by the author and van de Pol are proved. It turns out that the terms of the simply typed lambda-calculus define MF, but adding primitive recursion, and even monotonic primitive recursion changes the situation: already Z.Z(1 — sg) is not MMF. It is proved that extensionality is not Dialectica-realizable by MMF, and a simple example of a MF which is not hereditarily majorizable is given.

The paper presents a refined method of extracting reasonable and sometimes unexpected programs from classical proofs of formulas of the form ∀x∃yB . We also generalize previously known results, since B no longer needs to be quantifier-free, but only has to belong to a strictly larger class of so-called “goal formulas”. Furthermore we allow unproven lemmas D in the proof of ∀x∃yB , where D is a so-called “definite” formula.

Proceedings of the NATO Advanced Study Institute on Proof and Computation, held in Marktoberdorf, Germany, July 20 - August 1, 1993.

This is a tutorial for the Minlog Proof Assistant, version 5.0.

Constructive mathematics – mathematics in which ‘there exists’ always means ‘we can construct’ – is enjoying a renaissance. Fifty years on from Bishop’s groundbreaking account of constructive analysis, constructive mathematics has spread out to touch almost all areas of mathematics and to have profound influence in theoretical computer science. This handbook gives the most complete overview of modern constructive mathematics, with contributions from leading specialists surveying the subject’s myriad aspects. Major themes include: constructive algebra and geometry, constructive analysis, constructive topology, (...) constructive logic and foundations of mathematics, and computational aspects of constructive mathematics. A series of introductory chapters provides graduate students and other newcomers to the subject with foundations for the surveys that follow. Edited by four of the most eminent experts in the field, this is an indispensable reference for constructive mathematicians and a fascinating vista of modern constructivism for the increasing number of researchers interested in constructive approaches. (shrink)

Childhood adversity is associated with altered or dysregulated stress reactivity; these altered patterns of physiological functioning persist into adulthood. Evidence from both preclinical animal models and human neuroimaging studies indicates that early life experience differentially influences stressor-evoked activity within central visceral neural circuits proximally involved in the control of stress responses, including the subgenual anterior cingulate cortex (sgACC), paraventricular nucleus of the hypothalamus (PVN), bed nucleus of the stria terminalis (BNST) and amygdala. However, the relationship between childhood adversity and the (...) resting-state connectivity of this central visceral network remains unclear. To this end, we examined relationships between childhood threat and childhood socioeconomic deprivation, the resting-state connectivity between our regions of interest (ROIs), and affective symptom severity and diagnoses. We recruited a transdiagnostic sample of young adult males and females (n= 100; mean age = 27.28,SD= 3.99; 59 females) with a full distribution of maltreatment history and symptom severity across multiple affective disorders. Resting-state data were acquired using a 7.2-min functional magnetic resonance imaging (fMRI) sequence; noted ROIs were applied as masks to determine ROI-to-ROI connectivity. Threat was determined by measures of childhood traumatic events and abuse. Socioeconomic deprivation (SED) was determined by a measure of childhood socioeconomic status (parental education level). Covarying for age, race and sex, greater childhood threat was significantly associated with lower BNST-PVN, amygdala-sgACC and PVN-sgACC connectivity. No significant relationships were found between SED and resting-state connectivity. BNST-PVN connectivity was associated with the number of lifetime affective diagnoses. Exposure to threat during early development may entrain altered patterns of resting-state connectivity between these stress-related ROIs in ways that contribute to dysregulated neural and physiological responses to stress and subsequent affective psychopathology. (shrink)

This paper describes formalizations of Tait's normalization proof for the simply typed λ-calculus in the proof assistants Minlog, Coq and Isabelle/HOL. From the formal proofs programs are machine-extracted that implement variants of the well-known normalization-by-evaluation algorithm. The case study is used to test and compare the program extraction machineries of the three proof assistants in a non-trivial setting.

It is shown how to restrict recursion on notation in all finite types so as to characterize the polynomial-time computable functions. The restrictions are obtained by using a ramified type structure, and by adding linear concepts to the lambda calculus.

Schwichtenberg showed that the System T definable functionals are closed under a rule-like version Spector’s bar recursion of lowest type levels 0 and 1. More precisely, if the functional Y which controls the stopping condition of Spector’s bar recursor is T-definable, then the corresponding bar recursion of type levels 0 and 1 is already T-definable. Schwichtenberg’s original proof, however, relies on a detour through Tait’s infinitary terms and the correspondence between ordinal recursion for α < ε₀ and primitive (...) recursion over finite types. This detour makes it hard to calculate on given concrete system T input, what the corresponding system T output would look like. In this paper we present an alternative (more direct) proof based on an explicit construction which we prove correct via a suitably defined logical relation. We show through an example how this gives a straightforward mechanism for converting bar recursive definitions into T-definitions under the conditions of Schwichtenberg’s theorem. Finally, with the explicit construction we can also easily state a sharper result: if Y is in the fragment Tᵢ then terms built from BR^ℕ,σ for this particular Y are definable in the fragment T_i+max{1,level(σ)}+2. (shrink)

In a recent article, Hooper and Spicer make several arguments against legislation that would mandate the use of bicycle helmets. While they present reasonable objections to the utilitarian as well as the justice defence of such legislation, their review of the empirical evidence contains inaccuracies, omissions and a bias in the selection of empirical data. While there are legitimate reasons to argue against mandating helmet legislation, these arguments should still be based on clinically and scientifically sound evidence.

The issue of mandatory cycle helmets is highly contentious. The aim of this paper is not to argue for or against legislation but to suggest criteria on which the debate should focus. This is done by attempting to answer the question: 'What criteria must be met before cycle helmet wearing is enforced?' Consideration is given to principles, precedents and consequences and four criteria are suggested. The criteria are to do with effectiveness, personal liberty, public acceptability and the promotion of (...) the public health benefits of cycling. (shrink)

Bicycle helmets protect against head injury. Mandatory helmet laws likely increase their use. Although 21 states and Washington, DC have mandatory helmet laws for youth bicyclists, no U.S. state has a mandatory helmet law that applies to all ages; however, some localities have all-age helmet laws for bicyclists. This study abstracted local helmet laws applicable to all-ages to examine their elements.

Paternalism is a frequent source of anxiety and scholarly enquiry within public health. This article examines debate in the UK from the 1950s to the early 1980s about two quintessentially paternalistic laws: those making it compulsory to use a motorcycle helmet, and a car seatbelt. This kind of historical analysis, looking at change over time and the circumstances that prevent or enable such change, draws attention to two significant features: the contingent nature of that which is perceived as paternalistic (...) and therefore objectionable, and the wide range of arguments that can be marshalled for and against. It suggests that paternalism became a particularly disruptive accusation in the UK of the 1970s in relation to seatbelts, thanks to the population that would be affected and the wider socio-political context. It also suggests that arguments about the social cost of death and injury on the roads, along with overt acceptance that some element of paternalism could be acceptable, proved influential—as was the sense of inevitability that 10 years of regular debate helped to create. (shrink)

Motorcycle helmet laws are perceived to infringe upon individual rights even though they reduce mortality and health care costs. We describe proposed helmet legislation that protects individual rights and provides incentives for helmet use through a differential motorcycle registration fee that requires higher fees for those who wish to ride without a helmet.

This chapter charts a metamorphosis in Djarin's ethical decision‐making across the first two seasons of The Mandalorian. Philosophy and psychology have centered on moral reasoning and developmental processes based on logic, reasoning, and a primary concern with oneself, sometimes tempered by respect for others. Female development typically orients women toward an “ethics of care”: People have responsibilities toward others as well as themselves. The Mandalorian is the story of one man's moral overhaul toward care. Early Mando's moral decisions are based (...) on hierarchy, status, rules, fairness, maximizing benefit, and values. The shift in Mando's decision‐making approach occurred gradually, beginning with the impact of a rampaging blurrg. The hypothetical scenario about the pharmacy illuminates something crucial for understanding Djarin's gradual adoption of ethics of care: often, our choice to frame an ethical dilemma through one perspective or another winds up determining our moral decision. (shrink)