Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the corresponding frame (...) class is found. The method is a synthesis of a generation of calculi with internalized relational semantics, a Tait–Schütte–Takeuti style completeness proof, and procedures to finitize the countermodel construction. Finitizations for intuitionistic propositional logic are obtained through the search for a minimal derivation, through pruning of infinite branches in search trees by means of a suitable syntactic counterpart of semantic filtration, or through a proof-theoretic embedding into an appropriate provability logic. A number of examples illustrates the method, its subtleties, challenges, and present scope. (shrink)

A sufficient condition for an extension of positive logic with strong negation to be characterized by a class of finite trees is given.

We use formal semantic analysis based on new constructions to study abstract realizability, introduced by Läuchli in 1970, and expose its algebraic content. We claim realizability so conceived generates semantics-based intuitive confidence that the Heyting Calculus is an appropriate system of deduction for constructive reasoning.Well-known semantic formalisms have been defined by Kripke and Beth, but these have no formal concepts corresponding to constructions, and shed little intuitive light on the meanings of formulae. In particular, the completeness proofs for these semantics (...) do not generate confidence in the sufficiency of the Heyting Calculus, since we have no reason to believe that every intuitively constructive truth is valid in the formal semantics.Läuchli has proved completeness for a realizability semantics with formal concepts analogous to constructions. We argue in some detail that, in spite of a certain inherent inexactness of the analogy, every intuitively constructive truth is valid in Läuchli semantics, and therefore the Heyting Calculus is powerful enough to prove all constructive truths. Our argument is based on the postulate that a uniformly constructible object must be communicable in spite of imprecision in our language, and that the permutations in Läuchli's semantics represent conceivable imprecision in a language, while allowing a certain amount of freedom in choosing the particular structure of the language.We give a detailed generalization of Läuchli's proof of completeness for the propositional part of the Heyting Calculus, in order to make explicit constructive and algebraic content.In our treatment, we establish several new results about Läuchli models. We show how to extend the sconing and gluing constructions familiar from Kripke and Frame semantics and Topos theory, to Läuchli models, and use them to give an algebraic approach to countermodel construction. In particular, the Läuchli arguments are given without the restriction to the integers, Z, as a group of permutations, which makes much of the coding scheme used in Läuchli's original paper transparent.We also make use of a new propositions-as-types syntax for the Heyting calculus, with limited nondeterminism, in which validity of formulae can be decided without loop-detection. (shrink)

This paper is the second part of the syntactic demonstration of the Arithmetical Completeness of the modal system G, the first part of which is presented in [9]. Given a sequent S so that ⊢GL-LIN S, ⊬G S, and given its characteristic formula H = char(S), which expresses the non G-provability of S, we construct a canonical proof-tree T of ~ H in GL-LIN, the height of which is the distance d(S, G) of S from G. T is the syntactic (...) countermodel of S with respect to Gand is a tool of general interest in Provability Logic, that allows some classification in the set of the arithmetical interpretations. (shrink)

It is one thing for a given proposition to follow or to not follow from a given set of propositions and it is quite another thing for it to be shown either that the given proposition follows or that it does not follow.* Using a formal deduction to show that a conclusion follows and using a countermodel to show that a conclusion does not follow are both traditional practices recognized by Aristotle and used down through the history of logic. These (...) practices presuppose, respectively, a criterion of validity and a criterion of invalidity each of which has been extended and refined by modern logicians: deductions are studied in formal syntax (proof theory) and coun¬termodels are studied in formal semantics (model theory). The purpose of this paper is to compare these two criteria to the corresponding criteria employed in Boole’s first logical work, The Mathematical Analysis of Logic (1847). In particular, this paper presents a detailed study of the relevant metalogical passages and an analysis of Boole’s symbolic derivations. It is well known, of course, that Boole’s logical analysis of compound terms (involving ‘not’, ‘and’, ‘or’, ‘except’, etc.) contributed to the enlargement of the class of propositions and arguments formally treatable in logic. The present study shows, in addition, that Boole made significant contributions to the study of deduc¬tive reasoning. He identified the role of logical axioms (as opposed to inference rules) in formal deductions, he conceived of the idea of an axiomatic deductive sys¬tem (which yields logical truths by itself and which yields consequences when ap¬plied to arbitrary premises). Nevertheless, surprisingly, Boole’s attempt to imple¬ment his idea of an axiomatic deductive system involved striking omissions: Boole does not use his own formal deductions to establish validity. Boole does give symbolic derivations, several of which are vitiated by “Boole’s Solutions Fallacy”: the fallacy of supposing that a solution to an equation is necessarily a logical consequence of the equation. This fallacy seems to have led Boole to confuse equational calculi (i.e., methods for gen-erating solutions) with deduction procedures (i.e., methods for generating consequences). The methodological confusion is closely related to the fact, shown in detail below, that Boole had adopted an unsound criterion of validity. It is also shown that Boole totally ignored the countermodel criterion of invalid¬ity. Careful examination of the text does not reveal with certainty a test for invalidity which was adopted by Boole. However, we have isolated a test that he seems to use in this way and we show that this test is ineffectual in the sense that it does not serve to identify invalid arguments. We go beyond the simple goal stated above. Besides comparing Boole’s earliest criteria of validity and invalidity with those traditionally (and still generally) employed, this paper also investigates the framework and details of THE MATHEMATICAL ANALYSIS OF LOGIC. (shrink)

