The Ω\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Omega $$\end{document}-rule was introduced by W. Buchholz to give an ordinal-free proof of cut-elimination for a subsystem of analysis with Π11\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Pi ^{1}_{1}$$\end{document}-comprehension. W. Buchholz’s proof provides cut-free derivations by familiar rules only for arithmetical sequents. When second-order quantifiers are present, they are introduced by the Ω\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Omega $$\end{document}-rule and some residual cuts (...) are not eliminated. In the present paper, we introduce an extension of the Ω\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Omega $$\end{document}-rule and prove the complete cut-elimination by the same method as W. Buchholz: any derivation of arbitrary sequent is transformed into its cut-free derivation by the standard rules. In fact we treat the subsystem of Π11\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Pi ^{1}_{1}$$\end{document}-CA that W. Buchholz used for his explanation of G. Takeuti’s finite reductions. Extension to full Π11\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Pi ^{1}_{1}$$\end{document}-CA is planned for another paper. (shrink)

We describe a short model-theoretic proof of an extended normal form theorem for derivations in predicate logic which implies in PRA a normal form theorem for the arithmetic derivations . Consider the Gentzen-type formulation of predicate logic with invertible rules. A derivation with proper variables is one where a variable b can occur in the premiss of an inference L but not below this premiss only in the case when L is () or () and b is its eigenvariable. Free (...) variables of such derivation are eigenvariables and free variables of its last sequent. Then any sequent derivable in predicate logic has a cut-free derivation with proper variables where the main formula of any antecedent rule is underivable. The proof is by a simple modification of the construction of a countermodel of the formula from the open branch of its canonical proof-search tree. It extends to intuitionistic and higher order systems. The proof of the corresponding normalization theorem outlined in [8] uses the passage to the infinitary derivations enriched by finitary derivations. The normal form after a modification to make it decidable can be considered as a realization of Gentzen's idea stated at the end of [2], that his notion of reduction for arithmetic can be extended to other fields of mathematics. (shrink)

We present a general schema of easy normalization proofs for finite systems S like first-order arithmetic or subsystems of analysis, which have good infinitary counterparts S ∞ . We consider a new system S ∞ + with essentially the same rules as S ∞ but different derivable objects: a derivation d∈S ∞ + of a sequent Γ contains a derivation Φ∈S of Γ . Three simple conditions on Φ including a normal form theorem for S ∞ + easily imply a (...) weak normalization theorem for S . We give three examples of application of this schema. First, we take S≡PA but restrict the attention to derivations of Σ 1 0 -sentences. In this case it is possible to take S ∞ + to be essentially standard formulation of PA ∞ . Next, we illustrate extension to subsystems of analysis and consider the system BI 1 ∗ of W. Buchholz having the strength of ID 1 , again for derivations of Σ 1 0 -sentences. Finally, we return to the first-order arithmetic to illustrate changes needed to treat derivations of arbitrary formulas. (shrink)

Intuitionistic logic is presented here as part of familiar classical logic which allows mechanical extraction of programs from proofs. to make the material more accessible, basic techniques are presented first for propositional logic; Part II contains extensions to predicate logic. This material provides an introduction and a safe background for reading research literature in logic and computer science as well as advanced monographs. Readers are assumed to be familiar with basic notions of first order logic. One device for making this (...) book short was inventing new proofs of several theorems. The presentation is based on natural deduction. The topics include programming interpretation of intuitionistic logic by simply typed lambda-calculus (Curry-Howard isomorphism), negative translation of classical into intuitionistic logic, normalization of natural deductions, applications to category theory, Kripke models, algebraic and topological semantics, proof-search methods, interpolation theorem. The text developed from materal for several courses taught at Stanford University in 1992-1999. (shrink)

Several proof-theoretic notions of validity have been proposed in the literature, for which completeness of intuitionistic logic has been conjectured. We define validity for intuitionistic propositional logic in a way which is common to many of these notions, emphasizing that an appropriate notion of validity must be closed under substitution. In this definition we consider atomic systems whose rules are not only production rules, but may include rules that allow one to discharge assumptions. Our central result shows that Harrop’s (...) class='Hi'>rule is valid under substitution, which refutes the completeness conjecture for intuitionistic logic. (shrink)

A survey of works on automatic theorem-proving in the ussr 1964-1970. the philosophical problems are not touched.

