I present a decision problem in which causal decision theory appears to violate the independence of irrelevant alternatives (IIA) and normal-form extensive-form equivalence (NEE). I show that these violations lead to exploitable behavior and long-run poverty. These consequences appear damning, but I urge caution. This decision should lead causalists to a better understanding of what it takes for a decision between some collection of options to count as a subdecision of a decision between a larger (...) collection of options. And with this better understanding of subdecisions in hand, causalists will not violate the IIA or the NEE. This decision will also teach causalists that, in sequential decisions, a rational agent may be led to make a series of choices which are causally dominated by some other sequence of choices they could have made instead. I will encourage causalists to recognise this as an intrapersonal tragedy of the commons. (shrink)

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.

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)

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)

Graph normal form, introduced earlier for propositional logic, is shown to be a normal form also for first-order logic. It allows to view syntax of theories as digraphs, while their semantics as kernels of these digraphs. Graphs are particularly well suited for studying circularity, and we provide some general means for verifying that circular or apparently circular extensions are conservative. Traditional syntactic means of ensuring conservativity, like definitional extensions or positive occurrences guaranteeing exsitence of fixed points, (...) emerge as special cases. (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)

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 consider a normal-form game in which there is a single exogenously given coalition of cooperating players that can write a binding agreement on pre-selected actions. The actions representing other dimensions of the strategy space remain under the sovereign, individual control of the players. We consider a standard extension of the Nash equilibrium concept denoted as a partial cooperative equilibrium as well as an equilibrium concept in which the coalition of cooperators has a leadership position. Existence results are (...) stated and we identify conditions under which the various equilibrium concepts are equivalent. We apply this framework to existing models of multi-market oligopolies and international pollution abatement. In a multi-market oligopoly, typically, a merger paradox emerges in the partial cooperative equilibrium. The paradox vanishes if the cartel attains a leadership position. For international pollution abatement treaties, cooperation by a sufficiently large group of countries results in a Pareto improvement over the standard tragedy of the commons outcome described by the Nash equilibrium. (shrink)

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)

Sensory substitution devices provide through an unusual sensory modality (the substituting modality, e.g., audition) access to features of the world that are normally accessed through another sensory modality (the substituted modality, e.g., vision). In this article, we address the question of which sensory modality the acquired perception belongs to. We have recourse to the four traditional criteria that have been used to define sensory modalities: sensory organ, stimuli, properties, and qualitative experience (Grice, 1962), to which we have added the criteria (...) of behavioral equivalence (Morgan, 1977), dedication (Keeley, 2002), and sensorimotor equivalence (O’Regan & Noe¨, 2001). We discuss which of them are fulfilled by perception through sensory substitution devices and whether this favors the view that perception belongs to the substituting or to the substituted modality. Though the application of a number of criteria might be taken to point to the conclusion that perception with a sensory substitution device belongs to the substituted modality, we argue that the evidence leads to an alternative view on sensory substitution. According to this view, the experience after sensory substitution is a transformation, extension, or augmentation of our perceptual capacities, rather than being something equivalent or reducible to an already existing sensory modality. We develop this view by comparing sensory substitution devices to other ‘‘mind-enhancing tools’’ such as pen and paper, sketchpads, or calculators. An analysis of sensory substitution in terms of mind-enhancing tools unveils it as a thoroughly transforming perceptual experience and as giving rise to a novel form of perceptual interaction with the environment. (shrink)

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 (...) class='Hi'>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 present an extension of the lambda calculus with the letrec construct. In contrast to current theories, which impose restrictions on where the rewriting can take place, our theory is very liberal, e.g., it allows rewriting under lambda abstractions and on cycles. As shown previously, the reduction theory is non-confluent. Thus, we searched for and found a new property that resembles confluence and that is equivalent to uniqueness of infinite normal forms: skew confluence. This notion is based on the (...) intuition that some terms are better than others and that terms reduce to better terms. It states that if a term reduces to two other terms, the second of those terms can always be reduced to a term that is better than the first. Using skew confluence we define the infinite normal form of a term and show that the infinite normal form defines a congruence on the set of terms. We relate the lambda calculus plus letrec to the plain lambda calculus and to one of the infinitary lambda calculi. We also present a variant of our calculus, which follows the tradition of the explicit substitution calculi. (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)

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 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 paper gives a simple result on the existence of normal forms for the following equivalence relation between objects of a category: A∼B if and only if there are maps A→B and B→A , under the hypothesis that the category has epi-mono factorizations and each object has finitely many sub-objects and quotient-objects. Applications to algebra, logic, automata theory, databases are presented.