In this paper we give relational semantics and an accompanying relational proof theory for full Lambek calculus (a sequent calculus which we denote by FL). We start with the Kripke semantics for FL as discussed in [11] and develop a second Kripke-style semantics, RelKripke semantics, as a bridge to relational semantics. The RelKripke semantics consists of a set with two distinguished elements, two ternary relations and a list of conditions on the relations. It is accompanied by a Kripke-style valuation system (...) analogous to that in [11]. Soundness and completeness theorems with respect to FL hold for RelKripke models. Then, in the spirit of the work of Orlowska [14], [15], and Buszkowski and Orlowska [3], we develop relational logic RFL. The adjective relational is used to emphasize the fact that RFL has a semantics wherein formulas are interpreted as relations. We prove that a sequent Γ → α in FL is provable if and only if a translation, t( $\gamma_1 \bullet \cdots \bullet \gamma_n \supset \alpha)\varepsilon \upsilon u$ , has a cut-complete fundamental proof tree. This result is constructive: that is, if a cut-complete proof tree for $t(\gamma_1 \bullet \cdots \bullet \gamma_n \supset \alpha)\varepsilon \upsilon u$ is not fundamental, we can use the failed proof search to build a relational countermodel for $t(\gamma_1 \bullet \cdots \bullet \gamma_n \supset \alpha)\varepsilon \upsilon u$ and from this, build a RelKripke countermodel for $\gamma_1 \bullet \cdots \bullet \gamma_n \supset \alpha$ . These results allow us to add FL, the basic substructural logic, to the list of those logies of importance in computer science with a relational proof theory. (shrink)

The paper develops a set of quantified temporal alethic boulesic doxastic systems. Every system in this set consists of five parts: a ‘quantified’ part, a temporal part, a modal (alethic) part, a boulesic part and a doxastic part. There are no systems in the literature that combine all of these branches of logic. Hence, all systems in this paper are new. Every system is defined both semantically and proof-theoretically. The semantic apparatus consists of a kind of$$T \times W$$T×Wmodels, and the (...) proof-theoretical apparatus of semantic tableaux. The ‘quantified part’ of the systems includes relational predicates and the identity symbol. The quantifiers are, in effect, a kind of possibilist quantifiers that vary over every object in the domain. The tableaux rules are classical. The alethic part contains two types of modal operators for absolute and historical necessity and possibility. According to ‘boulesic logic’ (the logic of the will), ‘willing’ (‘consenting’, ‘rejecting’, ‘indifference’ and ‘non-indifference’) is a kind of modal operator. Doxastic logic is the logic of beliefs; it treats ‘believing’ (and ‘conceiving’) as a kind of modal operator. I will explore some possible relationships between these different parts, and investigate some principles that include more than one type of logical expression. I will show that every tableau system in the paper is sound and complete with respect to its semantics. Finally, I consider an example of a valid argument and an example of an invalid sentence. I show how one can use semantic tableaux to establish validity and invalidity and read off countermodels. These examples illustrate the philosophical usefulness of the systems that are introduced in this paper. (shrink)