Building on previous work by Mints, Buchholz and Schwichtenberg, a simplified version of continuous normalization for the untyped λ-calculus and Gödel’s is presented and analysed in the coalgebraic framework of non-wellfounded terms with so-called repetition constructors.The primitive recursive normalization function is uniformly continuous w.r.t. the natural metric on non-wellfounded terms. Furthermore, the number of necessary repetition constructors is locally related to the number of reduction steps needed to reach the normal form and its size.It is also shown how continuous normal (...) forms relate to derivations of strong normalizability in the typed λ-calculus and how this leads to new bounds for the sum of the height of the reduction tree and the size of the normal form.Finally, the methods are extended to an infinitary λ-calculus with ω-rule and permutative conversions and this is used to derive a strong form of normalization for an iterative version of Gödel’s system , leading to a value table semantics for number-theoretic functions. (shrink)

We present a survey of proof theory in the USSR beginning with the paper by Kolmogorov [1925] and ending (mostly) in 1969; the last two sections deal with work done by A. A. Markov and N. A. Shanin in the early seventies, providing a kind of effective interpretation of negative arithmetic formulas. The material is arranged in chronological order and subdivided according to topics of investigation. The exposition is more detailed when the work is little known in the West or (...) the original presentation can be improved using notions or results which appeared later. This includes such topics as Novikov's cut-elimination method (regular formulas) and Maslov's inverse method for the predicate logic. (shrink)

In an incendiary 2010 Nature article, M. A. Nowak, C. E. Tarnita, and E. O. Wilson present a savage critique of the best-known and most widely used framework for the study of social evolution, W. D. Hamilton’s theory of kin selection. More than a hundred biologists have since rallied to the theory’s defence, but Nowak et al. maintain that their arguments ‘stand unrefuted’. Here I consider the most contentious claim Nowak et al. defend: that Hamilton’s rule, the core explanatory (...) principle of kin selection theory, ‘almost never holds’. I first distinguish two versions of Hamilton’s rule in contemporary theory: a special version (HRS) that requires restrictive assumptions, and a general version (HRG) that does not. I then show that Nowak et al. are most charitably construed as arguing that HRS almost never holds, while HRG buys its generality at the expense of explanatory power. While their arguments against HRS are fairly uncontroversial, their arguments against HRG are more contentious, yet these have been largely overlooked in the ensuing furore. I consider the arguments for and against the explanatory value of HRG, with a view to assessing what exactly is at stake in the debate. I suggest that the debate hinges on issues concerning the causal interpretability of regression coefficients, and concerning the explanatory function Hamilton’s rule is intended to serve. (shrink)

According to Brad Hooker's rule-consequentialism, as well as ordinary moral prohibitions against lying, stealing, killing, and harming others, the optimific code will include an over-riding “prevent disaster clause”. This paper explores two issues related to the disaster clause. The first issue is whether the disaster clause is vague—and whether this is a problem for rule-consequentialism. I argue that on Hooker's rule-consequentialism, there will be cases where it is indeterminate whether a given outcome counts as a disaster such (...) that it is permissible to infringe a given prohibition to avoid that outcome. I argue that it counts in favour of Hooker's rule-consequentialism that it makes this space for vagueness. The second issue is how to understand the disaster clause so that it does not make rule-consequentialism intolerably demanding—and more particularly whether avoiding over-demandingness requires the rule-consequentialist to place a counterintuitive limit on requirements to aid. I will argue that rule-consequentialism can avoid over-demandingness without placing a counterintuitive limit on requirements to aid. (shrink)

Ackermann proved termination for a special order of reductions in Hilbert's epsilon substitution method for the first order arithmetic. We establish termination for arbitrary order of reductions.

Many professional football clubs in Europe have youth academies. The business model of such academies is that a club invests resources in training a player and then, when the player is old enough to sign an adult contract, either sells the player or offers him an adult contract. According to Fédération Internationale De Football Association (FIFA), international transfers of players are only permitted if the player is over the age of 18. There are five exceptions to this rule. One (...) of them is that if the player is between 16 and 18 and the transfer takes place within the territory of the European Economic Area (EEA), then an international transfer is allowed. This article is a discussion of the FIFA rules that mandate non-uniform age limits for when players can first transfer to clubs within the EEA area. The conclusion of the article is that FIFA is morally unjustified in setting a higher minimum age for transfer to EEA clubs for non-EEA players than for EEA players. The article first develops an argument for its conclusion. It then discusses, and rejects, the five best objections to this argument. (shrink)

