A famous theorem by van der Waerden states the following: Given any finite coloring of the integers, one color contains arbitrarily long arithmetic progressions. Equivalently, for every q,k, there is an N = N(q,k) such that for every q-coloring of an interval of length N one color contains a progression of length k. An obvious question is what is the growth rate of N = N(q,k). Some proofs, like van der Waerden's combinatorial argument, answer this question directly, while the topological (...) proof by Furstenberg and Weiss does not. We present an analysis of (Girard's variant of) Furstenberg and Weiss's proof based on monotone functional interpretation, both yielding bounds and providing a general illustration of proof mining in topological dynamics. The bounds do not improve previous results by Girard, but only—as is also revealed by the analysis—because the combinatorial proof and the topological dynamics proof in principle are identical. (shrink)

In this paper, we present another case study in the general project of proof mining which means the logical analysis of prima facie non-effective proofs with the aim of extracting new computationally relevant data. We use techniques based on monotone functional interpretation developed in Kohlenbach , Oxford University Press, Oxford, 1996, pp. 225–260) to analyze Cheney's simplification 189) of Jackson's original proof 320) of the uniqueness of the best L1-approximation of continuous functions fC[0,1] by polynomials pPn (...) of degree n. Cheney's proof is non-effective in the sense that it is based on classical logic and on the non-computational principle WKL . The result of our analysis provides the first effective uniform modulus of uniqueness . Moreover, the extracted modulus has the optimal ε-dependency as follows from Kroó 331). The paper also describes how the uniform modulus of uniqueness can be used to compute the best L1-approximations of a fixed fC[0,1] with arbitrary precision. The second author uses this result to give a complexity upper bound on the computation of the best L1-approximation in Oliva 66–77). (shrink)

This article presents a parametrized functional interpretation. Depending on the choice of two parameters one obtains well-known functional interpretations such as Gödel's Dialectica interpretation, Diller-Nahm's variant of the Dialectica interpretation, Kohlenbach's monotone interpretations, Kreisel's modified realizability, and Stein's family of functional interpretations. A functional interpretation consists of a formula interpretation and a soundness proof. I show that all these interpretations differ only on two design choices: first, on the number of (...) counterexamples for A which became witnesses for ¬A when defining the formula interpretation and, second, the inductive information about the witnesses of A which is considered in the proof of soundness. Sufficient conditions on the parameters are also given which ensure the soundness of the resulting functional interpretation. The relation between the parametrized interpretation and the recent bounded functional interpretation is also discussed. (shrink)

Recently, the second author, Briseid, and Safarik introduced nonstandard Dialectica, a functional interpretation capable of eliminating instances of familiar principles of nonstandard arithmetic—including overspill, underspill, and generalizations to higher types—from proofs. We show that the properties of this interpretation are mirrored by first-order logic in a constructive sheaf model of nonstandard arithmetic due to Moerdijk, later developed by Palmgren, and draw some new connections between nonstandard principles and principles that are rejected by strict constructivism. Furthermore, we introduce (...) a variant of the Diller–Nahm interpretation with two different kinds of quantifiers, similar to Hernest’s light Dialectica interpretation, and show that one can obtain nonstandard Dialectica by weakening the computational content of the existential quantifiers—a process called herbrandization. We also define a constructive sheaf model mirroring this new functional interpretation, and show that the process of herbrandization has a clear meaning in terms of these sheaf models. (shrink)

In recent years, proof theoretic transformations that are based on extensions of monotone forms of Gödel’s famous functional interpretation have been used systematically to extract new content from proofs in abstract nonlinear analysis. This content consists both in effective quantitative bounds as well as in qualitative uniformity results. One of the main ineffective tools in abstract functional analysis is the use of sequential forms of weak compactness. As we recently verified, the sequential form of weak compactness (...) for bounded closed and convex subsets of an abstract Hilbert space can be carried out in suitable formal systems that are covered by existing metatheorems developed in the course of the proof mining program. In particular, it follows that the monotone functional interpretation of this weak compactness principle can be realized by a functional Ω∗ definable from bar recursion of lowest type. While a case study on the analysis of strong convergence results that are based on weak compactness indicates that the use of the latter seems to be eliminable, things apparently are different for weak convergence theorems such as the famous Baillon nonlinear ergodic theorem. For this theorem we recently extracted an explicit bound on a metastable version of this theorem that is primitive recursive relative to Ω∗.In the current paper we for the first time give the construction of Ω∗ . As a corollary to the fine analysis of the use of bar recursion in this construction we obtain that Ω∗ elevates arguments in Tn at most to resulting functionals in Tn+2 . In particular, one can conclude from this that our bound on Baillon’s theorem is at least definable in T4. (shrink)