Robert Aumann presents his Agreement Theorem as the key conditional: “if two people have the same priors and their posteriors for an event A are common knowledge, then these posteriors are equal” (Aumann, 1976, p. 1236). This paper focuses on four assumptions which are used in Aumann’s proof but are not explicit in the key conditional: (1) that agents commonly know, of some prior μ, that it is the common prior; (2) that agents commonly know that each of them updates (...) on the prior by conditionalization; (3) that agents commonly know that if an agent knows a proposition, she knows that she knows that proposition (the “K K” principle); (4) that agents commonly know that they each update only on true propositions. It is shown that natural weakenings of any one of these strong assumptions can lead to countermodels to Aumann’s key conditional. Examples are given in which agents who have a common prior and commonly know what probability they each assign to a proposition nevertheless assign that proposition unequal probabilities. To alter Aumann’s famous slogan: people can “agree to disagree”, even if they share a common prior. The epistemological significance of these examples is presented in terms of their role in a defense of the Uniqueness Thesis: If an agent whose total evidence is E is fully rational in taking doxastic attitude D to P, then necessarily, any subject with total evidence E who takes a different attitude to P is less than fully rational. (shrink)

Ned Markosian has recently defended a new theory of composition, which he calls regionalism : some material objects xx compose something if and only if there is a material object located at the fusion of the locations of xx. Markosian argues that regionalism follows from what he calls the subregion theory of parthood. Korman and Carmichael agree. We provide countermodels to show that regionalism does not follow from, even together with fourteen potentially implicit background principles. We then show that (...) regionalism does follow from five of those background principles together with and two additional principles connecting parthood and location, which we call and. While the additional principles are not uncontroversial, our conjecture is that many will find them attractive. We conclude by mentioning that fills a previously unnoticed gap in the formal theory of location presented in Parsons. (shrink)

A novel fatalistic argument that combines elements of modal, temporal, and epistemic logic to prove that the fixed past is not compatible with the open future has recently been presented by Lampert (Analysis 82(3):426–434, 2022). By the construction of a countermodel, it is shown that his line of reasoning is defective. However, it is also explained how Lampert’s argument could be corrected if it were supported with an extra premise regarding the temporal status of a priori knowledge. This additional assumption—which (...) was tacit in the original presentation—is shown to be the weakest link, and it is argued that, despite Lampert’s assurance, it can be plausibly rejected in a roughly Ockhamist framework. Thus, it is concluded that the fixed past poses no threat to the open future; however, a few different lessons about knowledge, necessity, and time are drawn from careful reflection on this novel argument. (shrink)

The aim of this paper is to provide a decision procedure for Dummett's logic LC, such that with any given formula will be associated either a proof in a sequent calculus equivalent to LC or a finite linear Kripke countermodel.

This paper provides a proof-theoretic study of quantified non-normal modal logics. It introduces labelled sequent calculi based on neighbourhood semantics for the first-order extension, with both varying and constant domains, of monotone NNML, and studies the role of the Barcan formulas in these calculi. It will be shown that the calculi introduced have good structural properties: invertibility of the rules, height-preserving admissibility of weakening and contraction and syntactic cut elimination. It will also be shown that each of the calculi introduced (...) is sound and complete with respect to the appropriate class of neighbourhood frames. In particular, the completeness proof constructs a formal derivation for derivable sequents and a countermodel for non-derivable ones, and gives a semantic proof of the admissibility of cut. (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)

According to a leading view, emotions such as admiration, contempt, pride, and shame are important vehicles of agential development. Through admiration and contempt, we establish models and countermodels against which to shape our character; through pride and shame, we get a sense of how we measure up to them. Critics of this view object that these emotions always deliver uncompromising evaluations: admiration casts people in a completely positive light, while contempt casts aspersion on them. Therefore, insofar as they lack (...) the capacity for nuance, these emotions are systematically unfitting and misleading. This paper discusses this objection as originally formulated by John Doris as well as Macalester Bell’s response. Drawing from research on emotional intentionality, it will be argued that Doris’ and Bell’s accounts are respectively misguided criticisms and inadequate defences of these emotions. Their mistake lies in an invalid transition from the claim that these emotions are intentionally directed towards persons to the claim that they deliver global evaluations of those towards whom they are directed. By rejecting this inference, it will be shown that these emotions can deliver nuanced and fitting evaluations in a way Doris’ objection overlooks and Bell’s response precludes us from articulating. (shrink)

