We present a new functional interpretation, based on a novel assignment of formulas. In contrast with Gödel’s functional “Dialectica” interpretation, the new interpretation does not care for precise witnesses of existential statements, but only for bounds for them. New principles are supported by our interpretation, including the FAN theorem, weak König’s lemma and the lesser limited principle of omniscience. Conspicuous among these principles are also refutations of some laws of classical logic. Notwithstanding, we end (...) up discussing some applications of the new interpretation to theories of classical arithmetic and analysis. (shrink)

We prove that the (non-intuitionistic) law of the double negation shift has a bounded functional interpretation with bar recursive functionals of finite type. As an application. we show that full numerical comprehension is compatible with the uniformities introduced by the characteristic principles of the bounded functional interpretation for the classical case.

In this article we study applications of the bounded functional interpretation to theories of feasible arithmetic and analysis. The main results show that the novel interpretation is sound for considerable generalizations of weak König’s Lemma, even in the presence of very weak induction. Moreover, when this is combined with Cook and Urquhart’s variant of the functional interpretation, one obtains effective versions of conservation results regarding weak König’s Lemma which have been so far only obtained (...) non-constructively. (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.

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)

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)

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)

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)

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)

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)

In this paper I draw from Martin Heidegger’s phenomenology of the 1920s to outline some basic features of his theory of intentionality that I believe have not been fully appreciated or utilized, and that allow for both novel and fruitful interventions in questions about meaning, the relationship between mind and the world, and epistemic justification, principally as they appear in John McDowell’s synoptic project in Mind and World. I argue that while elements of McDowell’s picture are ultimately unsatisfying and problematic, (...) much of his conceptual framework can and should be put into dialogue with Heidegger’s, and that in so doing we make available powerful resources for amending the McDowellian account. Moreover, these emendations have attractive implications for his distinctive desiderata. In particular, they provide original conceptions of normativity’s place in nature, of the boundaries of the space of reasons, and of the relationship between the answerability of thought both to the world and to human beings as a rational community. (shrink)

We describe an extension to our quantifier-free computational logic to provide the expressive power and convenience of bounded quantifiers and partial functions. By quantifier we mean a formal construct which introduces a bound or indicial variable whose scope is some subexpression of the quantifier expression. A familiar quantifier is the Σ operator which sums the values of an expression over some range of values on the bound variable. Our method is to represent expressions of the logic as objects in (...) the logic, to define an interpreter for such expressions as a function in the logic, and then define quantifiers as "mapping functions." The novelty of our approach lies in the formalization of the interpreter and its interaction with the underlying logic. Our method has several advantages over other formal systems that provide quantifiers and partial functions in a logical setting. The most important advantage is that proofs not involving quantification or partial recursive functions are not complicated by such notions as "capturing," "bottom," or "continuity." Naturally enough, our formalization of the partial functions is nonconstructive. The theorem prover for the logic has been modified to support these new features. We describe the modifications. The system has proved many theorems that could not previously be stated in our logic. Among them are. (shrink)

This essay explores small “ordinary” experiences of moral harm as problems of social injustice. Starting with two stories, we first argue against a dominant framework of personal responsibility that assigns responsibility to particular blameworthy agents. Instead we sketch an account of why structural responsibility for social harm must be considered, drawing on the work of Iris Marion Young and Pierre Bourdieu. Finally, drawing on Margaret Walker’s notion of moral repair and Christopher Marshall’s interpretation of the parable of the Good (...) Samaritan, we sketch an account of Christian moral responsibility grounded in restorative justice that seeks to address daily experiences of moral harm through the moral repair work of neighbor-love. (shrink)

Metaphor straddles both epistemology and metaphysics. What makes metaphor elusive is intimately bound up in its dual character, a "thing" of the imagination covering both knowledge and reality. Due to its unique position, metaphor is often only understood up to a certain point: we frame it solely as a concern of knowledge or only as a matter of what is. In order to appreciate the impact metaphor has for both of these realms, this paper takes up three constitutive concepts of (...) metaphor (truth, meaning, and reference), and attempts to understand what the content is of each on both sides of the epistemology/metaphysics fence. (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)