In view of an enhancement of our implementation on the computer, we explore the possibility of an algorithmic optimization of the various proof-theoretic techniques employed by Kohlenbach for the synthesis of new effective uniform bounds out of established qualitative proofs in Numerical Functional Analysis. Concretely, we prove that the method of “colouring” some of the quantifiers as “non-computational” extends well to ε-arithmetization, elimination-of-extensionality and model-interpretation.

We prove a result relating the author's monotone functional interpretation to the bounded functional interpretation due to Ferreira and Oliva. More precisely we show that largely a solution for the bounded interpretation also is a solution for the monotone functional interpretation although the latter uses the existence of an underlying precise witness. This makes it possible to focus on the extraction of bounds while using the conceptual benefit of having precise realizers at the (...) same time without having to construct them. (shrink)

A notion of feasible function of finite type based on the typed lambda calculus is introduced which generalizes the familiar type 1 polynomial-time functions. An intuitionistic theory IPVω is presented for reasoning about these functions. Interpretations for IPVω are developed both in the style of Kreisel's modified realizability and Gödel's Dialectica interpretation. Applications include alternative proofs for Buss's results concerning the classical first-order system S12 and its intuitionistic counterpart IS12 as well as proofs of some of Buss's conjectures concerning (...) IS12, and a proof that IS12 cannot prove that extended Frege systems are not polynomially bounded. (shrink)

In this paper we study with proof-theoretic methods the function(al) s provably recursive relative to Ramsey's theorem for pairs and the cohesive principle (COH). Our main result on COH is that the type 2 functional provably recursive from $RCA_0 + COH + \Pi _1^0 - CP$ are primitive recursive. This also provides a uniform method to extract bounds from proofs that use these principles. As a consequence we obtain a new proof of the fact that $WKL_0 + (...) \Pi _1^0 - CP + COH$ is $\Pi _1^0 $ -conservative over PRA. Recent work of the first author showed that $\Pi _1^0 + CP + COH$ is equivalent to a weak variant of the Bolzano-Weierstraß principle. This makes it possible to use our results to analyze not only combinatorial but also analytical proofs. For Ramsey's theorem for pairs and two colors $\left( {RT_2^2 } \right)$ we obtain the upper bounded that the type 2 functionals provable recursive relative to $RCA_0 + \sum\nolimits_2^0 {IA + RT_2^2 } $ are in T₁. This is the fragment of Gödel's system T containing only type 1 recursion—roughly speaking it consists of functions of Ackermann type. With this we also obtain a uniform method for the extraction of T₁-bounds from proofs that use RT2..... Moreover, this yields a new proof of the fact that $WKL_0 + \sum\nolimits_2^0 {IA} + RT_2^2 $ is $\Pi _1^0 $ -conservative over $RCA_0 + \sum\nolimits_2^0 { - IA} $ . The results are obtained in two steps: in the first step a term including Skolem functions for the above principles is extracted from a given proof. This is done using Gödel's functional interpretation. After this the term is normalized, such that only specific instances of the Skolem functions are used. In the second step this term is interpreted using $\Pi _1^0 $ -comprehension. The comprehension is then eliminated in favor of induction using either elimination of monotone Skolem functions (for COH) or Howard's ordinal analysis of bar recursion (for $RT_2^2 $. (shrink)

We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to Gödel and Shoenfield can be used to rewrite proofs performed in these systems into standard ones. These functional interpretations show in particular that our nonstandard systems are conservative extensions of E-HAω and E-PAω, strengthening earlier results by Moerdijk and Palmgren, and Avigad and Helzner. We will also indicate how our rewriting algorithm can be used for term extraction purposes. To (...) conclude the paper, we will point out some open problems and directions for future research, including some initial results on saturation principles. (shrink)

We show how to extract effective bounds Φ for $\bigwedge u^1 \bigwedge v \leq_\gamma tu \bigvee w^\eta G_0$ -sentences which depend on u only (i.e. $\bigwedge u \bigwedge v \leq_\gamma tu \bigvee w \leq_\eta \Phi uG_0$ ) from arithmetical proofs which use analytical assumptions of the form \begin{equation*}\tag{*}\bigwedge x^\delta\bigvee y \leq_\rho sx \bigwedge z^\tau F_0\end{equation*} (γ, δ, ρ, and τ are arbitrary finite types, η ≤ 2, G0 and F0 are quantifier-free, and s and t are closed terms). If τ (...) ≤ 2, (*) can be weakened to $\bigwedge x^\delta, z^\tau\bigvee y \leq_\rho sx \bigwedge \tilde{z} \leq_\tau z F_0$ . This is used to establish new conservation results about weak König's lemma. Applications to proofs in classical analysis, especially uniqueness proofs in approximation theory, will be given in subsequent papers. (shrink)