An important link between model theory and proof theory is to construe a deductive disproof of S as an attempted construction of a countermodel to it. In the function logic outlined here, this idea is implemented in such a way that different kinds of individuals can be introduced into the countermodel in any order whatsoever. This imposes connections between the length of the branches of the tree that a disproof is and their number. If there are already n individuals in (...) the countermodel that is being constructed, the next individual has to be considered in its relations to each of the n old ones, creating 2^n different cases and accordingly at least 2^n different branches. Hence a disproof procedure of a polynomial length is normally not equivalent with an exponential one. Because every computation can be represented as a deduction with the same number of constant terms, the same holds for nondeterministic computations. Apparent exceptions seem to come about if a branch created by a new individual i is redundant. But when the disproof is a shortest one (contains the minimum number of different constant terms) then not introducing that idle term at all would result in an even shorter disproof, violating the shortness assumption. (shrink)

Ted Sider’s Proportionality of Justice condition requires that any two moral agents instantiating nearly the same moral state be treated in nearly the same way. I provide a countermodel in supervaluation semantics to the proportionality of justice condition. It is possible that moral agents S and S' are in nearly the same moral state, S' is beyond all redemption and S is not. It is consistent with perfect justice then that moral agents that are not beyond redemption go determinately to (...) heaven and moral agents that are beyond all redemption go determinately to hell. I conclude that moral agents that are in nearly the same moral state may be treated in very unequal ways. (shrink)

We investigate sequent calculi for the weak modal (propositional) system reduced to the equivalence rule and extensions of it up to the full Kripke system containing monotonicity, conjunction and necessitation rules. The calculi have cut elimination and we concentrate on the inversion of rules to give in each case an effective procedure which for every sequent either furnishes a proof or a finite countermodel of it. Applications to the cardinality of countermodels, the inversion of rules and the derivability of (...) Löb rules are given. (shrink)

This paper is the final part of the syntactic demonstration of the Arithmetical Completeness of the modal system G; in the preceding parts [9] and [10] the tools for the proof were defined, in particular the notion of syntactic countermodel. Our strategy is: PA-completeness of G as a search for interpretations which force the distance between G and a GL-LIN-theorem to zero. If the GL-LIN-theorem S is not a G-theorem, we construct a formula H expressing the non G-provability of S, (...) so that ⊢GL-LIN ∼ H and so that a canonical proof T of ∼ H in GL-LIN is a syntactic countermodel for S with respect to G, which has the height θ(T) equal to the distance d(S, G) of S from G. Then we define the interpretation ξ of S which represents the proof-tree T in PA. By induction on θ(T), we prove that ⊢PA Sξ and d(S, G) > 0 imply the inconsistency of PA. (shrink)

In classical and intuitionistic arithmetics, any formula implies a true equation, and a false equation implies anything. In weaker logics fewer implications hold. In this paper we rehearse known results about the relevant arithmetic R, and we show that in linear arithmetic LL by contrast false equations never imply true ones. As a result, linear arithmetic is desecsed. A formula A which entails 0 = 0 is a secondary equation; one entailed by 0 6= 0 is a secondary unequation. A (...) system of formal arithmetic is secsed if every extensional formula is either a secondary equation or a secondary unequation. We are indebted to the program MaGIC for the simple countermodel SZ7, on which 0 = 1 is not a secondary formula. This is a small but signi cant success for automated reasoning. (shrink)

We develop multi-conclusion nested sequent calculi for the fifteen logics of the intuitionistic modal cube between IK and IS5. The proof of cut-free completeness for all logics is provided both syntactically via a Maehara-style translation and semantically by constructing an infinite birelational countermodel from a failed proof search. Interestingly, the Maehara-style translation for proving soundness syntactically fails due to the hierarchical structure of nested sequents. Consequently, we only provide the semantic proof of soundness. The countermodel construction used to prove completeness (...) required a completely novel approach to deal with two independent sources of non-termination in the proof search present in the case of transitive and Euclidean logics. (shrink)