LetA H be the Herbrand normal form ofA andA H,D a Herbrand realization ofA H. We showThere is an example of an (open) theory ℐ+ with function parameters such that for someA not containing function parameters Similar for first order theories ℐ+ if the index functions used in definingA H are permitted to occur in instances of non-logical axiom schemata of ℐ, i.e. for suitable ℐ,A In fact, in (1) we can take for ℐ+ the fragment (Σ 1 (...) 0 -IA)+ of second order arithmetic with induction restricted toΣ 1 0 -formulas, and in (2) we can take for ℐ the fragment (Σ 1 0,b -IA) of first order arithmetic with induction restricted to formulas VxA(x) whereA contains only bounded quantifiers.On the other hand, $$PA^2 \vdash A^H \Rightarrow PA \vdash A,$$ wherePA 2 is the extension of first order arithmeticPA obtained by adding quantifiers for functions andA∈ℒ(PA). This generalizes to extensional arithmetic in the language of all finite types but not to sentencesA with positively occurring existential quantifiers for functions. (shrink)

A proof-theoretic test for paradoxicality was famously proposed by Tennant: a paradox must yield a closed derivation of absurdity with no normal form. Drawing on the remark that all derivations of a given proposition can be transformed into derivations in normal form of a logically equivalent proposition, we investigate the possibility of paradoxes in normal form. We compare paradoxes à la Tennant and paradoxes in normal form from the viewpoint of the computational (...) interpretation of proofs and from the viewpoint of proof-theoretic semantics. (shrink)

ABSTRACT Most theorem provers for Classical Logic transform the input formula into a particular normal form. This tranformation is done before the execution of the algorithm or it is integrated into the deductive algorithm. This situation is no different for Non-Classical Logics and, particularly, for Temporal Logics. However, unlike classical logic, temporal logic does not provide an extension of the notion of non negative normal form. In this work, we define a temporal negative normal (...) class='Hi'>form for the future fragment of the linear time propositional temporal logic, named FNext. The definition saves as much information as possible about implicants and implicates of the input formula and its subformulas. This property is the novelty of this normal form; for example, in [Fis97] the normal form is guided by the separation property and in [Ven86] the normal form provided prepares the input formula to be treated by a resolution method. Moreover, we also introduce an algorithm having linear cost, which transforms the input formula into a temporal negative normal form. Furthermore, in this work we present a new structure and a set of operators over it that allows us to efficiently manage the information about unitary implicants and implicates contained in the subformulae. (shrink)

We investigate the substitution Frege () proof system and its relationship to extended Frege () in the context of modal and superintuitionistic propositional logics. We show that is p-equivalent to tree-like , and we develop a “normal form” for -proofs. We establish connections between for a logic L, and for certain bimodal expansions of L.We then turn attention to specific families of modal and si logics. We prove p-equivalence of and for all extensions of , all tabular (...) logics, all logics of finite depth and width, and typical examples of logics of finite width and infinite depth. In most cases, we actually show an equivalence with the usual system for classical logic with respect to a naturally defined translation.On the other hand, we establish exponential speed-up of over for all modal and si logics of infinite branching, extending recent lower bounds by P. Hrubeš. We develop a model-theoretical characterization of maximal logics of infinite branching to prove this result. (shrink)

We show that every formula of L ω 1p is equivalent to one which is a propositional combination of formulas with only one quantifier. It follows that the complete theory of a probability model is determined by the distribution of a family of random variables induced by the model. We characterize the class of distribution which can arise in such a way. We use these results together with a form of de Finetti's theorem to prove an almost sure interpolation (...) theorem for L ω 1p. (shrink)