Logics for ‘generally’ are intended to express some vague notions, such as ‘generally’, ‘several’, ‘many’, ‘most’, etc., by means of the new generalized quantifier ∇ and to reason about assertions with ‘generally’ . We introduce the idea of functional interpretation for ‘generally’ and show that representative functions enable elimination of ∇ and reduce consequence to classical theories. Thus, one can use proof procedures and theorem provers for classical first-order logic to reason about assertions involving ‘generally’.

Gödel's dialectica interpretation of Heyting arithmetic HA may be seen as expressing a lack of confidence in our understanding of unbounded quantification. Instead of formally proving an implication with an existential consequent or with a universal antecedent, the dialectica interpretation asks, under suitable conditions, for explicit 'interpreting' instances that make the implication valid. For proofs in constructive set theory CZF-, it may not always be possible to find just one such instance, but it must suffice to explicitly name (...) a set consisting of such interpreting instances. The aim of eliminating unbounded quantification in favor of appropriate constructive functionals will still be obtained, as our ∧-interpretation theorem for constructive set theory in all finite types CZFω- shows. By changing to a hybrid interpretation ∧q, we show closure of CZFω- under rules that – in stronger forms – have already been studied in the context of Heyting arithmetic. In a similar spirit, we briefly survey modified realizability of CZFω- and its hybrids. Central results of this paper have been proved by Burr 2000a and Schulte 2006, however, for different translations. We use a simplified interpretation that goes back to Diller and Nahm 1974. A novel element is a lemma on absorption of bounds which is essential for the smooth operation of our translation. (shrink)

Gödel's dialectica interpretation of Heyting arithmetic HA may be seen as expressing a lack of confidence in our understanding of unbounded quantification. Instead of formally proving an implication with an existential consequent or with a universal antecedent, the dialectica interpretation asks, under suitable conditions, for explicit ‘interpreting’ instances that make the implication valid. For proofs in constructive set theory CZF‐, it may not always be possible to find just one such instance, but it must suffice to explicitly name (...) a set consisting of such interpreting instances. The aim of eliminating unbounded quantification in favor of appropriate constructive functionals will still be obtained, as our ∧‐interpretation theorem for constructive set theory in all finite types CZFω‐ shows. By changing to a hybrid interpretation ∧q, we show closure of CZFω‐ under rules that – in stronger forms – have already been studied in the context of Heyting arithmetic. In a similar spirit, we briefly survey modified realizability of CZFω‐ and its hybrids. Central results of this paper have been proved by Burr 2000a and Schulte 2006, however, for different translations. We use a simplified interpretation that goes back to Diller and Nahm 1974. A novel element is a lemma on absorption of bounds which is essential for the smooth operation of our translation. (shrink)

Abstract.Carrying out a suggestion by Kreisel, we adapt Gödel’s functional interpretation to ordinary first-order predicate logic(PL) and thus devise an algorithm to extract Herbrand terms from PL-proofs. The extraction is carried out in an extension of PL to higher types. The algorithm consists of two main steps: first we extract a functional realizer, next we compute the β-normal-form of the realizer from which the Herbrand terms can be read off. Even though the extraction is carried out in (...) the extended language, the terms are ordinary PL-terms. In contrast to approaches to Herbrand’s theorem based on cut elimination orɛ-elimination this extraction technique is, except for the normalization step, of low polynomial complexity, fully modular and furthermore allows an analysis of the structure of the Herbrand terms, in the spirit of Kreisel ([13]), already prior to the normalization step. It is expected that the implementation of functional interpretation in Schwichtenberg’s MINLOG system can be adapted to yield an efficient Herbrand-term extraction tool. (shrink)

We will apply the methods developed in the field of ‘proof mining’ to the Bolzano-Weierstraß theorem BW and calibrate the computational contribution of using this theorem in proofs of combinatorial statements. We provide an explicit solution of the Gödel functional interpretation as well as the monotone functional interpretation of BW for the product space Πi ∈ℕ[–ki, ki] . This results in optimal program and bound extraction theorems for proofs based on fixed instances of BW, i.e. (...) for BW applied to fixed sequences in Πi ∈ℕ[–ki, ki]. (shrink)

Gödel interpreted Heyting arithmetic HA in a “logic-free” fragment T 0 of his theory T of primitive recursive functionals of finite types by his famous Dialectica-translation D . This works because the logic of HA is extremely simple. If the logic of the interpreted system is different—in particular more complicated—, it forces us to look for different and more complicated functional translations. We discuss the arising logical problems for arithmetical and set theoretical systems from HA to CZF . We (...) want to test the thesis: While the functionals take care of the proof theoretic strength of the interpreted system, it is the functional translation that has to cope with the logical complexities of the system. (shrink)