A rejection system, also referred to as a complementary calculus, is a proof system axiomatising the invalid formulas of a logic, in contrast to traditional calculi which axiomatise the valid ones. Rejection systems therefore introduce a purely syntactic way of determining non-validity without having to consider countermodels, which can be useful in procedures for automated deduction and proof search. Rejection calculi have first been formally introduced by Łukasiewicz in the context of Aristotelian syllogistic and subsequently rejection systems for many (...) well-known logics have been proposed. In this paper, we deal with rejection systems for so-called non-deterministic finite-valued logics, a special case of non-deterministic many-valued logics which were introduced by Avron and Lev as a generalisation of traditional many-valued logics. More specifically, we introduce a systematic method for constructing sequent-style rejection systems for any given non-deterministic finite-valued logic. Furthermore, as special instances of our method, we provide concrete calculi for specific paraconsistent logics which can be characterised in terms of non-deterministic two- and three-valued semantics, respectively. (shrink)

The main result of the present paper is that the variable-free fragment of logic K*, the logic with a single K-style modality and its “reflexive and transitive closure,” is EXPTIMEcomplete. It is then shown that this immediately gives EXPTIME-completeness of variable-free fragments of a number of known EXPTIME-complete logics. Our proof contains a general idea of how to construct a polynomial-time reduction of a propositional logic to its n-variable—and even, in the cases of K*, PDL, CTL, ATL, and some others, (...) variable-free—fragments. Complexity of countermodels for such fragments is considered. (shrink)

We obtain an effective embedding of the classical predicate logic into the logic of partial quasiary predicates. The embedding has the property that an image of a non-theorem of the classical logic is refutable in a model of the logic of partial quasiary predicates that has the same cardinality as the classical countermodel of the non-theorem. Therefore, we also obtain an embedding of the classical predicate logic of finite models into the logic of partial quasiary predicates over finite structures. As (...) a consequence, we prove that the logic of partial quasiary predicates is undecidable—more precisely, $\varSigma ^0_1$-complete—over arbitrary structures and not recursively enumerable—more precisely, $\varPi ^0_1$-complete—over finite structures. (shrink)

This article discusses two coextensive concepts of logical consequence that are implicit in the two fundamental logical practices of establishing validity and invalidity for premise-conclusion arguments. The premises and conclusion of an argument have information content (they ?say? something), and they have subject matter (they are ?about? something). The asymmetry between establishing validity and establishing invalidity has long been noted: validity is established through an information-processing procedure exhibiting a step-by-step deduction of the conclusion from the premise-set. Invalidity is established by (...) exhibiting a countermodel satisfying the premises but not the conclusion. The process of establishing validity focuses on information content; the process of establishing invalidity focuses on subject matter. Corcoran's information-theoretic concept of logical consequence corresponds to the former. Tarski's model-theoretic concept of logical consequence formulated in his famous 1936 no-countermodels definition corresponds to the latter. Both are found to be indispensable for understanding the rationale of the deductive method and each complements the other. This study discusses the ontic question of the nature of logical consequence and the epistemic question of the human capabilities presupposed by practical applications of these two concepts as they make validity and invalidity accessible to human knowledge. (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)

If two self-connected individuals are connected, it follows in classical extensional mereotopology that the sum of those individuals is self-connected too. Since mainland Europe and mainland Asia, for example, are both self-connected and connected to each other, mainland Eurasia is also self-connected. In contrast, in non-extensional mereotopologies, two individuals may have more than one sum, in which case it does not follow from their being self-connected and connected that the sum of those individuals is self-connected too. Nevertheless, one would still (...) expect it to follow that a sum of connected self-connected individuals is self-connected too. In this paper, we present some surprising countermodels which show that this conjecture is incorrect. (shrink)

According to Whitehead’s rectified principle, two individuals are connected just in case there is something self-connected which overlaps both of them, and every part of which overlaps one of them. Roberto Casati and Achille Varzi have offered a counterexample to the principle, consisting of an individual which has no self-connected parts. But since atoms are self-connected, Casati and Varzi’s counterexample presupposes the possibility of gunk or, in other words, things which have no atoms as parts. So one may still wonder (...) whether Whitehead’s rectified principle follows from the assumption of atomism. This paper presents an atomic countermodel to show the answer is no. (shrink)

Predicate modal formulas are considered as schemata of arithmetical formulas, where is interpreted as the standard formula of provability in a fixed sufficiently rich theory T in the language of arithmetic. QL T(T) and QL T are the sets of schemata of T-provable and true formulas, correspondingly. Solovay's well-known result — construction an arithmetical counterinterpretation by Kripke countermodel — is generalized on the predicate modal language; axiomatizations of the restrictions of QL T(T) and QL T by formulas, which contain no (...) variables different from x, are given by means of decidable prepositional bimodal systems; under the assumption that T is 1-complete, there is established the enumerability of the restrictions of QL T(T) and QL T by: 1) formulas in which the domains of different occurrences of don't intersect and 2) formulas of the form n A. (shrink)