Dynamic topological logic provides a context for studying the confluence of the topological semantics for S4, topological dynamics, and temporal logic. The topological semantics for S4 is based on topological spaces rather than Kripke frames. In this semantics, □ is interpreted as topological interior. Thus S4 can be understood as the logic of topological spaces, and □ can be understood as a topological modality. Topological dynamics studies the asymptotic properties of continuous maps on topological spaces. Let a dynamic topological system (...) be a topological space X together with a continuous function f. f can be thought of in temporal terms, moving the points of the topological space from one moment to the next. Dynamic topological logics are the logics of dynamic topological systems, just as S4 is the logic of topological spaces. Dynamic topological logics are defined for a trimodal language with an S4-ish topological modality □ , and two temporal modalities, ○ and * , both interpreted using the continuous function f. In particular, ○ expresses f’s action on X from one moment to the next, and * expresses the asymptotic behaviour of f. (shrink)

Dynamic topological logic provides a context for studying the confluence of the topological semantics for S4, topological dynamics, and temporal logic. The topological semantics for S4 is based on topological spaces rather than Kripke frames. In this semantics, □ is interpreted as topological interior. Thus S4 can be understood as the logic of topological spaces, and □ can be understood as a topological modality. Topological dynamics studies the asymptotic properties of continuous maps on topological spaces. Let a dynamic topological system (...) be a topological space X together with a continuous function f. f can be thought of in temporal terms, moving the points of the topological space from one moment to the next. Dynamic topological logics are the logics of dynamic topological systems, just as S4 is the logic of topological spaces. Dynamic topological logics are defined for a trimodal language with an S4-ish topological modality □, and two temporal modalities, ○ and *, both interpreted using the continuous function f. In particular, ○ expresses f’s action on X from one moment to the next, and * expresses the asymptotic behaviour of f. (shrink)

Gupta’s Rule of Revision theory of truth builds on insights to be found in Martin and Woodruff and Kripke in order to permanently deepen our understanding of truth, of paradox, and of how we work our language while our language is working us. His concept of a predicate deriving its meaning by way of a Rule of Revision ought to impact significantly on the philosophy of language. Still, fortunately, he has left me something to.

We consider HA*, that is Heyting's Arithmetic extended with transfinite induction over all recursive well orderings, which may be viewed as defining constructive truth, since PA* agrees with classical truth. We prove that Markov's Principle, as a schema, is not provable in HA*, but that HA* is closed under Markov's Rule.

Mathematical game theory has been embraced by a variety of scholars: social scientists, biologists, linguists, and now, increasingly, logicians. This volume illustrates the recent advances of game theory in the field. Logicians benefit from things like game theory's ability to explain informational independence between connectives; meanwhile, game theorists have even begun to benefit from logical epistemic analyses of game states. In concert with such pioneering work, this volume also present surprising developments in classical fields, including first-order logic and set theory.

We put together several observations on constructive negation. First, Russell anticipated intuitionistic logic by clearly distinguishing propositional principles implying the law of the excluded middle from remaining valid principles. He stated what was later called Peirce’s law. This is important in connection with the method used later by Heyting for developing his axiomatization of intuitionistic logic. Second, a work by Dragalin and his students provides easy embeddings of classical arithmetic and analysis into intuitionistic negationless systems. In the last section, we (...) present in some detail a stepwise construction of negation which essentially concluded the formation of the logical base of the Russian constructivist school. Markov’s own proof of Markov’s principle (different from later proofs by Friedman and Dragalin) is described. (shrink)

This paper presents a formulation and completeness proof of the resolution-type calculi for the first order fragment of Girard's linear logic by a general method which provides the general scheme of transforming a cutfree Gentzen-type system into a resolution type system, preserving the structure of derivations. This is a direct extension of the method introduced by Maslov for classical predicate logic. Ideas of the author and Zamov are used to avoid skolomization. Completeness of strategies is first established for the Gentzen-type (...) system, and then transferred to resolution. The propositional resolution system was implemented by T. Tammet. (shrink)

S4C is a logic of continuous transformations of a topological space. Cut elimination for it requires new kind of rules and new kinds of reductions.

Two readings of Wittgenstein's rule-following paradox dominate the literature: either his arguments lead to skepticism, and thus to the view that only a deflated account of meaning is available, or they lead to quietism, and thus to the view that no philosophical account of meaning is called for. I argue, against both these positions, that a proper diagnosis of the paradox points the way towards a constructive, non-sceptical account of meaning.