The book addresses two main areas of Kant’s theoretical philosophy: the doctrine of transcendental idealism and various central aspects of the arguments from the Metaphysical and Transcendental Deductions, as well as the relation between the deduction argument and idealism. -/- Among the topics covered are the nature of objective validity, the role and function of transcendental logic in relation to general or formal logic, the possibility of contradictory thoughts, the meaning of the Leitfaden at A79 and the unity of cognition, (...) the two-steps-in-one-proof interpretation and categorial instantiation, categorial illusion, Strawson’s transcendental argument, the persistently perplexing question of the derivation of the categories, and the relation between apperception, objectivity, judgement, and idealism. -/- With regard to idealism in particular, the focus is on the metaphysical two-aspect interpretation and its problems, on the merits and demerits of the controversial phenomenalist reading of Kant’s idealism, and on the topic of subjectivism and epistemic humility. -/- In all of the aforementioned topics, the book presents wholly novel interpretations compared to the standard or mainstream interpretations. (shrink)

Most interpreting theories claim that different interpreting types should involve varied processing mechanisms and procedures. However, few studies have examined their underlying differences. Even though some previous results based on quantitative approaches show that different interpreting types yield outputs of varying lexical and syntactic features, the grammatical parsing approach is limited. Language sequences that form without relying on parsing or processing with a specific linguistic approach or grammar excel other quantitative approaches at revealing the sequential behavior of language production. As (...) a non-grammatically-bound unit of language sequences, frequency motif can visualize the local distribution of content and function words, and can also statistically classify languages and identify text types. Thus, the current research investigates the distribution, length and position-dependent properties of frequency motifs across different interpreting outputs in pursuit of the sequential generation behaviors. It is found that the distribution, the length and certain position-dependent properties of the specific language sequences differ significantly across simultaneous interpreting and consecutive interpreting output. The features of frequency motifs manifest that both interpreting output is produced in the manner that abides by the least effort principle. The current research suggests that interpreting types can be differentiated through this type of language sequential unit and offers evidence for how the different task features mediate the sequential organization of interpreting output under different demand to achieve cognitive load minimization. (shrink)

Alternative theories to quantum mechanics motivate important fundamental tests of our understanding and descriptions of the smallest physical systems. Here, using spontaneous parametric downconversion as a heralded single-photon source, we place experimental limits on a class of alternative theories, consisting of classical field theories which result in power-dependent normalized correlation functions. In addition, we compare our results with standard quantum mechanical interpretations of our spontaneous parametric downconversion source over an order of magnitude in intensity. Our data match the quantum mechanical (...) expectations, and do not show a statistically significant dependence on power, limiting quantum mechanics alternatives which require power-dependent autocorrelation functions. (shrink)

This paper argues, on the basis of data from St'át'imcets (Lillooet Salish), for a theory of wide-scope indefinites which is similar, though not identical, to that proposed by Kratzer (1998). I show that a subset of S'át'imcets indefinites takes obligatory wide scope with respect to if-clauses, negation, and modals, and is unable to be distributed over by quantificational phrases. These wide-scope effects cannot be accounted for by movement, but require an analysis involving choice functions (Reinhart 1995, 1997). However, Reinhart's particular (...) choice function analysis is unable to account for the St'át'imcets data. A Kratzer-style theory, on the other hand, accounts not only for the wide-scope effects, but also for the emergence of narrower-than-widest interpretations for indefinites which contain bound variables. I depart from Kratzer's analysis in claiming that St'át'imcets choice function indefinites are not 'specific'; the discourse context does not provide a value for the function variable. Therefore, I utilize wide- scope existential closure over choice functions rather than leaving the variables free. However, my analysis provides support for Kratzer's claim that English indefinites are ambiguous between a choice function interpretation and a quantificational interpretation, since St'át'imcets determiners overtly encode the English ambiguity. I conclude by suggesting that the proposed analysis of wide-scope indefinites may be universally valid. (shrink)

This thesis is concerned with Immanuel Kant's mature philosophy as a whole. My aim is to show the systematic relationship among Kant's three Critiques, and the continuity of these with the Inaugral Dissertation. I use recent interpretations of Kant's projects in the Critique of Pure Reason and I offer my own interpretation of the Critique of Judgment, in which I highlight the importance of the final Appendix in that work, to argue that the goal of these three works taken (...) together is to replace traditional metaphysics with a new approach entirely. In place of the traditional approach in which the principles of metaphysics are supposed to be principles of the objective order of things quite apart from the way they appear to us, Kant argues in favour of a system of subjective principles that he believes will nevertheless allow us to achieve the goals of metaphysics. The new metaphysics will not be knowledge-based, as traditional metaphysics had been. Rather Kant's system is primarily ethics-based. That is, the primary principles of Kant's metaphysical system are those of his rational ethics, which have the function of regulating our activity in, and organization of, the world. Instead of knowledge, ethics, and theology being uneasily coordinated parts of philosophy, as they are in traditional metaphysical systems, all three become integrated within an ethical, and essentially teleological, framework in Kant's system. Showing the role of the Critique of Judgment in bringing about this change, as well as showing the importance of teleology for Kant's philosophy, are both important goals of the thesis. (shrink)