In this paper we prove the completeness of three logical systems I LI, IL2 and IL3. IL1 deals solely with identities {a = b), and its deductions are the direct deductions constructed with the three traditional rules: (T) from a = b and b = c infer a = c, (S) from a = b infer b = a and (A) infer a = a(from anything). IL2 deals solely with identities and inidentities {a ± b) and its deductions include both (...) the direct and the indirect deductions constructed with the three traditional rules. IL3 is a hybrid of IL1 and IL2: its deductions are all direct as in IL1 but it deals with identities and inidentities as in IL2. IL1 and IL2 have a high degree of naturalness. Although the hybrid system IL3 was constructed as an artifact useful in the mathematical study of IL1 and IL2, it nevertheless has some intrinsically interesting aspects. The main motivation for describing and studying such simple systems is pedagogical. In teaching beginning logic one would like to present a system of logic which has the following properties. First, it exemplifies the main ideas of logic: implication, deduction, non-implication, counterargument(or countermodel), logical truth, self-contradiction, consistency,satisfiability, etc. Second, it exemplifies the usual general metaprinciples of logic: contraposition and transitivity of implication, cut laws, completeness,soundness, etc. Third, it is simple enough to be thoroughly grasped by beginners. Fourth, it is obvious enough so that its rules do not appear to be arbitrary or purely conventional. Fifth, it does not invite confusions which must be unlearned later. Sixth, it involves a minimum of presuppositions which are no longer accepted in mainstream contemporary logic. (shrink)

Predicate modal formulas with non-modalized quantifiers (call them Q-formulas) are considered as schemata of arithmetical formulas, where is interpreted as the provability predicate of some fixed correct extension T of arithmetic. A method of constructing 1) non-provable in T and 2) false arithmetical examples for Q-formulas by Kripke-like countermodels of certain type is given. Assuming the means of T to be strong enough to solve the (undecidable) problem of derivability in QGL, the Q-fragment of the predicate version of the (...) logic GL, we prove the recursive enumerability of the sets of Q-formulas all arithmetical examples of which are: 1) T-provable, 2) true. In. particular, the first one is shown to be exactly QGL and the second one to be exactly the Q-fragment of the predicate version of Solovay's logic S. (shrink)

Featuring essays by some of the most prominent names in contemporary political and cultural theory, _Sovereignty in Ruins_ presents a form of critique grounded in the conviction that political thought is itself an agent of crisis. Aiming to develop a political vocabulary capable of critiquing and transforming contemporary political frameworks, the contributors advance a politics of crisis that collapses the false dichotomies between sovereignty and governmentality and between critique and crisis. Their essays address a wide range of topics, such as (...) the role history plays in the development of a politics of crisis; Arendt's controversial judgment of Adolf Eichmann; Strauss's and Badiou's readings of Plato's _Laws_; the acceptance of the unacceptable; the human and nonhuman; and flesh as a biopolitical category representative of the ongoing crisis of modernity. Altering the terms through which political action may take place, the contributors think through new notions of the political that advance countermodels of biopolitics, radical democracy, and humanity. Contributors. Judith Butler, George Edmondson, Roberto Esposito, Carlo Galli, Klaus Mladek, Alberto Moreiras, Andrew Norris, Eric L. Santner, Adam Sitze, Carsten Strathausen, Rei Terada, Cary Wolfe. (shrink)

In this paper we introduce a game semantics for System P, one of the most studied axiomatic systems for non-monotonic reasoning, conditional logic and belief revision. We prove soundness and completeness of the game semantics with respect to the rules of System P, and show that an inference is valid with respect to the game semantics if and only if it is valid with respect to the standard order semantics of System P. Combining these two results leads to a new (...) completeness proof for System P with respect to its order semantics. Our approach allows us to construct for every inference either a concrete proof of the inference from the rules in System P or a countermodel in the order semantics. Our results rely on the notion of a witnessing set for an inference, whose existence is a concise, necessary and sufficient condition for validity of an inferences in System P. We also introduce an infinitary variant of System P and use the game semantics to show its completeness for the restricted class of well-founded orders. (shrink)