Bergmann’s rule and Allen’s rule played important roles in mid-twentieth century discussions of adaptation, variation, and geographical distribution. Although inherited from the nineteenth-century natural history tradition these rules gained significance during the consolidation of the modern synthesis as evolutionary theorists focused attention on populations as units of evolution. For systematists, the rules provided a compelling rationale for identifying geographical races or subspecies, a function that was also picked up by some physical anthropologists. More generally, the rules provided strong (...) evidence for adaptation by natural selection. Supporters of the rules tacitly, or often explicitly, assumed that the clines described by the rules reflected adaptations for thermoregulation. This assumption was challenged by the physiologists Laurence Irving and Per Scholander based on their arctic research conducted after World War II. Their critique spurred a controversy played out in a series of articles in Evolution, in Ernst Mayr’s Animal Species and Evolution, and in the writings of other prominent evolutionary biologists and physical anthropologists. Considering this episode highlights the complexity and ambiguity of important biological concepts such as adaptation, homeostasis, and self-regulation. It also demonstrates how different disciplinary orientations and styles of scientific research influenced evolutionary explanations, and the consequent difficulties of constructing a truly synthetic evolutionary biology in the decades immediately following World War II. (shrink)

We present a cut-elimination proof for simple type theory with an axiom of choice formulated in the language with an epsilon-symbol. The proof is modeled after Takahashi's proof of cut-elimination for simple type theory with extensionality. The same proof works when types are restricted, for example for second-order classical logic with an axiom of choice.

A predicate extension SQHT= of the logic of here-and-there was introduced by V. Lifschitz, D. Pearce, and A. Valverde to characterize strong equivalence of logic programs with variables and equality with respect to stable models. The semantics for this logic is determined by intuitionistic Kripke models with two worlds with constant individual domain and decidable equality. Our sequent formulation has special rules for implication and for pushing negation inside formulas. The soundness proof allows us to establish that SQHT= is a (...) conservative extension of the logic of weak excluded middle with respect to sequents without positive occurrences of implication. The completeness proof uses a non-closed branch of a proof search tree. The interplay between rules for pushing negation inside and truth in the “there” world of the resulting Kripke model can be of independent interest. We prove that existence is definable in terms of remaining connectives. (shrink)

Patricia Crone's _God's Rule_ is a fundamental reconstruction and analysis of Islamic political thought focusing on its intellectual development during the six centuries from the rise of Islam to the Mongol invasions. Based on a wide variety of primary sources--including some not previously considered from the point of view of political thought--this is the first book to examine the medieval Muslim answers to questions crucial to any Western understanding of Middle Eastern politics today, such as why states are necessary, what (...) functions they are meant to fulfill, and whether or why they must be based on religious law. The character of Muslim political thought differs fundamentally from its counterpart in the West. The Christian West started with the conviction that truth (both cognitive and moral) and political power belonged to separate spheres. Ultimately, both power and truth originated with God, but they had distinct historical trajectories and regulated different aspects of life. The Muslims started with the opposite conviction: truth and power appeared at the same time in history and regulated the same aspects of life. In medieval Europe, the disagreement over the relationship between religious authority and political power took the form of a protracted controversy regarding the roles of church and state. In the medieval Middle East, religious authority and political power were embedded in a single, divinely sanctioned Islamic community--a congregation and state made one. The disagreement, therefore, took the form of a protracted controversy over the nature and function of the leadership of Islam itself. Crone makes Islamic political thought accessible by relating it to the contexts in which it was formulated, analyzing it in terms familiar to today's reader, and, where possible, comparing it with medieval European and modern political thought. By examining the ideological point of departure for medieval Islamic political thought, Crone provides an invaluable foundation for a better understanding of contemporary Middle Eastern politics and current world events. (shrink)

Brad Hooker’s rule-consequentialism and T.M. Scanlon’s contractualism have been some of the most debated ethical theories in normative ethics during the last twenty years or so. This article suggests that these theories can be compared at two levels. Firstly, what are the deep, structural differences between the rule-consequentialist and contractualist frameworks in which Hooker and Scanlon formulate their views? Secondly, what are the more superficial differences between Hooker’s and Scanlon’s formulations of these theories? Based on exploring these questions (...) and several purported differences between Hooker’s and Scanlon’s views, this article argues that, at the structural level, the two theories are more similar than previous recognised. It suggests that there is only one candidate for a deeper difference and even it may not be that significant. This insight sheds new light on both contractualism and rule-consequentialism, and it will also help us to formulate better versions of the views. (shrink)