There are two different ways to introduce the notion of truthin constructive mathematics. The first one is to use a Tarskian definition of truth in aconstructive (meta)language. According to some authors, (Kreisel, van Dalen, Troelstra ... ),this definition is entirely similar to the Tarskian definition of classical truth (thesis A).The second one, due essentially to Heyting and Kolmogorov, and known as theBrouwer–Heyting–Kolmogorov interpretation, is to explain informally what it means fora mathematical proposition to be constructively proved. According to other (...) authors (Martin-Löfand Shapiro), this interpretation and the Tarskian definition of truth amount to thesame (thesis B). My aim in this paper is to show that thesis A is only reasonable, that thesis Bis false and to answer the following question: what is defined by the Tarskian definition ofconstructive truth? (shrink)

We adapt Streicher and Kohlenbach's proof of the factorization S = KD of the Shoenfield translation S in terms of Krivine's negative translation K and the Gödel functional interpretation D, obtaining a proof of the factorization U = KB of Ferreira's Shoenfield-like bounded functional interpretation U in terms of K and Ferreira and Oliva's bounded functional interpretation B.

In ordinal analysis of impredicative theories so-called collapsing functions are of central importance. Unfortunately, the definition procedure of these functions makes essential use of uncountable cardinals whereas the notation system that they call into being corresponds to a recursive ordinal. It has long been claimed that, instead, one should manage to develop such functions directly on the basis of admissible ordinals. This paper is meant to show how this can be done. Interpreting the collapsing functions as operating directly on admissible (...) sets also renders a new and perspicuous approach to well-ordering proofs possible. MSC: 03F15, 03F35. (shrink)

This article systematically investigates so-called “truth variants” of several functional interpretations. We start by showing a close relation between two variants of modified realizability, namely modified realizability with truth and q-modified realizability. Both variants are shown tobe derived from a single “functional interpretation with truth” of intuitionistic linear logic. This analysis suggests that several functional interpretations have truth and q-variants. These variants, however, require a more involved modification than the ones previously considered. Following this lead we (...) present truth and q-variants of the Diller-Nahm interpretation, the bounded modified realizability and the bounded functional interpretation. (shrink)

This essay discusses the instructional value of mathematical proofs using different interpretations of the analysis cum synthesis method in Apollonius’ Conics as a case study. My argument is informed by Descartes’ complaint about ancient geometers and William Thurston’s discussion on how mathematical understanding is communicated. Three historical frameworks of the analysis/synthesis distinction are used to understand the instructive function of the analysis cum synthesis method: the directional interpretation, the structuralist interpretation, and the phenomenological interpretation. I apply these (...) interpretations to the analysis cum synthesis method in order reveal how the same underlying mathematical activity occurs at different levels of scale: at the level of an individual proof, at the level of a collection of proofs, and at the level of a single line within a proof. On the basis of this investigation, I argue that the instructive value of mathematical proof lies in engendering in the reader the same mathematical activity experienced by the author themselves. (shrink)

This paper is a companion to work of Feferman, Jäger, Glaß, and Strahm on the proof theory of the type two functionals μ and E1 in the context of Feferman-style applicative theories. In contrast to the previous work, we analyze these two functionals in the context of Schlüter's weakened applicative basis PRON which allows for an interpretation in the primitive recursive indices. The proof-theoretic strength of PRON augmented by μ and E1 is measured in terms of the (...) two subsystems of second order arithmetic, Π10-CA and Π11-CA, respectively. (shrink)

Growth of the private sector and privatization of state companies around the world have led to the emergence of various stock markets, some of which are depicted by insider trading. Law literature uses the arguments of unfairness, breach of fiduciary rights and damage to others to define and rule against insider trading. Economic literature can be used to interpret insider trading from other perspectives. This study argues that the question of insider trading in developing markets can be resolved by the (...) extent stock markets generate externalities and are public goods. It advocates structural changes in the developing markets and examines the conditions under which the Coase Theorem would work. (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)

The Born’s rule to interpret the square of wave function as the probability to get a specific value in measurement has been accepted as a postulate in foundations of quantum mechanics. Although there have been so many attempts at deriving this rule theoretically using different approaches such as frequency operator approach, many-world theory, Bayesian probability and envariance, literature shows that arguments in each of these methods are circular. In view of absence of a convincing theoretical proof, recently some researchers (...) have carried out experiments to validate the rule up-to maximum possible accuracy using multi-order interference (Sinha et al, Science, 329, 418 [2010]). But, a convincing analytical proof of Born’s rule will make us understand the basic process responsible for exact square dependency of probability on wave function. In this paper, by generalizing the method of calculating probability in common experience into quantum mechanics, we prove the Born’s rule for statistical interpretation of wave function. (shrink)

The many-worlds interpretation of quantum mechanics is based on three key assumptions: the completeness of the physical description by means of the wave function, the linearity of the dynamics for the wave function, and multiplicity. In this paper, I argue that the combination of these assumptions may lead to a contradiction. In order to avoid the contradiction, we must drop one of these key assumptions.