We provide an economic interpretation of the practice consisting in incorporating risk measures as constraints in an expected prospect maximization problem. For what we call the infimum of expectations class of risk measures, we show that if the decision maker (DM) maximizes the expectation of a random prospect under constraint that the risk measure is bounded above, he then behaves as a “generalized expected utility maximizer” in the following sense. The DM exhibits ambiguity with respect to a family (...) of utility functions defined on a larger set of decisions than the original one; he adopts pessimism and performs first a minimization of expected utility over this family, then performs a maximization over a new decisions set. This economic behaviour is called “maxmin under risk” and studied by Maccheroni (Econ Theory 19:823–831, 2002). As an application, we make the link between an expected prospect maximization problem, subject to conditional value-at-risk being less than a threshold value, and a non-expected utility economic formulation involving “loss aversion”-type utility functions. (shrink)

Expressions such as English himself are interpreted as locally bound anaphors in certain syntactic environments and are exempt from the binding conditions in others. This article provides a unified semantics for himself in both of these uses. Their difference is reduced to the interaction with the syntactic environment. The semantics is based on an extension of the treatment of pronominals in variable-free semantics. The adoption of variable free semantics is inspired by the existence of proxy-readings, which motivate an analysis based (...) on Skolem functions. It is explained why certain anaphor types allow proxy-readings whereas others do not. (shrink)

It is pointed out that ordinary quantum mechanics as a classical field theory cannot account for the wave function collapse if it is not seen within the framework of field quantization. That is needed to understand the particle structure of matter during wave function evolution and to explain the collapse as symmetry breakdown by detection. The decay of a two-particle bound s state and the Stern-Gerlach experiment serve as examples. The absence of the nonlocality problem in Bohm’s version of the (...) EPR arrangement favours the approach described. (shrink)

If patriotism can thus be seen as an incentive or as an instigation even in such a recondite science as epistemology, how much more readily can it be seen to perform such functions in other studies more immediately or inextricably bound up with communal human life? I pass over instances that occur to me—for instance, the Victorian Jesuit, Father Hopkins, declaring that every good poem written by an Englishman was a blow struck for England--and profit instead, if I may, by (...) the presence among us of Edward Said. I do not know, and it is none of my business to know, what passport Said presents at the international frontier. But it is surely common knowledge among us that he has deep and feelingful and intimate allegiances to the state of Lebanon. Who of us has failed to connect this with his books Orientalism and The Question of Palestine? The point is that, having made this connection, none of us thinks the worse of Said. On the contrary, we recognize that he has a special stake in such topics and therefore speaks on them with a special authority. Unless I am mistaken, that stake and that authority are, in a perhaps extended sense, patriotic. And whatever our speculative objections to the idea and the principle of patriotism, in practice we recognize it and we honour it.What I am questioning, it will now be plain, is the principle of "disinterest." "The disinterested pursuit of knowledge"—it is what in our distinct disciplines all of us have paid lip-service to, and perhaps more than lip-service. But when we come right down to it, is it what we believe? The honest patriot declares an interest; and if we are wise, we take note of the declaration, making allowances and reserving doubts accordingly. But what are we to make of the scholar who declares no interest, who claims implicitly to be truly disinterested. Can we believe him? And if we cannot, what guidance do we have as to what reservations to make, what doubts to entertain? I am of one mind with my Marxist colleagues who, from a political position very far from mine, warn us to be especially suspicious of the scholar who claims to have no axe to grind. We, all of us, have axes to grind; the crucial distinction is between those who know this about themselves and those who don't.Let me make myself clear. When I urge that the terms "patriotism" and "patriotic" be reinstated in our discourse, and particularly in those forms of our discourse that may be called "interpretation," I do not imply that patriotism is a nobler, a more elevated instigation than sundry others, mostly ideological, of which we are more aware. The point is precisely that of these others we are aware because we share a vocabulary which acknowledges them, whereas "patriotic" has been banished from our vocabulary, and so the reality which the word represents is left out of our calculations. Let me admit for the sake of argument what I do not in fact believe-- that patriotism is a concept and a sentiment so besmirched by the unholy uses made of it that, if mankind is to survive, patriotism will have to be eradicated. Even if that were the case, it remains true that patriotic interest and incitement are very far from having been eradicated from the world that we in fact inhabit, and try to interpret, here and now; and if we try to work within a vocabulary that pretends otherwise, we condemn ourselves to producing interpretations that are drastically partial and perhaps disastrously misleading. The point is not whether patriotism is a good thing or a bad thing but simply that it is; it exists, as powerful factor which we all in our hearts acknowledge even as our vocabulary refuses to. And when we speak in this context of "the world," we certainly include in that world ourselves, who offer to interpret it. Every one of our interpretations is coloured by the fact that we, the several interpreters, are British or American, French or Italian or Russian or whatever. If we think otherwise, we deceive ourselves; and yet where, in any of our currently acceptable vocabularies, determined as all of them are by the glib rationalism of the Enlightenment, do we find that momentous fact about ourselves acknowledged? Where is it acknowledged, for instance, in the vocabulary of feminism that "woman," as conceived by an American writing about Italians, cannot help but be significantly different from "woman" as conceived by an Italian looking at Americans? Or again, an Italian woman may well, we must suppose, be an Italian patriot; but where, in the current vocabulary of feminists, is that dimension of her "woman-ness" allowed for? Let it be acknowledged only so as to be deplored; but let it in any event be acknowledged. At the moment, it isn't.Donald A. Davie, the distinguished poet, is Andrew W. Mellon Professor of the Humanities at Vanderbilt University and honorary fellow of Saint Catharine's College, Cambridge and of Trinity College, Dublin. He has edited The New Oxford Book of Christian Verse, and his Collected Poems 1950-1970 appeared in 1972. His latest publications are Dissentient Voice and These the Companions; Recollections. (shrink)