Ackermann proved termination for a special order of reductions in Hilbert's epsilon substitution method for the first order arithmetic. We establish termination for arbitrary order of reductions.

In the 1950s, Alan Turing proposed his influential test for machine intelligence, which involved a teletyped dialogue between a human player, a machine, and an interrogator. Two readings of Turing's rules for the test have been given. According to the standard reading of Turing's words, the goal of the interrogator was to discover which was the human being and which was the machine, while the goal of the machine was to be indistinguishable from a human being. According to the literal (...) reading, the goal of the machine was to simulate a man imitating a woman, while the interrogator – unaware of the real purpose of the test – was attempting to determine which of the two contestants was the woman and which was the man. The present work offers a study of Turing's rules for the test in the context of his advocated purpose and his other texts. The conclusion is that there are several independent and mutually reinforcing lines of evidence that support the standard reading, while fitting the literal reading in Turing's work faces severe interpretative difficulties. So, the controversy over Turing's rules should be settled in favor of the standard reading. (shrink)

Probabilities in quantum theory are traditionally given by Born’s rule as the expectation values of projection operators. Here it is shown that Born’s rule is insufficient in universes so large that they contain identical multiple copies of observers, because one does not have definite projection operators to apply. Possible replacements for Born’s rule include using the expectation value of various operators that are not projection operators, or using vari-.

Patricia Crone's _God's Rule_ is a fundamental reconstruction and analysis of Islamic political thought focusing on its intellectual development during the six centuries from the rise of Islam to the Mongol invasions. Based on a wide variety of primary sources -- including some not previously considered from the point of view of political thought -- this is the first book to examine the medieval Muslim answers to questions crucial to any Western understanding of Middle Eastern politics today, such as why (...) states are necessary, what functions they are meant to fulfill, and whether or why they must be based on religious law. The character of Muslim political thought differs fundamentally from its counterpart in the West. The Christian West started with the conviction that truth and political power belonged to separate spheres. Ultimately, both power and truth originated with God, but they had distinct historical trajectories and regulated different aspects of life. The Muslims started with the opposite conviction: truth and power appeared at the same time in history and regulated the same aspects of life. In medieval Europe, the disagreement over the relationship between religious authority and political power took the form of a protracted controversy regarding the roles of church and state. In the medieval Middle East, religious authority and political power were embedded in a single, divinely sanctioned Islamic community -- a congregation and state made one. The disagreement, therefore, took the form of a protracted controversy over the nature and function of the leadership of Islam itself. Crone makes Islamic political thought accessible by relating it to the contexts in which it was formulated, analyzing it in terms familiar to today's reader, and, where possible, comparing it with medieval European and modern political thought. By examining the ideological point of departure for medieval Islamic political thought, Crone provides an invaluable foundation for a better understanding of contemporary Middle Eastern politics and current world events. (shrink)

We present a new experimental approach using a three-path interferometer and find a tighter empirical upper bound on possible violations of Born’s Rule. A deviation from Born’s rule would result in multi-order interference. Among the potential systematic errors that could lead to an apparent violation we specifically study the nonlinear response of our detectors and present ways to calibrate this error in order to obtain an even better bound.

Chapter 5 addresses the provisional morality of the Treatise on the Emendation of the Intellect (TIE). The young Spinoza proposes that even as one works at emending the intellect, one should live by certain rules, which one must assume to be good. One should accommodate ordinary ways of speaking and living to the extent that one can without compromising one’s project. One should enjoy pleasures in moderation. Finally, one should seek instrumental goods only insofar as they are necessary for health (...) and social acceptability. In order to explain shifts in Spinoza’s views about the way that individuals should live while pursuing the good, the chapter traces developments in his accounts of ideas and of the relationship between the philosopher and society. (shrink)

It is proved that Ackermann’s rule δ is admissible in a wide spectrum of relevant logics satisfying certain syntactical properties.

Richard Jeffrey's generalization of Bayes' rule of conditioning follows, within the theory of belief functions, from Dempster's rule of combination and the rule of minimal extension. Both Jeffrey's rule and the theory of belief functions can and should be construed constructively, rather than normatively or descriptively. The theory of belief functions gives a more thorough analysis of how beliefs might be constructed than Jeffrey's rule does. The inadequacy of Bayesian conditioning is much more general than (...) Jeffrey's examples of uncertain perception might suggest. The ``parameter α '' that Hartry Field has introduced into Jeffrey's rule corresponds to the "weight of evidence" of the theory of belief functions. (shrink)