Originating from work in operations research the cutting plane refutation systemCP is an extension of resolution, where unsatisfiable propositional logic formulas in conjunctive normal form are recognized by showing the non-existence of boolean solutions to associated families of linear inequalities. Polynomial sizeCP proofs are given for the undirecteds-t connectivity principle. The subsystemsCP q ofCP, forq≥2, are shown to be polynomially equivalent toCP, thus answering problem 19 from the list of open problems of [8]. We present a normal (...) form theorem forCP 2-proofs and thereby for arbitraryCP-proofs. As a corollary, we show that the coefficients and constant terms in arbitrary cutting plane proofs may be exponentially bounded by the number of steps in the proof, at the cost of an at most polynomial increase in the number of steps in the proof. The extensionCPLE +, introduced in [9] and there shown top-simulate Frege systems, is proved to be polynomially equivalent to Frege systems. Lastly, since linear inequalities are related to threshold gates, we introduce a new threshold logic and prove a completeness theorem. (shrink)

We study the expressive power in the finite of the logic Fixed-Point+Counting, the extension of first-order logic which is obtained through adding both the fixed-point constructor and the ability to count. To this end an isomorphism preserving (`generic') model of computation is introduced whose PTime restriction exactly corresponds to this level of expressive power, while its PSpace restriction corresponds to While+Counting. From this model we obtain a normal form which shows a rather clear separation of the relational vs. (...) the arithmetical side of the algorithms involved. In parallel, we study the relations of Fixed-Point+Counting with the infinitary logics L r ∞ω (∃ ≥ m ) m∈ω and the corresponding pebble games. The main result, however, involves the concept of an arithmetical invariant. By this we mean a functor taking every finite relational structure to an expansion of (an initial segment of) the standard arithmetical structure. In particular its values are linearly ordered structures. We establish the existence of a family of arithmetical invariants (J r ) r≥ 1 with the following properties: $\bullet$ The invariants themselves can be evaluated in polynomial time. $\bullet$ A class of finite relational structures is definable in Fixed-Point+Counting if and only if membership can be decided in polynomial time on the basis of the values of one of the invariants. $\bullet$ The invariant J r classifies all finite relational structures exactly up to equivalence with respect to the logic L r ∞ω (∃ ≥ m ) m∈ω . We also give a characterization of Fixed-Point+Counting in terms of sequences of formulae in the L r ωω (∃ ≥ m ) m∈ω : It corresponds exactly to the polynomial time computable families (φ n ) n∈ω in these logics. Towards a positive assessment of the expressive power of Fixed-Point+Counting, it is shown that the natural extension of fixed-point logic by Lindström quantifiers, which capture all the PTime computable properties of cardinalities of definable predicates, is strictly weaker than what we get here. This implies in particular that every extension of fixed-point logic by means of monadic Lindstrom quantifiers, which stays within PTime, must be strictly contained in Fixed-Point+Counting. (shrink)

We investigate some logics which use the concept of minimal models in their definition. Minimal objects are widely used in Logic and Computer Science. They are applied in the context of Inductive Definitions, Logic Programming and Artificial Intelligence. An example of logic which uses this concept is the MIN logic due to van Benthem [20]. He shows that MIN is equivalent to the Least Fixed Point logic in expressive power. In [6], we extended MIN to the MIN Logic and proved (...) it is equivalent to second-order logic in expressive power. Here, we exhibit a fragment of MIN, the MINΔ logic, which is more expressive than LFP, less expressive than MIN and closed under boolean connectives and first-order quantification. In order to do this, in the Section 2, we prove that the Downward Löwenheim-Skolem Theorem holds for arbitrary countable sets of LFP-formulas by showing that every infinite structure has a countable LFP-substructure. The method may be used to generalize this theorem to any set of LFP-formulas. We also analyse the expressive power of the Nested Abnormality Theories of Lifschitz, another formalism based on minimal models used in Artificial Intelligence, and we demonstrate that for each second-order theory Γ there is a NAT which is a conservative extension of Γ. We give a translation from second-order sentences into such NATs which is linear in the size of the sentence in prenex normal form. Finally, we establish a hierarchy of expressiveness of these logics that deal with the concept of minimal models. (shrink)

Each closed (i.e. variable free) formula of interpretability logic is equivalent in ILF to a closed formula of the provability logic G, thus to a Boolean combination of formulas of the form n.

It would be useful to have a category of extensive-form games whose isomorphisms specify equivalences between games. Since working with entire games is too large a project for a single paper, I begin here with preforms, where a “preform” is a rooted tree together with choices and information sets. In particular, this paper first defines the category \, whose objects are “functioned trees”, which are specially designed to be incorporated into preforms. I show that \ is isomorphic to (...) the full subcategory of \ whose objects are converging arborescences. Then the paper defines the category \, whose objects are “node-and-choice preforms”, each of which consists of a node set, a choice set, and an operator mapping node-choice pairs to nodes. I characterize the \ isomorphisms, define a forgetful functor from \ to \, and show that \ is equivalent to the full subcategory of \ whose objects are perfect-information preforms. The paper also shows that many game-theoretic entities can be derived from preforms, and that these entities are well-behaved with respect to \ morphisms and isomorphisms. (shrink)

In 1990, J.L. Krivine introduced the notion of storage operator to simulate, in $lambda$-calculus, the 'call by value' in a context of a 'call by name'. J.L. Krivine has shown that, using Gödel translation from classical into intuitionistic logic, we can find a simple type for storage operators in AF2 type system. In this present paper, we give a general type for storage operators in a slight extension of AF2. We give at the end (without proof) a generalization of this (...) result to other types. (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.

A logic \ is called self-extensional if it allows to replace occurrences of a formula by occurrences of an \-equivalent one in the context of claims about logical consequence and logical validity. It is known that no three-valued paraconsistent logic which has an implication can be self-extensional. In this paper we show that in contrast, the famous Dunn–Belnap four-valued logic has exactly one self-extensional four-valued extension which has an implication. We also investigate the main properties of this logic, determine the (...) expressive power of its language, and provide a cut-free Gentzen-type proof system for it. (shrink)

For Tarski logics, there are simple criteria that enable one to conclude that two premise sets are equivalent. We shall show that the very same criteria hold for adaptive logics, which is a major advantage in comparison to other approaches to defeasible reasoning forms. A related property of Tarski logics is that the extensions of equivalent premise sets with the same set of formulas are equivalent premise sets. This does not hold for adaptive logics. However a very similar criterion does. (...) We also shall show that every monotonic logic weaker than an adaptive logic is weaker than the lower limit logic of the adaptive logic or identical to it. This highlights the role of the lower limit for settling the adaptive equivalence of extensions of equivalent premise sets. (shrink)

Models of normal open induction (NOI) are those discretely ordered rings, integrally closed in their fraction field whose nonnegative part satisfy Peano's induction axioms for open formulas in the language of ordered semirings. Here we study the problem of representability of an element a of a model M of NOI (in some extension of M) by a quadratic form of the type X2 + bY2 where b is a nonzero integer. Using either a trigonometric or a hyperbolic parametrization (...) we prove that except in some trivial cases, M[ x, y] with x2 + by2 = a can be embedded in a model of NOI. We also study quadratic extensions of a model M of NOI; we first prove some properties of the ring of Gaussian integers of M. Then we study the group of solutions of a Pell equation in NOI; we construct a model in which the quotient group by the squares has size continuum. (shrink)

We investigate the set theoretical strength of some properties of normality, including Urysohn's Lemma, Tietze-Urysohn Extension Theorem, normality of disjoint unions of normal spaces, and normality of Fσ subsets of normal spaces.

The idea of rejection of some sentences on the basis of others comes from Aristotle, as Jan Łukasiewicz states in his studies on Aristotle's syllogistic [1939, 1951], concerning rejection of the false syllogistic form and those on certain calculus of propositions. Short historical remarks on the origin and development of the notion of a rejected sentence, introduced into logic by Jan Łukasiewicz, are contained in the Introduction of this paper. This paper is to a considerable extent a summary of (...) papers which are not easily available, even to the Polish reader: (1) J. Słupecki, Funkcja Łukasiewicza (Łukasiewicz’s function), Zeszyty Naukowe Uniwersytetu Wrocławskiego, Seria B, nr 3 (1959), 33-40; (2) U. Wybraniec-Skardowska, Teoria zdań odrzuconych (Theory of Rejected Sentences), (doctoral dissertation under the supervision of Jerzy Słupecki, published as a monograph), Zeszyty Naukowe Wyższej Szkoły Pedagogicznej w Opolu, Studia i Monografie, Nr 22 (1969), 5-131; (3) G. Bryll, Kilka uzupełnień teorii zdań odrzuconych (Some supplements to the theory of rejcted sentences), Zeszyty Naukowe Wyższej Szkoły Pedagogicznej w Opolu, Studia i Mnografie, Nr 22 (1969), 153-154. The paper also contains a good number of results which have not been published yet. Chapter I contains results presented in the papers (1)-(3). It provides an extension of Alfred Tarski’s theory of deductive systems presented by him in the papers [1930]: Fundamentale Begriffe der Methodologie der deduktiven Wssenschaften, I and Über einige fundamentale Begriffe der Metamathematik. The enriched theory is marked with T. The most essential new concept in T is the function Cn-1, whose definition was given by Słupecki in (1) on the basis of the so-called Tarski’s general theory of deductive systems. It has the form: y e Cn-1X iff Ex e X (x e Cn {y}), where Cn is Tarski’s consequence operation. In accordance with the definition: A sentence y is rejected on the basis of the sentences of the set X iff at least one of sentences of X is a consequence of y (is deducible from y). The intuitive meaning of the rejection function Cn-1: on the basis of false sentences we can reject false sentences only (while by means of the consequence operation Cn on the basis of true sentences we can deduce true sentences only). The function Cn-1 is a generalization of the notion of rejected sentences which was introduced into logic by Łukasiewicz. The essential property of the rejection function Cn-1 is that it satisfies the axioms of general Tarski’s consequence Cn, so it is a consequence operation, called the rejection consequence. In addition, it is an additive and normal operation. In Chapter I, there are given notions analogous to those of the theory of deductive systems, but they are written down by means of the symbol ‘Cn-1’ and not ‘Cn’. There are established the properties of introduced notions and differences and analogies taking place between them and properties of respective notions of the theory T. There are also given generalizations of the notions of ‘decidable system’ and ‘consistent system’ used by Łukasiewicz. The short Chapter II contains axioms of the system T’ which is equivalent to the system T. The only difference between sets of primitive notions of these systems consists in the appearance of the function Cn-1 in the system T’ instead of the function Cn. This chapter reproduces the results given in (2), but they are partially simplified. (shrink)

Model-theoretic 1-types overa given first-order theory T may be construed as natural metalogical miniatures of G. W. Leibniz' ``complete individual notions'', ``substances'' or ``substantial forms''. This analogy prompts this essay's modal semantics for an essentiallyundecidable first-order theory T, in which one quantifies over such ``substances'' in a boolean universe V(C), where C is the completion of the Lindenbaum-algebra of T.More precisely, one can define recursively a set-theoretic translate of formulae νNϕ of formulae ν of a normal modal theory Tm (...) based on T, such that the counterpart `ξi' of a the modal variable `xi' of L(Tm) in this translation-scheme ranges over elements of V(C) that are 1-types of T with value 1 (sometimes called `definite' C-valued 1-types of T).The article's basic completeness-result (2.13) then establishes that ϕvarphi; is a theorem of Tm iff [[νN(ϕ) is aconsequenceof νN(Tm) for each extension N of T which is a subtheory of the canonical generic theory (ultrafilter) u]] = 1 – or equivalently, that Tm is consistent iff[[there is anextension N of T such that N is a subtheory of the canonical generic theory u, and νN(ϕ) for all ϕ in Tm]] > 0.The proof of thiscompleteness-result also shows that an N which provides a countermodel for a modally unprovable ϕ – or equivalently, a closed set in the Stone space St(T) in the sense of V(C) – is intertranslatable with an `accessibility'-relation of a closely related Kripke-semantics whose `worlds' are generic extensions of an initial universe V via C.This interrelation providesa fairly precise rationale for the semantics' recourse to C-valued structures, and exhibits a sense in which the boolean-valued context is sharp. (shrink)

We describe a natural deduction system NDIL for the second order intuitionistic linear logic which admits normalization and has a subformula property. NDIL is an extension of the system for !-free multiplicative linear logic constructed by the author and elaborated by A. Babaev. Main new feature here is the treatment of the modality !. It uses a device inspired by D. Prawitz' treatment of S4 combined with a construction $<\Gamma>$ introduced by the author to avoid cut-like constructions used in $\otimes$ (...) -elimination and global restrictions employed by Prawitz. Normal form for natural deduction is obtained by Prawitz translation of cut-free sequent derivations. (shrink)

Several extensions of Gödel's system TT with new forms of recursion have been designed for the purpose of giving a computational interpretation to classical analysis. One can organise many of these extensions into two groups: those based on bar recursion , which include Spector's original bar recursion, modified bar recursion and the more recent products of selections functions, or those based on open recursion which in particular include the symmetric Berardi–Bezem–Coquand functional. We relate these two groups by showing that both (...) open recursion and the BBC functional are primitive recursively equivalent to a variant of modified bar recursion. Our results, in combination with existing research, essentially complete the classification up to primitive recursive equivalence of those extensions of system TT used to give a direct computational interpretation to choice principles. (shrink)

The notion of a minimal form is defined as an extension of the notion of a normal form in λ-β-calculus and its meaning is discussed in a computational environment. The features of the Knuth-Gross reduction strategy are used to prove that to possess a minimal form, for a generic term, is a semidecidable predicate.

We introduce the notion of τ-like partial order, where τ is one of the linear order types ω, ω*, ω + ω*, and ζ. For example, being ω-like means that every element has finitely many predecessors, while being ζ-like means that every interval is finite. We consider statements of the form “any τ-like partial order has a τ-like linear extension” and “any τ-like partial order is embeddable into τ” . Working in the framework of reverse mathematics, we show that (...) these statements are equivalent either to equation image or to equation image over the usual base system equation image. (shrink)

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)

For any subset $Z \subseteq {\mathbb {Q}}$, consider the set $S_Z$ of subfields $L\subseteq {\overline {\mathbb {Q}}}$ which contain a co-infinite subset $C \subseteq L$ that is universally definable in L such that $C \cap {\mathbb {Q}}=Z$. Placing a natural topology on the set ${\operatorname {Sub}({\overline {\mathbb {Q}}})}$ of subfields of ${\overline {\mathbb {Q}}}$, we show that if Z is not thin in ${\mathbb {Q}}$, then $S_Z$ is meager in ${\operatorname {Sub}({\overline {\mathbb {Q}}})}$. Here, thin and meager both mean “small”, (...) in terms of arithmetic geometry and topology, respectively. For example, this implies that only a meager set of fields L have the property that the ring of algebraic integers $\mathcal {O}_L$ is universally definable in L. The main tools are Hilbert’s Irreducibility Theorem and a new normal form theorem for existential definitions. The normal form theorem, which may be of independent interest, says roughly that every $\exists $-definable subset of an algebraic extension of ${\mathbb Q}$ is a finite union of single points and projections of hypersurfaces defined by absolutely irreducible polynomials. (shrink)

We generalize a theorem of Mundici relating compactness of a regular logic L to a strong form of normality of the associated spaces of models. Moreover, it is shown that compactness is in fact equivalent to ordinary normality of the model spaces when L has uniform reduction for infinite disjoint sums of structures. Some applications follow. For example, a countably generated logic is countably compact if and only if every clopen class in the model spaces is elementary. The model (...) spaces of L are not normal for vocabularies of uncountable power ωα. It also follows that first-order logic is the only finite-dependence logic having normal model spaces and satisfying at the same time the downward Löwenheim-Skolem theorem and uniform reduction for pairs. (shrink)

Discussions of life extension ethics have focused mainly on whether an extended life would be desirable to have, and on the social consequences of widely available life extension. I want to explore a different range of issues: four ways in which the advent of life extension will change our relationship with death, not only for those who live extended lives, but also for those who cannot or choose not to. Although I believe that, on balance, the reasons in favor of (...) developing life extension outweigh the reasons against doing so, most of these changes probably count as reasons against doing so. First, the advent of life extension will alter the human condition for those who live extended lives, and not merely by postponing death. Second, it will make death worse for those who lack access to life extension, even if those people live just as long as they do now. Third, for those who have access to life extension but prefer to live a normal lifespan because they think that has advantages, the advent of life extension will somewhat reduce some of those advantages, even if they never use life extension. Fourth, refusing life extension turns out to be a form of suicide, and this will force those who have access to life extension but turn it down to choose between an extended life they don't want and a form of suicide they may consider immoral. (shrink)

A novel normal form for propositional theories underlies the logic pdl, which captures some essential features of natural discourse, independent from any particular subject matter and related only to its referential structure. In particular, pdlallows to distinguish vicious circularity from the innocent one, and to reason in the presence of inconsistency using a minimal number of extraneous assumptions, beyond the classical ones. Several, formally equivalent decision problems are identified as potential applications: non-paradoxical character of discourses, admissibility of arguments (...) in argumentation networks, propositional satisfiability, and the existence of kernels of directed graphs. Directed graphs provide the basis for the semantics of pdl and the paper concludes by an overview of relevant graph-theoretical results and their applications in diagnosing paradoxical character of natural discourses. (shrink)

Some varieties that are extensions of relational algebras with two constants that play the role of projections are studied. The classes have as a subvariety the abstract fork algebra equivalent variety involving projections. They are obtained by weakening some laws valid in AFA. Some applications of the varieties in the literature and in the specification of abstract data types are exhibited. For each of the classes obtained, an answer is given to the question: 'Is the relational reduct of the class (...) representable?'. For the subvarieties formed with the models that have a representable relational reduct, a representation theorem is proved. For them the finitization problem is studied. Next the varieties presented are compared by means of the inclusion order. For each class the problem of characterizing finite models is considered. Simple models in the varieties are studied. Finally the existence of equivalent classes with a binary operation like fork is studied. (shrink)

Brian Skyrms constructs a theory of "dynamic deliberation" and uses it to investigate rational decision-making in cases of strategic interaction. This illuminating book will be of great interest to all those in many disciplines who use decision theory and game theory to study human behavior and thought. Skyrms begins by discussing the Bayesian theory of individual rational decision and the classical theory of games, which at first glance seem antithetical in the criteria used for determining action. In his effort to (...) show how methods for dealing with information feedback can be productively combined, the author skillfully leads us through the mazes of equilibrium selection, the Nash equilibria for normal and extensive forms, structural stability, causal decision theory, dynamic probability, the revision of beliefs, and, finally, good habits for decision. The author provides many clarifying illustrations and a handy appendix called "Deliberational Dynamics on Your Personal Computer." His powerful model has important implications for understanding the rational origins of convention and the social contract, the logic of nuclear deterrence, the theory of good habits, and the varied strategies of political and economic behavior. (shrink)

Given a 1-ary sentence operator , we describe L - another 1-ary operator - as as a left inverse of in a given logic if in that logic every formula is provably equivalent to L. Similarly R is a right inverse of if is always provably equivalent to R. We investigate the behaviour of left and right inverses for taken as the operator of various normal modal logics, paying particular attention to the conditions under which these logics are conservatively (...) extended by the addition of such inverses, as well as to the question of when, in such extensions, the inverses behave as normal modal operators in their own right. (shrink)

G3-style sequent calculi for the logics in the cube of non-normal modal logics and for their deontic extensions are studied. For each calculus we prove that weakening and contraction are height-preserving admissible, and we give a syntactic proof of the admissibility of cut. This implies that the subformula property holds and that derivability can be decided by a terminating proof search whose complexity is in Pspace. These calculi are shown to be equivalent to the axiomatic ones and, therefore, they (...) are sound and complete with respect to neighbourhood semantics. Finally, a Maehara-style proof of Craig’s interpolation theorem for most of the logics considered is given. (shrink)