This paper investigates whether the fundamental linguistic insights and intuitions of Lexical Functional Grammar, which is usually presented as a constraint-based linguistic theory, can be reformulated in a resource sensitive framework using a substructural modal logic. In the approach investigated here, LFG's f-descriptions are replaced with expressions from a multi-modal propositional logic. In effect, the feature structure unification basis of LFG's f-structures is replaced with a very different resource based mechanism. It turns out that some linguistic analyses that required (...) non-monotonic devices in LFG analysis of Icelandic) can be straightforwardly expressed in the framework presented here. Moreover, a Curry– Howard correspondence between proofs in this logic and -terms provides a semantic interpretation as a by-product of the process of showing syntactic well-formedness. (shrink)

Some quantitative results obtained by proof mining take the form of Herbrand disjunctions that may depend on additional parameters. We attempt to elucidate this fact through an extension to first-order arithmetic of the proof of Herbrand’s theorem due to Gerhardy and Kohlenbach which uses the functional interpretation.

Humans' voice offers the widest variety of motor phenomena of any human activity. However, its clinical evaluation in people with movement disorders such as Parkinson's disease lags behind current knowledge on advanced analytical automatic speech processing methodology. Here, we use deep learning-based speech processing to differentially analyze voice recordings in 14 people with PD before and after dopaminergic medication using personalized Convolutional Recurrent Neural Networks and Phone Attribute Codebooks. p-CRNN yields an accuracy of 82.35% in the binary classification of ON (...) and OFF motor states at a sensitivity/specificity of 0.86/0.78. The PAC-based approach's accuracy was slightly lower with 73.08% at a sensitivity/specificity of 0.69/0.77, but this method offers easier interpretation and understanding of the computational biomarkers. Both p-CRNN and PAC provide a differentiated view and novel insights into the distinctive components of the speech of persons with PD. Both methods detect voice qualities that are amenable to dopaminergic treatment, including active phonetic and prosodic features. Our findings may pave the way for quantitative measurements of speech in persons with PD. (shrink)

Natural resources, especially minerals from the earth, are to be protected by humanity. The church, which acts as leaven in the world is called to rise and address the unfriendly mining activities called mining-induced displacement and resettlement. The general theory of interpretation of creation account calls for human stewardship in the world. Humans must view themselves as partners with God in preserving and sustaining the cosmos. The communities had suffered negative socio-economic imbalances. The ekklesia in this cosmic chaos is (...) called upon to fulfil four major functions, namely identity, integration, policy, and management as a way of intervention in communities that are victims of these mining activities. This response, ecclesiology in context, is the combination of theological and social-scientific approaches to the development of practical models and strategies for the church’s interaction with modern society and its challenges. (shrink)

This paper addresses the strength of Ramsey's theorem for pairs ($RT^2_2$) over a weak base theory from the perspective of 'proof mining'. Let $RT^{2-}_2$ denote Ramsey's theorem for pairs where the coloring is given by an explicit term involving only numeric variables. We add this principle to a weak base theory that includes weak König's Lemma and a substantial amount of $\Sigma^0_1$-induction (enough to prove the totality of all primitive recursive functions but not of all primitive recursive functionals). In (...) the resulting theory we show the extractability of primitive recursive programs and uniform bounds from proofs of $\forall\exists$-theorems. There are two components of this work. The first component is a general proof-theoretic result, due to the second author, that establishes conservation results for restricted principles of choice and comprehension over primitive recursive arithmetic PRA as well as a method for the extraction of primitive recursive bounds from proofs based on such principles. The second component is the main novelty of the paper: it is shown that a proof of Ramsey's theorem due to Erdős and Rado can be formalized using these restricted principles. So from the perspective of proof unwinding the computational content of concrete proofs based on $RT^2_2$ the computational complexity will, in most practical cases, not go beyond primitive recursive complexity. This even is the case when the theorem to be proved has function parameters f and the proof uses instances of $RT^2_2$ that are primitive recursive in f. (shrink)

In Prawitz’s semantics, the validity of an argument may be defined, either relatively to an atomic base which determines the meaning of the non-logical terminology, or relatively to the whole class of atomic bases, namely as logical validity. In the first case, which may be qualified as local, one has to choose whether validity of arguments is or not monotonic over expansions of bases, while in the second case, which may be qualified as global, one has to choose whether the (...) reduction functions which justify non-primitive inferences are or not base-depending. I claim that these oppositions enjoy some conceptual symmetries, and that these symmetries may be understood as putting restrictions on one’s choice both at the local and at the global level. This produces two different proof-theoretic semantics in line with Prawitz’s tenets. However, I also argue that the symmetries stem from a deeper interaction within Prawitz’s semantics, i.e. non-logical meanings vs interpretation of rules. This interaction is in turn based on some primitive ingredients which, when suitably combined, produce other two Prawitz-compatible readings. The four readings form a diagram where some order relations hold. I finally claim that this diagram is complete, namely that, if we combine the ingredients in ways other than those giving rise to the four readings above, we obtain nothing new, or nothing compatible with general semantic requirements. Thus, symmetries between the local and the global level, and interaction between non-logical meaning and interpretation of rules, produce a complete classification of potential Prawitzian semantics. (shrink)

