It is well known that Nash equilibria may not be Pareto-optimal; worse, a unique Nash equilibrium may be Pareto-dominated, as in Prisoners’ Dilemma. By contrast, we prove a previously conjectured result: every finite normal-form game of complete information and common knowledge has at least one Pareto-optimal nonmyopic equilibrium (NME) in pure strategies, which we define and illustrate. The outcome it gives, which depends on where play starts, may or may not coincide with that given by a Nash equilibrium. (...) We use some simple examples to illustrate properties of NMEs—for instance, that NME outcomes are usually, though not always, maximin—and seem likely to foster cooperation in many games. Other approaches for analyzing farsighted strategic behavior in games are compared with the NME analysis. (shrink)

It is shown that the axioms Cubitt and Sugden (1994; Economic J. 104: 798) impose on a theory of rationally justifiable play (TRJP) do not prevent the possibility that two players necessarily disagree concerning the probability they ascribe to the choice of a third player. This appears to indicate that those axioms are not sufficient for defining a `reasonable' TRJP. In addition, for the case in which a player's beliefs are statistically independent, conditions for a TRJP are suggested under which (...) the existence of a quasi-strict equilibrium is sufficient, but the existence of a consistent n-pair is not, for defining a TRJP meeting those requirements. (shrink)

Two recent papers (Cubitt and Sugden, 1994; Samuelson, 1992) have established impossibility results which cast doubt on the coherence of the assumption of ’common knowledge of rationality'. It is shown that the Cubitt–Sugden result is the more powerful of the two impossibilities. Second, it is proved that the existence of a quasi-strict equilibrium is sufficient to construct sets which satisfy the Cubitt–Sugden axioms. This fact is used to establish that their impossibility result cannot arise in 2-player games. Finally, it (...) is shown that if a weak symmetry postulate is added, a new impossibility result arises for this class of games. (shrink)

The evolution of boundedly rational rules for playing normal form games is studied within stationary environments of stochastically changing games. Rules are viewed as algorithms prescribing strategies for the different normal form games that arise. It is shown that many of the “folk results” of evolutionary game theory, typically obtained with a fixed game and fixed strategies, carry over to the present environments. The results are also related to some recent experiments on rules (...) and games. (shrink)

Evidence presented in Salmon (2001; Econometrica 69(6) 1597) indicates that typical tests to identify learning behavior in experiments involving normal form games possess little power to reject incorrect models. This paper begins by presenting results from an experiment designed to gather alternative data to overcome this problem. The results from these experiments indicate support for a learning-to-learn or rule learning hypothesis in which subjects change their decision rule over time. These results are then used to construct an (...) adaptive learning model which is intended to mimic more accurately the behavior observed. The final section of the paper presents results from a simple simulation based analysis comparing the performance of this adaptive learning model with that of several standard decision rules in reproducing the choice patterns observed in the experiment. (shrink)

In single-person decision theory, Bayesian rationality requires the agent first to attach subjective probabilities to each uncertain event, and then to maximize the expected value of a von Neumann—Morgenstern utility function that is unique up to a cardinal equivalence class. When the agent receives new information, it also requires subjective probabilities to be revised according to Bayes’ rule.

The relationship between extensive and normal form analyses in non-cooperative game theory seems to be dominated, at least traditionally, by the so-called ‘sufficiency of the normal form principle’, according to which all that is necessary to analyse and ‘solve’ an extensive game is already in its normal form representation. The traditional defence of the sufficiency principle, that Myerson (1991, p. 50) attributes to von Neumann and Morgenstern, holds that, with respect to extensive games, (...) it can be assumed without loss of generality, that players formulate simultaneously and independently their strategic plans at the beginning of the game – a situation which, it is claimed, is exactly described by the normal representation of an extensive game. (shrink)

We prove a local normal form theorem of the Gaifman type for the infinitary logic L∞ωω whose formulas involve arbitrary unary quantifiers but finite quantifier rank. We use a local Ehrenfeucht-Fraïssé type game similar to the one in [9]. A consequence is that every sentence of L∞ωω of quantifier rank n is equivalent to an infinite Boolean combination of sentences of the form ψ, where ψ has counting quantifiers restricted to the -neighborhood of y.

We prove a local normal form theorem of the Gaifman type for the infinitary logic L∞ωω whose formulas involve arbitrary unary quantifiers but finite quantifier rank. We use a local Ehrenfeucht-Fraïssé type game similar to the one in [9]. A consequence is that every sentence of L∞ωω of quantifier rank n is equivalent to an infinite Boolean combination of sentences of the form ψ, where ψ has counting quantifiers restricted to the -neighborhood of y.

The "traditional" view of normative decision theory, as reported (for example) in chapter 2 of Luce and RaiÃa's [1957] classic work, Games and Decisions, proposes a reduction of sequential decisions problems to non-sequential decisions: a reduction of extensive forms to normal forms. Nonetheless, this reduction is not without its critics, both from inside and outside expected utility theory, It islay purpose in this essay to join with those critics by advocating the following thesis.

Contents. Introduction. 1. Preliminaries. 2. Normal Form Games. 3. Extensive Games. 4. Applications of Game Theory. 5. The Methodology of Game Theory. Conclusion. Appendix. Bibliography. Index. Does game theory—the mathematical theory of strategic interaction—provide genuine explanations of human behaviour? Can game theory be used in economic consultancy or other normative contexts? Explaining Games: The Epistemic Programme in Game Theory—the first monograph on the philosophy of game theory—is an attempt to combine insights from epistemic logic and (...) the philosophy of science to investigate the applicability of game theory in such fields as economics, philosophy and strategic consultancy. I prove new mathematical theorems about the beliefs, desires and rationality principles of individual human beings, and explore in detail the logical form of game theory as it is used in explanatory and normative contexts. I argue that game theory reduces to rational choice theory if used as an explanatory device, and that game theory is nonsensical if used as a normative device. A provocative account of the history of game theory reveals that this is not bad news for all of game theory, though. Two central research programmes in game theory tried to find the ultimate characterisation of strategic interaction between rational agents. Yet, while the Nash Equilibrium Refinement Programme has done badly thanks to such research habits as overmathematisation, model-tinkering and introversion, the Epistemic Programme, I argue, has been rather successful in achieving this aim. "The 'epistemic' approach to game theory has emerged over the past twenty-five years. What is this approach? How does it differ from the conventional equilibrium-based approach to game theory? What have been its strengths and weaknesses to date? To find out, read this comprehensive and excellently written account". Adam Brandenburger, J. P. Valles Professor of Business Economics and Strategy, Stern School of Business, New York University "Reading Boudewijn de Bruin's book should be rewarding both for game theorists interested in the conceptual foundations of their discipline and for philosophers who want to learn more about formal analysis of strategic interaction. It provides an in-depth logical study of the currently dominant epistemic approaches to non-cooperative games, with an eye both to the attractions and to the serious challenges facing the Epistemic Programme". Wlodek Rabinowicz, Professor of Practical Philosophy, Department of Philosophy, Lund University . (shrink)

We show that in quantum logic of closed subspaces of Hilbert space one cannot substitute quantum operations for classical (standard Hilbert space) ones and treat them as primitive operations. We consider two possible ways of such a substitution and arrive at operation algebras that are not lattices what proves the claim. We devise algorithms and programs which write down any two-variable expression in an orthomodular lattice by means of classical and quantum operations in an identical form. Our results show (...) that lattice structure and classical operations uniquely determine quantum logic underlying Hilbert space. As a consequence of our result, recent proposals for a deduction theorem with quantum operations in an orthomodular lattice as well as a, substitution of quantum operations for the usual standard Hilbert space ones in quantum logic prove to be misleading. Quantum computer quantum logic is also discussed. (shrink)

We show that for solvable games, the calculation of the strategies which survive iterative elimination of dominated strategies in normal games is equivalent to the calculation of the backward induction outcome of some extensive game. However, whereas the normal game form does not provide information on how to carry out the elimination, the corresponding extensive game does. As a by-product, we conclude that implementation using a subgame perfect equilibrium of an extensive game with perfect information (...) is equivalent to implementation through a solution concept which we call guided iteratively elimination of dominated strategies which requires a uniform order of elimination. Journal of Economic Literature Classifica-. (shrink)

We show that for solvable games, the calculation of the strategies which survive iterative elimination of dominated strategies in normal games is equivalent to the calculation of the backward induction outcome of some extensive game. However, whereas the normal game form does not provide information on how to carry out the elimination, the corresponding extensive game does. As a by-product, we conclude that implementation using a subgame perfect equilibrium of an extensive game with perfect information (...) is equivalent to implementation through a solution concept which we call guided iteratively elimination of dominated strategies which requires a uniform order of elimination. Journal of Economic Literature Classification Number: C72. (shrink)

In the standard formulation of game theory, agents use mixed strategies in the form of objective and probabilistically precise devices to conceal their actions. We introduce the larger set of probabilistically imprecise devices and study the consequences for the basic results on normal form games. While Nash equilibria remain equilibria in the extended game, there arise new Ellsberg equilibria with distinct outcomes, as we illustrate by negotiation games with three players. We characterize Ellsberg equilibria in (...) two-person conflict and coordination games. These equilibria turn out to be related to experimental deviations from Nash equilibrium play. (shrink)

The emergence of shared symbol systems is considered to be a pivotal moment in human evolution and human development. These changes are normally explained by reference to changes in people's internal cognitive processes. We present 2 experiments which provide evidence that changes in the external, collaborative processes that people use to communicate can also affect the structure and organization of symbol systems independently of cognitive change. We propose that mutual‐modifiability—opportunities for people to edit or manipulate each other's contributions—is a key (...) constraint on the emergence of complex symbol systems. We discuss the implications for models of language development and the origins of compositionality. (shrink)

We consider Effort Games, a game-theoretic model of cooperation in open environments, which is a variant of the principal-agent problem from economic theory. In our multiagent domain, a common project depends on various tasks; carrying out certain subsets of the tasks completes the project successfully, while carrying out other subsets does not. The probability of carrying out a task is higher when the agent in charge of it exerts effort, at a certain cost for that agent. A central authority, (...) called the principal, attempts to incentivize agents to exert effort, but can only reward agents based on the success of the entire project.We model this domain as a normal form game, where the payoffs for each strategy profile are defined based on the different probabilities of carrying out each task and on the boolean function that defines which task subsets complete the project, and which do not. We view this boolean function as a simple coalitional game, and call this game the underlying coalitional game. We suggest the Price of Myopia as a measure of the influence the model of rationality has on the minimal payments the principal has to make in order to motivate the agents in such a domain to exert effort.We consider the computational complexity of testing whether exerting effort is a dominant strategy for an agent, and of finding a reward strategy for this domain, using either a dominant strategy equilibrium or using iterated elimination of dominated strategies. We show these problems are generally #P-hard, and that they are at least as computationally hard as calculating the Banzhaf power index in the underlying coalitional game. We also show that in a certain restricted domain, where the underlying coalitional game is a weighted voting game with certain properties, it is possible to solve all of the above problems in polynomial time. We give bounds on PoM in weighted voting effort games, and provide simulation results regarding PoM in another restricted class of effort games, namely effort games played over Series-Parallel Graphs. (shrink)

We study repeated normal form games where the number of players is large. We argue that it is interesting to look at such games as being divided into subgames, each of which we call a neighbourhood. The structure of such a game is given by a graph G whose nodes are players and edges denote visibility. The neighbourhoods are maximal cliques in G. The game proceeds in rounds where in each round the players of every clique (...) X of G play a strategic form game among each other. A player at a node v strategises based on what she can observe, i.e., the strategies and the outcomes in the previous round of the players at vertices adjacent to v. Based on this, the player may switch strategies in the same neighbourhood, or migrate to another neighbourhood.We are interested in addressing questions regarding the eventual stability of such games. We incrementally impose constraints on the ‘types’ of the players. First, we look at players who are unconstrained in their strategising abilities, in that, players who may use unbounded memory. We then consider the case of memoryless players. We show that in both these cases the eventual stability of the game can be characterised in terms of potentials. We then introduce a simple modal logic in which the types of the players can be specified. We show that when the players play according to these specified types, it can be effectively decided whether the game stabilises. Finally, we look at the important heuristic of imitation. Simple imitative strategies can be specified in the logic introduced by us. We show that in a population of optimisers and imitators, we can decide how ‘worse-off’ the imitators are by playing imitative strategies rather than optimal ones. (shrink)

This paper examines the existence of strategic solutions to finite normal form games under the assumption that strategy choices can be described as choices among lotteries where players have security- and potential level preferences over lotteries (e.g., Cohen, Theory and Decision, 33, 101–104, 1992, Gilboa, Journal of Mathematical Psychology, 32, 405–420, 1988, Jaffray, Theory and Decision, 24, 169–200, 1988). Since security- and potential level preferences require discontinuous utility representations, standard existence results for Nash equilibria in mixed strategies (...) (Nash, Proceedings of the National Academy of Sciences, 36, 48–49, 1950a, Non-Cooperative Games, Ph.D. Dissertation, Princeton University Press, 1950b) or for equilibria in beliefs (Crawford, Journal of Economic Theory, 50, 127–154, 1990) do not apply. As a key insight this paper proves that non-existence of equilibria in beliefs, and therefore non-existence of Nash equilibria in mixed strategies, is possible in finite games with security- and potential level players. But, as this paper also shows, rationalizable strategies (Bernheim, Econometrica, 52, 1007–1028, 1984, Moulin, Mathematical Social Sciences, 7, 83–102, 1984, Pearce, Econometrica, 52, 1029–1050, 1984) exist for such games. Rationalizability rather than equilibrium in beliefs therefore appears to be a more favorable solution concept for games with security- and potential level players. (shrink)

We study a class of two-player normal-form games with cyclical payoff structures. A game is called circulant if both players’ payoff matrices fulfill a rotational symmetry condition. The class of circulant games contains well-known examples such as Matching Pennies, Rock-Paper-Scissors, as well as subclasses of coordination and common interest games. The best response correspondences in circulant games induce a partition on each player’s set of pure strategies into equivalence classes. In any Nash Equilibrium, all (...) strategies within one class are either played with strictly positive or with zero probability. We further show that, strikingly, a single parameter fully determines the exact number and the structure of all Nash equilibria in these games. The parameter itself only depends on the position of the largest payoff in the first row of one of the player’s payoff matrix. (shrink)

This book represents a major contribution to game theory. It offers this conception of equilibrium in games: strategic equilibrium. This conception arises from a study of expected utility decision principles, which must be revised to take account of the evidence a choice provides concerning its outcome. The argument for these principles distinguishes reasons for action from incentives, and draws on contemporary analyses of counterfactual conditionals. The book also includes a procedure for identifying strategic equilibria in ideal normal-form (...) games. In synthesizing decision theory and game theory in a powerful way this book will be of particular interest to all philosophers concerned with decision theory and game theory as well as economists and other social scientists. (shrink)

We investigate a simple game paradigm for intuitionistic logic, inspired by Wajsberg’s implicit inhabitation algorithm and Beth tableaux. The principal idea is that one player, ∃ros, is trying to construct a proof in normal form while his opponent, ∀phrodite, attempts to build a counter-model. The determinacy of the game implies therefore both completeness and semantic cut-elimination.

Gaifman's normal form theorem showed that every first-order sentence of quantifier rank n is equivalent to a Boolean combination of “scattered local sentences”, where the local neighborhoods have radius at most 7n−1. This bound was improved by Lifsches and Shelah to 3×4n−1. We use Ehrenfeucht–Fraïssé type games with a “shrinking horizon” to get a spectrum of normal form theorems of the Gaifman type, depending on the rate of shrinking. This spectrum includes the result of Lifsches (...) and Shelah, with a more easily understood proof and with the bound on the radius improved to 4n−1. We also obtain bounds for a normal form theorem of Schwentick and Barthelmann. (shrink)

The prelims comprise: Strategic Interaction Nash Equilibrium Normal‐form Refinements Games in Extensive Form Extensive‐form Refinements Selection by Evolution Notes.

Reasoning about equilibria in normal form games involves the study of players’ incentives to deviate unilaterally from any profile. In the case of large anonymous games, the pattern of reasoning is different. Payoffs are determined by strategy distributions rather than strategy profiles. In such a game each player would strategise based on expectations of what fraction of the population makes some choice, rather than respond to individual choices by other players. A player may not even know (...) how many players there are in the game. Logicising such strategisation involves many challenges as the set of players is potentially unbounded. This suggests a logic of quantification over player variables and modalities for player deviation, but such a logic is easily seen to be undecidable. Instead, we propose a propositional modal logic using player types as names and implicit quantification over players. With modalities for player deviation and transitive closure, the logic can be used to specify game equilibrium and interesting patterns of reasoning in large games. We show that the logic is decidable and present a complete axiomatisation of the valid formulas. (shrink)

The paper argues that the Nash Equilibrium Refinement Programme was less successful than its competitor, the Epistemic Programme. The prime criterion of success is the extent to which the programmes were able to reach the key objective guiding non-cooperative game theory for much of the twentieth century, namely, to develop a complete characterisation of the strategic rationality of economic agents in the form of the ultimate solution concept for any normal form and extensive game. The paper explains (...) this in terms of unjustified degrees of mathematisation in Nash Equilibrium Refinement Programme. While this programme’s mathematical models were often inspired by purely mathematical concerns rather than the economic phenomena they were intended to model, the Epistemic Programme’s models were developed with a keen eye to the role beliefs and desires play in strategic interaction between rational economic agents playing games; that is, their interactive epistemology. The Epistemic Programme succeeded in developing mathematical models formalising aspects of strategic interaction that remained implicit in the Nash Equilibrium Refinement Programme owing to an unjustified degree of mathematisation. As a result, the Epistemic Programme is the more successful theory.Keywords: Epistemic Programme; Game theory; Interactive epistemology; Mathematisation; Nash equilibrium. (shrink)

Counterexamples to two results by Stalnaker (Theory and Decision, 1994) are given and a corrected version of one of the two results is proved. Stalnaker's proposed results are: (1) if at the true state of an epistemic model of a perfect information game there is common belief in the rationality of every player and common belief that no player has false beliefs (he calls this joint condition ‘strong rationalizability’), then the true (or actual) strategy profile is path equivalent to a (...) Nash equilibrium; (2) in a normal-form game a strategy profile is strongly rationalizable if and only if it belongs to C8 , the set of profiles that survive the iterative deletion of inferior profiles. (shrink)

This paper analyzes the core of cooperative games generated by asymmetric aggregative normal-form games, i.e., games where the payoff of each player depends on his strategy and the sum of the strategies of all players. We assume that each coalition calculates its worth presuming that the outside players stand alone and select individually best strategies. We show that under some mild monotonicity assumptions on payoffs, the resulting cooperative game is balanced and has a non-empty core. (...) Our paper thus offers an existence result for a core notion which is frequently encountered in the theory and applications of cooperative games with externalities. (shrink)

This book represents a major contribution to game theory. It offers this conception of equilibrium in games: strategic equilibrium. This conception arises from a study of expected utility decision principles, which must be revised to take account of the evidence a choice provides concerning its outcome. The argument for these principles distinguishes reasons for action from incentives, and draws on contemporary analyses of counterfactual conditionals. The book also includes a procedure for identifying strategic equilibria in ideal normal-form (...) games. In synthesizing decision theory and game theory in a powerful way this book will be of particular interest to all philosophers concerned with decision theory and game theory as well as economists and other social scientists. (shrink)

PurposeThe purpose of this paper is to argue that playing computer games for lengthy periods of time, even in a manner that will force the player to forgo certain other activities normally seen as more important, can be an integral part of human flourishing.Design/methodology/approachThe authors' claim is based on a modern reading of Aristotle's Nichomacean Ethics. It should be emphasized that the authors do not argue that computer gaming and other similar online activities are central to all people under (...) all circumstances; but only seek to show that the claim holds true for some people under some circumstances and the authors try to spell out the relevant circumstances in detail.FindingsThe authors provide a list of situations in which playing computer games for lengthy periods of time, in a manner that will force the player to forgo certain other activities normally seen as more important, is an integral part of human flourishing.Originality/valueThe paper puts some novel pressure on the widely‐held belief that playing computer games for lengthy periods of time, in a manner that will force the player to forgo certain other activities normally seen as more important. The paper claims that playing some computer games and partaking in some forms of online activities could be highly conducive to what it actually means in practice to take care of oneself and, to paraphrase Aristotle, to be eager for fine actions. (shrink)

Paralympic Games, involving people with disabilities, are a manifestation of excellence in sport. They show that athletics performed by PWD counts as genuine sport. They also support a wider meaning of the term ‘health,’ understood not just like a utopian state of perfection, but like the ability to realize oneself in the projects and activities of one’s own choosing. Notwithstanding these virtues, PG—in their current form—may paradoxycally reinforce social prejudice against PWD. This is due to the fact that (...) PG and Olympic Games are now two distinct events. In this article, I argue that PG should be integrated in the OG, just like women’s and ‘minor’ sports, because the separation of PG and OG indicates a morally arbitrary separation between people with and without disabilities. I also propose to remove the word ‘Para-lympic’ because it stigmatizes the sport performed by PWD as an appendix of ‘normal’ sport. Athletes with disabilities deserve special attention because they have special nee.. (shrink)

Normative game theory unsatisfactorily explains rational behavior. Real people do not behave as predicted, and what is prescribed as rational behavior is normally unattainable in real-life. The problem is that current normative analysis does not account for people's cognitive limitations – their bounded rationality. However, this paper develops an account of bounded rationality that explains the rationality of more realistic behavior. I focus on the Centipede Game, in which boundedly rational players explore and test others' immediate behavior, until they can (...) apply limited backward induction. The result is that the game has a solution in the form of a subjective Nash equilibrium, which boundedly rational players can possibly realize. (shrink)

Akama et al. [1] systematically studied an arithmetical hierarchy of the law of excluded middle and related principles in the context of first-order arithmetic. In that paper, they first provide a prenex normal form theorem as a justification of their semi-classical principles restricted to prenex formulas. However, there are some errors in their proof. In this paper, we provide a simple counterexample of their prenex normal form theorem [1, Theorem 2.7], then modify it in an appropriate (...) way which still serves to largely justify the arithmetical hierarchy. In addition, we characterize a variety of prenex normal form theorems by logical principles in the arithmetical hierarchy. The characterization results reveal that our prenex normal form theorems are optimal. For the characterization results, we establish a new conservation theorem on semi-classical arithmetic. The theorem generalizes a well-known fact that classical arithmetic is $\Pi _2$ -conservative over intuitionistic arithmetic. (shrink)

The system of natural deduction that originated with Gentzen , and for which Prawitz proved a normalization theorem, is re-cast so that all elimination rules are in parallel form. This enables one to prove a very exigent normalization theorem. The normal forms that it provides have all disjunction-eliminations as low as possible, and have no major premisses for eliminations standing as conclusions of any rules. Normal natural deductions are isomorphic to cut-free, weakening-free sequent proofs. This form (...) of normalization theorem renders unnecessary Gentzen's resort to sequent calculi in order to establish the desired metalogical properties of his logical system.Ultimate normal forms are well-adapted to the needs of the computational logician, affording valuable constraints on proof-search. They also provide an analysis of deductive relevance. There is a deep isomorphism between natural deductions and sequent proofs in the relevantized system. (shrink)

A notation for an ordinal using patterns of resemblance is based on choosing an isominimal set of ordinals containing the given ordinal. There are many choices for this set meaning that notations are far from unique. We establish that among all such isominimal sets there is one which is smallest under inclusion thus providing an appropriate notion of normal form notation in this context. In addition, we calculate the elements of this isominimal set using standard notations based on (...) collapsing functions. This provides a capstone to the results in [2, 6, 8, 9, 7], using further refinement of ordinal arithmetic developed in [8] which then both allows for a simple characterization of normal forms for patterns of order one and will play a key role in the arithmetical analysis of pure patterns of order two, [5]. (shrink)

Montague [7] translates English into a tensed intensional logic, an extension of the typed -calculus. We prove that each translation reduces to a formula without -applications, unique to within change of bound variable. The proof has two main steps. We first prove that translations of English phrases have the special property that arguments to functions are modally closed. We then show that formulas in which arguments are modally closed have a unique fully reduced -normal form. As a corollary, (...) translations of English phrases are contained in a simply defined proper subclass of the formulas of the intensional logic. (shrink)

Statman and Orevkov independently proved that cut-elimination is of nonelementary complexity. Although their worst-case sequences are mathematically different the syntax of the corresponding cut formulas is of striking similarity. This leads to the main question of this paper: to what extent is it possible to restrict the syntax of formulas and — at the same time—keep their power as cut formulas in a proof? We give a detailed analysis of this problem for negation normal form , prenex (...) class='Hi'>normal form and monotone formulas. We show that proof reduction to NNF is quadratic, while PNF behaves differently: although there exists a quadratic transformation into a proof in PNF too, additional cuts are needed; the elimination of these cuts requires nonelementary expense in general. By restricting the logical operators to {,,,}, we obtain the type of monotone formulas. We prove that the elimination of monotone cuts can be of nonelementary complexity . On the other hand, we define a large class of problems where cut-elimination of monotone cuts is only exponential and show that this bound is tight. This implies that the elimination of monotone cuts in equational theories is at most exponential. Particularly, there are no short proofs of Statman's sequence with monotone cuts. (shrink)

We start with a simple proof of Leivant's normal form theorem for ∑11 formulas over finite successor structures. Then we use that normal form to prove the following:1. over all finite structures, every ∑21 formula is equivalent to a ∑21 formula whose first-order part is a Boolean combination of existential formulas, and2. over finite successor structures, the Kolaitis-Thakur hierarchy of minimization problems collapses completely and the Kolaitis-Thakur hierarchy of maximization problems collapses partially.The normal form (...) theorem for ∑21 fails if ∑21 is replaced with ∑11 or if infinite structures are allowed. (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 show that derivations in the nonassociative and commutative Lambek calculus with product can be transformed to a normal form as it is the case with derivations in noncommutative calculi. As an application we obtain that the class of languages generated by categorial grammars based on the nonassociative and commutative Lambek calculus with product is included in the class of CF-languages. MSC: 68Q50, 03D15, 03B65.

Let $R$ be a convergent term rewriting system, and let $CR$-equality on combinatory logic terms be the equality induced by $\beta \eta R$-equality on terms of the lambda calculus under any of the standard translations between these two frameworks for higher-order reasoning. We generalize the classical notion of strong reduction to a reduction relation which generates $CR$-equality and whose irreducibles are exactly the translates of long $\beta R$-normal forms. The classical notion of strong normal form in combinatory (...) logic is also generalized, yielding yet another description of these translates. Their resulting tripartite characterization extends to the combined first-order algebraic and higher-order setting the classical combinatory logic descriptions of the translates of long $\beta$-normal forms in the lambda calculus. As a consequence, the translates of long $\beta R$-normal forms are easily seen to serve as canonical representatives for $CR$-equivalence classes of combinatory logic terms for non-empty, as well as for empty, $R$. (shrink)

Functions of type n are characteristic functions on n-ary relations. Keenan [5] established their importance for natural language semantics, by showing that natural language has many examples of irreducible type n functions, i.e., functions of type n that cannot be represented as compositions of unary functions. Keenan proposed some tests for reducibility, and Dekker [3] improved on these by proposing an invariance condition that characterizes the functions with a reducible counterpart with the same behaviour on product relations. The present paper (...) generalizes the notion of reducibility (a quantifier is reducible if it can be represented as a composition of quantifiers of lesser, but not necessarily unary, types), proposes a direct criterion for reducibility, and establishes a diamond theorem and a normal form theorem for reduction. These results are then used to show that every positive n function has a unique representation as a composition of positive irreducible functions, and to give an algorithm for finding this representation. With these formal tools it can be established that natural language has examples of n-ary quantificational expressions that cannot be reduced to any composition of quantifiers of lesser degree. (shrink)

Formulas of n variables of Łukasiewicz sentential calculus can be represented, via McNaughton’s theorem, by piecewise linear functions, with integer coefficients, from hypercube [0,1] n to [0,1], called McNaughton functions. As a consequence of the McNaughton representation of a formula it is obtained a canonical form of a formula. Indeed, up to logical equivalence, any formula can be written as an infimum of finite suprema of formulas associated to McNaughton functions which are truncated functions to $[0,1]$ of the restriction (...) to [0,1] n of single hyperplanes, for short, called simple McNaughton functions. In the present paper we will concern with the problem of presenting formulas of Lukasiewicz sentential calculus in normal form. Here we list the main results we obtained: a) we give an axiomatic description of some classes of formulas having the property to be canonically mapped one-to-one onto the class of simple Mc Naughton functions; b) we provide normal forms for Lukasiewicz sentential calculus, making use of formulas defined in a); c) we prove the polynomial complexity of formulas, in normal form, coming from a certain class described as in a); d) we extend the results described in a), b) and c) to Rational Lukasiewicz logic. (shrink)