The wavefunction is the central mathematical entity of quantum mechanics, but it still lacks a universally accepted interpretation. Much effort is spent on attempts to probe its fundamental nature. Here I investigate the consequences of a matter ontology applied to spherical masses of constant bulk density. The governing equation for the center-of-mass wavefunction is derived and solved numerically. The ground state wavefunctions and resulting matter densities are investigated. A lowering of the density from its bulk value is found for (...) low masses due to increased spatial spreading. A discussion of the possibility to experimentally observe these effects is given and the possible consequences for choosing an ontological interpretation for quantum mechanics are commented upon. (shrink)

The function of law and of constitutional law is to make determinate what we ought to do. And in constitutional law, that is true of both structural provisions and rights provisions. It is not the function of constitutions to establish our real moral rights. We possess those independently of the constitution, which cannot affect them. And all organs of government are bound morally if not legally by those rights. I have taken no position on the relative competence of legislatures and (...) courts to ascertain the content of real moral rights, and it is possible that the judiciary is well-equipped to be our wise Platonic guardians. However, if the game is interpretation, all that can be interpreted are authored rules, and what those rules mean can only be what their authors meant by them. Anything else is reauthoring—that is, creating new rules. There is no “living tree” constitutional interpretation. The only “living trees” are the judges. So you’d better hope that they are well cultivated. And you may conclude that a bit of pruning is in order. (shrink)

This paper focuses on a constructive treatment of the mathematical formalism of quantum theory and a possible role of constructivist philosophy in resolving the foundational problems of quantum mechanics, particularly, the controversy over the meaning of the wave function of the universe. As it is demonstrated in the paper, unless the number of the universe’s degrees of freedom is fundamentally upper bounded or hypercomputation is physically realizable, the universal wave function is a non-constructive entity in the sense of constructive (...) recursive mathematics. This means that even if such a function might exist, basic mathematical operations on it would be undefinable and subsequently the only content one would be able to deduce from this function would be pure symbolical. (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)

It is shown that functional interpretation can be used to show the existence property of intuitionistic number theory. On the basis of truth variants a comparison is then made between realisability and functional interpretation showing a structural difference between the two.

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)

As a result of these restrictions, an implementation of L [subscript lambda] does not need to implement full higher-order unification. Instead, an extension to first-order unification that respects bound variable names and scopes is all that is required. Such unification problems are shown to be decidable and to possess most general unifiers when unifiers exist. A unification algorithm and logic programming interpreter are described and proved correct. Several examples of using L[subscript lambda] as a meta-programming language are presented.

In the present paper we give a functional interpretation of Aczel's constructive set theories CZF − and CZF in systems T ∈ and T ∈ + of constructive set functionals of finite types. This interpretation is obtained by a translation × , a refinement of the ∧ -translation introduced by Diller and Nahm 49–66) which again is an extension of Gödel's Dialectica translation. The interpretation theorem gives characterizations of the definable set functions of CZF − and (...) CZF in terms of constructive set functionals. In a second part we introduce constructive set theories in all finite types. We expand the interpretation to these theories and give a characterization of the translation × . We further show that the simplest non-trivial axiom of extensionality is not interpretable by functionals of T ∈ and T ∈ + . We obtain this result by adapting Howard's notion of hereditarily majorizable functionals to set functionals. Subject of the last section is the translation ∨ that is defined in Burr for an interpretation of Kripke-Platek set theory with infinity. (shrink)