The paper briefly surveys the sentential proof-theoretic semantics for fragment of English. Then, appealing to a version of Frege’s context-principle (specified to fit type-logical grammar), a method is presented for deriving proof-theoretic meanings for sub-sentential phrases, down to lexical units (words). The sentential meaning is decomposed according to the function-argument structure as determined by the type-logical grammar. In doing so, the paper presents a novel proof-theoretic interpretation of simple type, replacing Montague’s model-theoretic type interpretation (in (...) arbitrary Henkin models). The domains of derivations are collections of derivations in the associated “dedicated” natural-deduction proof-system, and functions therein (with no appeal to models, truth-values and elements of a domain). The compositionality of the semantics is analyzed. (shrink)

The paper proposes a semantic value for the logical constants (connectives and quantifiers) within the framework of proof-theoretic semantics, basic meaning on the introduction rules of a meaning conferring natural deduction proof system. The semantic value is defined based on Fregecontributions” to sentential meanings as determined by the function-argument structure as induced by a type-logical grammar. In doing so, the paper proposes a novel proof-theoretic interpretation of the semantic types, traditionally interpreted in Henkin models. The compositionality (...) of the resulting attribution of semantic values is discussed. Elsewhere, the same method was used for defining proof-theoretic meaning of subsentential phrases in a fragment of natural language. Doing the same for (the simpler and clearer case of) logic sheds more light on the proposal. (shrink)

In discussions of standards of proof, a familiar perspective often emerges. According to what we call specificationism, standards of proof are legal rules that specify the quantum of evidence required to determine that a litigant’s claim has been proven. In so doing, they allocate the risk of error among litigants (and potential litigants), minimizing the risk of certain types of error. Specificationism is meant as a description of the way the rules actually function. We argue, however, that its (...) claims are either mistaken or at a minimum deeply misleading, especially when it comes to standard of proof rules (SPRs) that contain indeterminate formulas, as is typical. As against specificationism, we argue that SPRs are best understood as rules that confer competence to decide whether a given standard has been met—according to whatever vague or inchoate interpretation (if any) of the rule in question triers of fact implicitly or explicitly employ. We call this the competence-norm approach. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Feminist Studies 41, no. 3. © 2015 by Feminist Studies, Inc. 623 Jaye Cee Whitehead, Kath Bassett, Leia Franchini, and Michael Iacolucci “The Proof Is in the Pudding”: How Mental Health Practitioners View the Power of “Sex Hormones” in the Process of Transition In the United States today, popular discourse touts the power of “sex hormones” and hormone receptors in the brain to chemically produce gender expressions (manifested (...) in physical sex traits, behaviors, and attitudes) and identities (a sense of self as feminine or masculine). These accounts range from common assumptions that Western ideals of femininity (such as empathy understanding, cooperative orientation, nurturing behavior) and masculinity (rational/spatial understanding, competitive orientation, violent behavior) are produced by corresponding sex hormones, to studies that reduce complex gender identities and macrosocial economic phenomena to presocial, binary, hormonal processes.1 For sociologists, accounts that reduce complex identities to internal hormonal reactions are problematic for two primary reasons: first, they are inaccurate because they fail to examine how hormonal reactions are embedded in a complex cultural process of meaning and interpretation; second, they operate as bioreductive ideologies that obscure the social power inherent to the process of gender identity construction. In what follows, we extend both of these insights by examining mental health 1. For an example of a hybrid popular-scientific account of the power of sex hormones to destabilize economic structures, see Jon Coates and Joe Herbert, “Endogenous Steroids and Financial Risk Taking on a London Trading Floor,” Proceedings of the National Academy of Sciences 105, no. 16 (April 2008): 6167–72. 624 Whitehead, Bassett, Franchini, and Iacolucci practitioners’ divergent interpretations of the power of sex hormones in the process of gender transition.2 In doing so, we examine the cultural power of sex hormones in crafting gender identities without reproducing reductionist interpretations of trans embodiment. Perhaps what is most perplexing about the way we speak of sex hormones is that we know it is inaccurate to describe these hormones as sexed; scientists have acknowledged since the 1930s that they are neither sex specific in their function, nor in terms of their location in male or female bodies.3 In her extensive historicization of sex hormones, Anne Fausto-Sterling concludes that it is more accurate to call androgen- and estrogen-based hormones, “steroid hormones” as they have functions that are not confined to corresponding sexed bodies. In fact she urges scientists to “break out of the sex hormone straightjacket” and to look at steroids as just one of a number of components that are important to the creation of sex and gender, including environment and experience.4 Scholars also point to an inextricable link between the chemical operation of hormones and the social process of constructing meaning, both at the level of social interaction and macrocultural constructions of sex categories and gender ideologies.5 While brain organization/activation theory attributes sex and gender differences to hormonal interactions within the developing brain, Fausto-Sterling questions the distinction between activation and organization by pointing out how “the brain can respond to hormonal stimuli with anatomical changes…hormonal systems, after all, respond exquisitely to experience, be it in the form of nutrition, stress, or sexual activity (to name but a few possibilities ).”6 Drawing from Elizabeth Grosz, Fausto-Sterling argues that the power of hormones is best understood according to the model of the 2. “Gender transition” is a controversial phrase, as it implies that transgendered individuals who receive hormone therapy are changing identities. We are only using it for lack of clear alternative phrasing, not because we believe body modifications change gender identities. 3. See Anne Fausto-Sterling, Sexing the Body: Gender Politics and the Construction of Sexuality (New York: Basic Books, 2000); Rebecca Jordan-Young, Brainstorm: The Flaws in the Science of Sex Differences (Cambridge, MA: Harvard University Press, 2010); and Nelly Oudshoorn, Beyond the Natural Body: An Archeology of Sex Hormones (New York: Routledge, 1994). 4. Fausto-Sterling, Sexing the Body, 193–94. 5. Fausto-Sterling, Sexing the Body. 6. Ibid., 232. Whitehead, Bassett, Franchini, and Iacolucci 625 Möbius strip, wherein internal components of the self are always connected to and continuous with outer components such as culture and environment.7 In other... (shrink)

Kohlenbach, U., Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation, Annals of Pure and Applied Logic 64 27–94.We consider uniqueness theorems in classical analysis having the form u ε U, v1, v2 ε Vu = 0 = G→v 1 = v2), where U, V are complete separable metric spaces, Vu is compact in V and G:U x V → is a constructive function.If is proved by arithmetical means from analytical assumptions (...) x εXy ε Yx z ε Z = 0) only , then we can extract from the proof of → an effective modulus of uniqueness, which depends on u, k but not on v1,v2, i.e., u ε U, v1, v2 ε Vu, k εG, G 2-φuk→dv2-itk). Such a modulus φ can e.g. be used to give a finite algorithm which computes the zero of G on Vu with prescribed precision if it exists classically.The extraction of φ uses a proof-theoretic combination of functional interpretation and pointwise majorization. If the proof of → uses only simple instances of induction, then φ is a simple mathematical operation. (shrink)

Since the beginning of human history, there has been no society that did not have any religion. Man meets his need to believe, encoded in his nature by turning to God. God has not left humans alone in their journey on earth, and from time to time, He has intervened in the world through his prophets. The prophethood, which constitutes one of the main subjects of theology, is an important institution in God-human communication. The messengers chosen by God convey to (...) people the information that they received through revelation and offer teachings that will bring them to salvation. The idea of salvation by God when suffering or feeling helpless has driven people to the expectation of a savior. Nearly all religions except Shintoism have the awaited savior belief in the world. Accordingly, the savior will emerge in an environment of chaos where disasters are experienced, and a moral collapse is observed. The expected savior will drive people away from this turmoil, bring them happiness, well-being, and lead them to salvation. Although there is a savior belief in Judaism and Christianity, Muslims claim that the awaited savior in these religions is Muhammad. Muslim thinkers who believe that Muhammad was heralded in previous scripts, tried to find evidence on the subject from the Bible. One of the Islamic scholars who did researches for this purpose is Shamsuddin al-Samarqandi. Shamsuddin Mohammed b. Ashraf al-Husayni al-Samarqandi is an important Turkish-Islamic scholar who lived in Turkestan at the end of the 7th century and the first quarter of the 8th century. Samarqandi is a versatile scholar who produced important works in various fields such as philosophy, logic, mathematics, discussion, debate and astronomy. Shamsuddin al-Samarqandi is one of the eminent scholars who have written his name in the history of science and philosophy with his works. He adopted a critical and analytical style in almost every field, putting the science of logic at the center of his system. His constructive criticisms had an important function in understanding and interpreting the ideas of numerous thinkers, from Greek philosophers to Islamic philosophers and representatives of philosophical theology. In addition to all these, Samarqandi did not hesitate to criticize the Christian and Jewish belief systems, religions such as Sanawiyyah and Zoroastrianism, and the teachings of the naturalist philosophers regarding the relationship between God and the world in the light of rational and scriptural evidence. Samarqandi, who distinguished himself in rational sciences, also showed himself with his background in theology. Due to his exceptional intellectual interest, he analyzes some key concepts and divine codes related to the Bible, making original inferences about the loyalty of Muhammad, the prophet of Islam. Samarqandi interprets some passages of the Torah and the New Testament, which he considers as signs of Muhammad's prophethood, in the axis of language, logic and the rules of shariah, and concludes that Muhammad is the last prophet to be announced. The conceptual framework that he mostly focuses on in this regard contains Mount Paran, Paraklite, comparison with Moses, and the good news given to the Ishmaelites. Samarqandi makes inferences about the environment in which Muhammad appeared, his qualities, and his lineage, based on the aforementioned concepts. Samarqandi also responds to the criticisms raised by the Ahl al-Kitab about the principles, such as the abolition of other religious rules constituting the basis of Muhammad's legitimacy and establishment of Islam instead, and him being a universal prophet. An important privilege of Samarqandi is that he not only grounds his claims on a theoretical scale but also engages in debates with the leaders of the Ahl al-Kitab. Although Samarqandi exhibits a satisfactory analytical attitude in most of his claims, he displays a sophisticated approach based on the method of coercion (ilzām) in some of his claims. Although he adheres to the tradition of beshair al-nubuwwah in general, he gives a different perspective and strong reasoning to the same evidence within the tradition with the effect of his identity as a verifier (muhaqqik). (shrink)