We are concerned with showing how ‘labelled’ Natural Deduction presentation systems based on an extension of the so-called Curry-Howard functional interpretation can help us understand and generalise most of the deduction calculi designed to deal with the logical notion of existential quantification. We present the labelling mechanism for ‘’ using what we call ‘ɛ-terms’, which have the form of ‘a’) in a dual form to the ‘Ax.f’ terms of in the sense that the ‘witness’ is chosen at the (...) time of assertion/introduction.With the intention of demonstrating the generality of our framework, we provide a brief comparison with some other calculi of existentials, including the model-theoretic interpretations of Skolem and Herbrand, indicating the way in which some of the classical results on prenex normal forms can be extended to a wide range of logics. The essential ingredient is to look at the conceptual framework of labelled natural deduction as an attempted reconstruction of Frege's functional calculus where the devices of the Begriffsschrift work separately from, yet in harmony with, those of the Grundgesetze 1. (shrink)

Extending Gödel's Dialectica interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.

What is the point of appealing to a social contract? An intuitively plausible answer is that the metaphor functions as a justification for the obligation to obey the law. If I have made a contract to establish a political authority, then I am bound to obey the commands of that authority. In a contract, my agreement creates an obligation to perform. Then only remaining question is what reasons I have to make the agreement in the first place. It would then (...) seem that classical social contract theory is divided between those who understand our reasons to agree as prudential and those who take our reasons to be moral. But this kind of interpretation fails to make sense of Kant’s political theory, which understands our obligation to enter into a civil condition as prior to the appeal to the social contract. The original contract enters into Kant’s theory at a crucially later point, after the creation of specific political institutions. It functions as a way of reconciling these institutions with the idea of rightful coercion, by imposing normative requirements on the political reasoning of legislators and citizens. For Kant, the distinctive feature of normative political reasoning is the notion of a unified will, an idea that was already present at the start of social contract theory in Hobbes, but had yet to be properly clarified. Kant appeals to the original contract not to ground our political obligations, but to explain both the coherence and the necessity of the idea of a common will for political argument. (shrink)

This book gives a detailed treatment of functional interpretations of arithmetic, analysis, and set theory. The subject goes back to Gödel's Dialectica interpretation of Heyting arithmetic which replaces nested quantification by higher type operations and thus reduces the consistency problem for arithmetic to the problem of computability of primitive recursive functionals of finite types. Regular functional interpretations, i.e. Dialectica and Diller-Nahm interpretation as well as Kreisel's modified realization, together with their Troelstra-style hybrids, are applied to constructive (...) as well as classical systems of arithmetic, analysis, and set theory. They yield relative consistency and conservativity results and closure under relevant rules of the theories in question as well as axiomatic characterizations of the functional translations. Prerequisites are: familiarity with classical and intuitionistic predicate logic, basics of computability theory, Gödel's incompleteness theorems. (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’.

Understanding the functional mechanisms underlying genetic signals associated with complex traits and common diseases, such as cancer, diabetes and Alzheimer's disease, is a formidable challenge. Many genetic signals discovered through genome‐wide association studies map to non‐protein coding sequences, where their molecular consequences are difficult to evaluate. This article summarizes concepts for the systematic interpretation of non‐coding genetic signals using genome annotation data sets in different cellular systems. We outline strategies for the global analysis of multiple association intervals and (...) the in‐depth molecular investigation of individual intervals. We highlight experimental techniques to validate candidate (potential causal) regulatory variants, with a focus on novel genome‐editing techniques including CRISPR/Cas9. These approaches are also applicable to low‐frequency and rare variants, which have become increasingly important in genomic studies of complex traits and diseases. There is a pressing need to translate genetic signals into biological mechanisms, leading to prognostic, diagnostic and therapeutic advances. (shrink)

Some evolutionary psychologists contend that the best way to discover the functions of our present psychological systems is by appealing to the notion of functional mesh, that is, the assumed tight fit between a trait's design and the adaptive problem it is supposed to solve. In this paper, I argue that there exist theoretical considerations and empirical evidence that undermine this assumption of optimal design. Instead, I suggest that cognitive systems are constrained by what I call bounded functionality. (...) This proposal makes use of Jacob's (1977) notion of evolution as a bricoleur and Simon's (1981) idea that problems can have ``satisficing'' solutions. Functional mesh will thus be shown to neglect constraints that are necessary to explain the evolution of psychological mechanisms. (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)