In [15], [16] G. Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peano arithmetic. In particular he proved, using a complicated ε-substitution method (due to W. Ackermann), that for every theorem A (A prenex) of first-order Peano arithmetic PA one can find ordinal recursive functionals Φ A of order type 0 which realize the Herbrand normal form A H of A. Subsequently more perspicuous proofs of this fact via functional interpretation (combined with normalization) and cut-elimination were found. These (...) proofs however do not carry out the no-counterexample interpretation as a local proof interpretation and don't respect the modus ponens on the level of the no-counterexample interpretation of formulas A and A → B. Closely related to this phenomenon is the fact that both proofs do not establish the condition (δ) and--at least not constructively-- (γ) which are part of the definition of an 'interpretation of a formal system' as formulated in [15]. In this paper we determine the complexity of the no-counterexample interpretation of the modus ponens rule for (i) PA-provable sentences, (ii) for arbitrary sentences A, B ∈ L(PA) uniformly in functionals satisfying the no-counterexample interpretation of (prenex normal forms of) A and A → B, and (iii) for arbitrary A, B ∈ L(PA) pointwise in given α( 0 ) -recursive functionals satisfying the no-counterexample interpretation of A and A → B. This yields in particular perspicuous proofs of new uniform versions of the conditions (γ), (δ). Finally we discuss a variant of the concept of an interpretation presented in [17] and show that it is incomparable with the concept studied in [15], [16]. In particular we show that the no-counterexample interpretation of PA n by α( n (ω))-recursive functionals (n ≥ 1) is an interpretation in the sense of [17] but not in the sense of [15] since it violates the condition (δ). (shrink)

In [15], [16] G. Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peano arithmetic. In particular he proved, using a complicated ε-substitution method (due to W. Ackermann), that for every theoremA(Aprenex) of first-order Peano arithmeticPAone can find ordinal recursive functionalsof order type < ε0which realize the Herbrand normal formAHofA.Subsequently more perspicuous proofs of this fact via functional interpretation (combined with normalization) and cut-elimination were found. These proofs however do not carry out the no-counterexample interpretation as alocalproof (...) class='Hi'>interpretation and don't respect the modus ponens on the level of the nocounterexample interpretation of formulasAandA → B. Closely related to this phenomenon is the fact that both proofs do not establish the condition (δ) and—at least not constructively—(γ) which are part of the definition of an ‘interpretation of a formal system’ as formulated in [15]. (shrink)

The subject of this paper is a characterization of the $\Sigma_1$ -definable set functions of Kripke-Platek set theory with infinity and a uniform version of axiom of choice: $KP\omega+(uniform\;AC)$ . This class of functions is shown to coincide with the collection of set functionals of type 1 primitive recursive in a given choice functional and $x\mapsto\omega$ . This goal is achieved by a Gödel Dialectica-style functional interpretation of $KP\omega+(uniform\;AC)$ and a computability proof for the involved functionals.

We obtain an equivalent implicit characterization of Lp Banach spaces that is amenable to a logical treatment. Using that, we obtain an axiomatization for such spaces into a higher order logical system, the kind of which is used in proof mining, a research program that aims to obtain the hidden computational content of mathematical proofs using tools from mathematical logic. As an aside, we obtain a concrete way of formalizing Lp spaces in positive-bounded logic. The axiomatization is followed by (...) a corresponding metatheorem in the style of proof mining. We illustrate its use with the derivation for this class of spaces of the standard modulus of uniform convexity. (shrink)

Hilbert’s program: • Formalize abstract, infinitary, nonconstructive mathematics. • Prove consistency using only finitary methods.