Proof nets provide abstract counterparts to sequent proofs modulo rule permutations; the idea being that if two proofs have the same underlying proof-net, they are in essence the same proof. Providing a convincing proof-net counterpart to proofs in the classical sequent calculus is thus an important step in understanding classical sequent calculus proofs. By convincing, we mean that there should be a canonical function from sequent proofs to proof nets, it should be possible to (...) check the correctness of a net in polynomial time, every correct net should be obtainable from a sequent calculus proof, and there should be a cut-elimination procedure which preserves correctness.Previous attempts to give proof-net-like objects for propositional classical logic have failed at least one of the above conditions. In Richard McKinley [22], the author presented a calculus of proof nets satisfying and ; the paper defined a sequent calculus corresponding to expansion nets but gave no explicit demonstration of . That sequent calculus, called LK⁎LK⁎ in this paper, is a novel one-sided sequent calculus with both additively and multiplicatively formulated disjunction rules. In this paper [22]), we give a full proof of for expansion nets with respect to LK⁎LK⁎, and in addition give a cut-elimination procedure internal to expansion nets – this makes expansion nets the first notion of proof-net for classical logic satisfying all four criteria. (shrink)

Certain anti-realisms about mathematics are distinguished by their taking proof rather than truth as the central concept in the account of the meaning of mathematical statements. This notion of proof which is meaning determining or canonical must be distinguished from a notion of demonstration as more generally conceived. This paper raises a set of objections to Dummett's characterisation of the notion via the notion of a normalised natural deduction proof. The main complaint is that Dummett's use (...) of normalised natural deduction proofs relies on formalisation playing a role for which it is unfit. Instead I offer an alternative account which does not rely on formalisation and go on to examine the relation of proof to canonical proof, arguing that rather than requiring an explicit characterisation of canonical proofs we need to be more aware of the complexities of that relation. (shrink)

Since the application of Postulate I.2 in Euclid's Elements is not uniform, one could wonder in what way should it be applied in Euclid's plane geometry. Besides legitimizing questions like this from the perspective of a philosophy of mathematical practice, we sketch a general perspective of conceptual analysis of mathematical texts, which involves an extended notion of mathematical theory as system of authorizations, and an audience-dependent notion of proof.

In different papers, Carnielli, W. & Rodrigues, A., Carnielli, W. Coniglio, M. & Rodrigues, A. and Rodrigues & Carnielli, present two logics motivated by the idea of capturing contradictions as conflicting evidence. The first logic is called BLE and the second—that is a conservative extension of BLE—is named LETJ. Roughly, BLE and LETJ are two non-classical logics in which the Laws of Explosion and Excluded Middle are not admissible. LETJ is built on top of BLE. Moreover, LETJ is a Logic (...) of Formal Inconsistency. This means that there is an operator that, roughly speaking, identifies a formula as having classical behavior. Both systems are motivated by the idea that there are different conditions for accepting or rejecting a sentence of our natural language. So, there are some special introduction and elimination rules in the theory that are capturing different conditions of use. Rodrigues & Carnielli’s paper has an interesting and challenging idea. According to them, BLE and LETJ are incompatible with dialetheia. It seems to show that these paraconsistent logics cannot be interpreted using truth-conditions that allow true contradictions. In short, BLE and LETJ talk about conflicting evidence avoiding to talk about gluts. I am going to argue against this point of view. Basically, I will firstly offer a new interpretation of BLE and LETJ that is compatible with dialetheia. The background of my position is to reject the one canonical interpretation thesis: the idea according to which a logical system has one standard interpretation. Then, I will secondly show that there is no logical basis to fix that Rodrigues & Carnielli’s interpretation is the canonical way to establish the content of logical notions of BLE and LETJ. Furthermore, the system LETJ captures inside classical logic. Then, I am also going to use this technical result to offer some further doubts about the one canonical interpretation thesis. (shrink)

The paper proposes an extension of the definition of a canonical proof, central to proof-theoretic semantics, to a definition of a canonical derivation from open assumptions. The impact of the extension on the definition of (reified) proof-theoretic meaning of logical constants is discussed. The extended definition also sheds light on a puzzle regarding the definition of local-completeness of a natural-deduction proof-system, underlying its harmony.

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)

Canonical extension has proven to be a powerful tool in algebraic study of propositional logics. In this paper we describe a generalisation of the theory of canonical extension to the setting of first order logic. We define a notion of canonical extension for coherent categories. These are the categorical analogues of distributive lattices and they provide categorical semantics for coherent logic, the fragment of first order logic in the connectives ∧, ∨, 0, 1 and ∃. We describe (...) a universal property of our construction and show that it generalises the existing notion of canonical extension for distributive lattices. Our new construction for coherent categories has led us to an alternative description of the topos of types, introduced by Makkai in [22]. This allows us to give new and transparent proofs of some properties of the action of the topos of types construction on morphisms. Furthermore, we prove a new result relating, for a coherent category C, its topos of types to its category of models. (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)

The canonical pair of a proof system P is the pair of disjoint NP sets where one set is the set of all satisfiable CNF formulas and the other is the set of CNF formulas that have P-proofs bounded by some polynomial. We give a combinatorial characterization of the canonical pairs of depth d Frege systems. Our characterization is based on certain games, introduced in this article, that are parametrized by a number k, also called the depth. (...) We show that the canonical pair of a depth d Frege system is polynomially equivalent to the pair (Ad+2,Bd+2) where Ad+2 (respectively, Bd+1) are depth d+1 games in which Player I (Player II) has a positional winning strategy. Although this characterization is stated in terms of games, we will show that these combinatorial structures can be viewed as generalizations of monotone Boolean circuits. In particular, depth 1 games are essentially monotone Boolean circuits. Thus we get a generalization of the monotone feasible interpolation for Resolution, which is a property that enables one to reduce the task of proving lower bounds on the size of refutations to lower bounds on the size of monotone Boolean circuits. However, we do not have a method yet for proving lower bounds on the size of depth d games for d>1. (shrink)

We present a canonical form for definable subsets of algebraically closed valued fields by means of decompositions into sets of a simple form, and do the same for definable subsets of real closed valued fields. Both cases involve discs, forming "Swiss cheeses" in the algebraically closed case, and cuts in the real closed case. As a step in the development, we give a proof for the fact that in "most" valued fields F, if f(x),g(x) ∈ F[ x] and (...) v is the valuation map, then the set {x : v(f(x)) ≤ v(g(x))} is a Boolean combination of discs; in fact, it is a finite union of Swiss cheeses. The development also depends on the introduction of "valued trees", which we define formally. (shrink)

David Lewis proved in 1974 that all logics without iterative axioms are weakly complete. In this paper we extend Lewis's ideas and provide a proof that such logics are canonical and so strongly complete. This paper also discusses the differences between relational and neighborhood frame semantics and poses a number of open questions about the latter.

We define the notions of a canonical inference rule and a canonical system in the framework of single-conclusion Gentzen-type systems (or, equivalently, natural deduction systems), and prove that such a canonical system is non-trivial iff it is coherent (where coherence is a constructive condition). Next we develop a general non-deterministic Kripke-style semantics for such systems, and show that every constructive canonical system (i.e. coherent canonical single-conclusion system) induces a class of non-deterministic Kripke-style frames for which (...) it is strongly sound and complete. We use this non-deterministic semantics to show that all constructive canonical systems admit a strong form of the cut-elimination theorem. We also use it for providing a decision procedure for every such system. These results identify a large family of basic constructive connectives, each having both a proof-theoretical characterization in terms of a coherent set of canonical rules, as well as a semantic characterization using non-deterministic frames. The family includes the standard intuitionistic connectives, together with many other independent connectives. (shrink)

We develop canonical rules capable of axiomatizing all systems of multiple-conclusion rules over K4 or IPC, by extension of the method of canonical formulas by Zakharyaschev [37]. We use the framework to give an alternative proof of the known analysis of admissible rules in basic transitive logics, which additionally yields the following dichotomy: any canonical rule is either admissible in the logic, or it is equivalent to an assumption-free rule. Other applications of canonical rules include (...) a generalization of the Blok–Esakia theorem and the theory of modal companions to systems of multiple-conclusion rules or (finitary structural global) consequence relations, and a characterization of splittings in the lattices of consequence relations over monomodal or superintuitionistic logics with the finite model property. (shrink)

We prove a number of consistency results complementary to the ZFC results from our paper [J. Cummings, M. Foreman, M. Magidor, Canonical structure in the universe of set theory: part one, Annals of Pure and Applied Logic 129 211–243]. We produce examples of non-tightly stationary mutually stationary sequences, sequences of cardinals on which every sequence of sets is mutually stationary, and mutually stationary sequences not concentrating on a fixed cofinality. We also give an alternative proof for the consistency (...) of the existence of stationarily many non-good points, show that diagonal Prikry forcing preserves certain stationary reflection properties, and study the relationship between some simultaneous reflection principles. Finally we show that the least cardinal where square fails can be the least inaccessible, and show that weak square is incompatible in a strong sense with generic supercompactness. (shrink)

We give a simple proof of the canonicity of Sahlqvist identities, using methods that were introduced in a paper by Jónsson and Tarski in 1951.

Proofs of God in Early Modern Europe offers a fascinating window into early modern efforts to prove God’s existence. Assembled here are twenty-two key texts, many translated into English for the first time, which illustrate the variety of arguments that philosophers of the seventeenth and eighteenth centuries offered for God. These selections feature traditional proofs—such as various ontological, cosmological, and design arguments—but also introduce more exotic proofs, such as the argument from eternal truths, the argument from universal aseity, and the (...) argument ex consensu gentium. Drawn from the work of eighteen philosophers, this book includes both canonical figures (such as Descartes, Spinoza, Newton, Leibniz, Locke, and Berkeley) and noncanonical thinkers (such as Norris, Fontenelle, Voltaire, Wolff, Du Châtelet, and Maupertuis). -/- Lloyd Strickland provides fresh translations of all selections not originally written in English and updates the spelling and grammar of those that were. Each selection is prefaced by a lengthy headnote, giving a biographical account of its author, an analysis of the main argument(s), and important details about the historical context. Strickland’s introductory essay provides further context, focusing on the various reasons that led so many thinkers of early modernity to develop proofs of God’s existence. -/- Proofs of God is perfect for both students and scholars of early modern philosophy and philosophy of religion. (shrink)

‘Morgan's canon’ is a rule for making inferences from animal behaviour about animal minds, proposed in 1892 by the Bristol geologist and zoologist C. Lloyd Morgan, and celebrated for promoting scepticism about the reasoning powers of animals. Here I offer a new account of the origins and early career of the canon. Built into the canon, I argue, is the doctrine of the Oxford philologist F. Max Müller that animals, lacking language, necessarily lack reason. Restoring the Müllerian origins of the (...) canon in turn illuminates a number of changes in Morgan's position between 1892 and 1894. I explain these changes as responses to the work of the American naturalist R. L. Garner. Where Morgan had a rule for interpreting experiments with animals, Garner had an instrument for doing them: the Edison cylinder phonograph. Using the phonograph, Garner claimed to provide experimental proof that animals indeed spoke and reasoned. (shrink)

We show that for finite n⩾3n⩾3, every first-order axiomatisation of the varieties of representable n-dimensional cylindric algebras, diagonal-free cylindric algebras, polyadic algebras, and polyadic equality algebras contains an infinite number of non-canonical formulas. We also show that the class of structures for each of these varieties is non-elementary. The proofs employ algebras derived from random graphs.

Our main results are:Theorem 1. Con implies Con. [In fact equiconsistency holds.]Theorem 3. Con implies Con.Theorem 5. Con ”) implies Con.We start with a discussion of the canonical functions and look at some combinatorial principles. Assuming the domination property of Theorem 1, we use the Ketonen diagram to show that ω2V is a limit of measurable cardinals in Jensen’s core model KMO for measures of order zero. Using related arguments we show that ω2V is a stationary limit of measurable (...) cardinals in KMO, if there exists a weakly normal ultrafilter on ω1. The proof yields some other results, e.g., on the consistency strength of weak*-saturated filters on ω1, which are of interest in view of the classical Ulam problem. (shrink)

What do you want to photograph? Nature? Fascinating places you visit? Family activities? Whatever your passion, your Canon Digital Rebel lets you leave limitations behind and express your creativity. This convenient guide is packed with helpful information you'll use almost every time you pull out your Digital Rebel? camera essentials, photography basics, and fail-proof formulas for creating dynamite photos, all richly illustrated in full color. It'll be the second most important tool in your camera bag.

In lieu of an abstract, here is a brief excerpt of the content:American Journal of Philology 123.1 (2002) 119-122 [Access article in PDF] Mary Depew and Dirk Obbink, eds. Matrices of Genre: Authors, Canons, and Society. Center for Hellenic Studies Colloquia 4. Cambridge, Mass.: Harvard University Press, 2000. vi + 346 pp. Cloth, $50. The present collection of essays, which originated as a colloquium at the Center for Hellenic Studies, starts, in the words of editor and organizer Dirk Obbink, from (...) the premise that "genre is a conceptual orienting device that suggests to the hearer the sort of receptorial conditions in which a fictive discourse might have been delivered." Obbink goes on to note that, as the discussion at the colloquium developed, "a more text-based conception of authorial performance" began to emerge (6). This evolution in turn parallels the movement in the volume from an initial discussion of archaic and classical Greek genres to those of Hellenistic poetry and its Roman imitators. One can only applaud this attempt to provide a more sophisticated framework for the reading and reception of ancient literature. As befits the stature of the sponsoring institution and of the many distinguished participants, all the contributions are of an unquestionable competence. In the end, however, it is unclear that we have achieved a more complex, refined, or problematized concept of genre than that with which we began. Indeed, with a few exceptions, most of the modern debates about the concept of genre are either ignored or cited in passing rather than directly engaged. Nonetheless, there are a number of interesting and important individual papers in this volume and only a few that disappoint.Among the most praiseworthy is Eric Csapo's "From Aristophanes to Menander? Genre Transformation in Greek Comedy." Csapo takes dead aim at the traditional narrative of the evolution from a politically engaged Old Comedy of ribald invective to an apolitical plot-centered New Comedy typified by Menander and his Roman epigones. Csapo's argument is that this narrative was manufactured, not through the accidents of preservation, but through a deliberate selection and canonization of texts by early Peripatetic critics and scholars. When we characterize Old Comedy as being typified by Aristophanes' carnivalesque assaults on the Athenian political establishment and then point to his plays as proof, we are not only engaging in circular reasoning, we are also treading a path that has been deliberately and tendentiously drawn for us. Thus, while the traditional narrative depicts a linear evolution from iambic to Old Comedy to New Comedy, which is portrayed as a movement from the personal and the topical to the universal and the apolitical, Aristotle himself, as Csapo notes (117), admits that Crates, Aristophanes' predecessor, abandoned the iambic and began to compose generalizing plots (Po. 1449b7-8). In short, plots of the kind deemed [End Page 119] typical of New Comedy are to be found at the very beginning of the comic form. By the same token, we have evidence of political comedy surviving well past Aristophanes' supposed invention of the Middle Comic style in the Plutus. Indeed, the last example of an Athenian comedy of political invective is Demetrius' Areopagite, dating from circa 294 B.C.E.Csapo's argument, of course, is not a simpleminded refusal to acknowledge change but rather an attempt to rethink the historical evolution of the comic genre outside the bounds of a narrow, teleological narrative. Genres are always complex negotiations between competing conceptions of the same form by different producers and consumers. At various times, for various intrinsic and extrinsic reasons, different versions of the same form will be ascendant or fading into eclipse. But it is never a question of an essence that either unfolds its fullness over time or declines from a single ideal instantiation.Less revolutionary but equally persuasive is Joseph W. Day's "Epigram and Reader: Generic Force as (Re-)Activation of Ritual." Day examines the relation between dedicatory epigrams on cult statues and their ritual contexts by arguing that the dedicatory genre is essentially performative rather than constative. These epigrams do their social work by activating a performative context in the mind of the reader... (shrink)

We introduce partial Esakia morphisms, well partial Esakia morphisms, and strong partial Esakia morphisms between Esakia spaces and show that they provide the dual description of (∧, →) homomorphisms, (∧, →, 0) homomorphisms, and (∧, →, ∨) homomorphisms between Heyting algebras, thus establishing a generalization of Esakia duality. This yields an algebraic characterization of Zakharyaschev’s subreductions, cofinal subreductions, dense subreductions, and the closed domain condition. As a consequence, we obtain a new simplified proof (which is algebraic in nature) of (...) Zakharyaschev’s theorem that each intermediate logic can be axiomatized by canonical formulas. (shrink)

Complex frameworks for defining programming languages aim to generate various tools (e.g. interpreters, symbolic execution engines, deductive verifiers, etc.) using only the formal definition of a language. When used at an industrial scale, these tools are constantly updated, and at the same time, it is required to be trustworthy. Ensuring the correctness of such a framework is practically impossible. A solution is to generate proof objects as correctness artefacts that can be checked by an external trusted checker. A logic (...) suitable for developing such frameworks is matching logic. K framework is a canonical example having matching logic-based foundation. Since the (symbolic) configurations of the programs are represented by matching logic patterns, the algorithms computing the dynamics of these configurations can be seen as pattern transformers and a proof object should be generated for the relationship between these patterns. In this paper, we show that conjunctions and disjunctions of patterns, produced by semantics or analysis rules, can be safely normalized using unification and antiunification algorithms. We also provide a prototype implementation of our proof object generation technique and a checker for certifying the generated objects. (shrink)

Families of types are fundamental objects in Martin-Löf type theory. When extending the notion of setoid (type with an equivalence relation) to families of setoids, a choice between proof-relevant or proof-irrelevant indexing appears. It is shown that a family of types may be canonically extended to a proof-relevant family of setoids via the identity types, but that such a family is in general proof-irrelevant if, and only if, the proof-objects of identity types are unique. A (...) similar result is shown for fibre representations of families. The ubiquitous role of proof-irrelevant families is discussed. (shrink)

This paper is the first of a series of three articles that present the syntactic proof of the PA-completeness of the modal system G, by introducing suitable proof-theoretic objects, which also have an independent interest. We start from the syntactic PA-completeness of modal system GL-LIN, previously obtained in [7], [8], and so we assume to be working on modal sequents S which are GL-LIN-theorems. If S is not a G-theorem we define here a notion of syntactic metric d(S, (...) G): we calculate a canonical characteristic fomula H of S (char(S)) so that ⊢G ∼ H → (∼S) and ⊢GL-LIN ∼ H, and the complexity σ of ∼ H gives the distance d(S, G) of S from G. Then, in order to produce the whole completeness proof as an induction on this d(S, G), we introduce the tree-interpretation of a modal sequent Q into PA, that sends the letters of Q into PA-formulas describing the properties of a GL-LIN-proof P of Q: It is also a d(*, G)-metric linked interpretation, since it will be applied to a proof-tree T of ∼ H with H = char(S) and σ(∼ H) = d(S, G). (shrink)

This paper obtains the weak completeness and decidability results for standard systems of modal logic using models built from formulas themselves. This line of work began with Fine (Notre Dame J. Form. Log. 16:229-237, 1975). There are two ways in which our work advances on that paper: First, the definition of our models is mainly based on the relation Kozen and Parikh used in their proof of the completeness of PDL, see (Theor. Comp. Sci. 113-118, 1981). The point is (...) to develop a general model-construction method based on this definition. We do this and thereby obtain the completeness of most of the standard modal systems, and in addition apply the method to some other systems of interest. None of the results use filtration, but in our final section we explore the connection. (shrink)

We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to (...) a derivation in the associated display calculus. A key insight in this converse translation is a canonical representation of display sequents as labeled polytrees. Labeled polytrees, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics. (shrink)

After sketching an argument for radical anti-realism that does not appeal to human limitations but polynomial-time computability in its definition of feasibility, I revisit an argument by Wittgenstein on the surveyability of proofs, and then examine the consequences of its application to the notion of canonical proof in contemporary proof-theoretical-semantics.

The aim of the paper is to develop the notion of partial probability distributions as being more realistic models of belief systems than the standard accounts. We formulate the theory of partial probability functions independently of any classical semantic notions. We use the partial probability distributions to develop a formal semantics for partial propositional calculi, with extensions to predicate logic and higher order languages. We give a proof theory for the partial logics and obtain soundness and completeness results.

We establish the dichotomy property for stable canonical multi-conclusion rules for IPC, K4, and S4. This yields an alternative proof of existence of explicit bases of admissible rules for these logics.

In the first chapter, we discuss Dummett’s idea that the notion of truth arises from the one of the correctness of an assertion. We argue that, in a first-order language, the need of defining truth in terms of the notion of satisfaction, which is yielded by the presence of quantifiers, is structurally analogous to the need of a notion of truth as distinct from the one of correctness of an assertion. In the light of the analogy between predicates in Frege (...) and open formulas in Tarksi, we concentrate on the semantic status of predicates. We register a dual attitude of Dummett towards Frege’s ascription of reference to predicates. On the one it is needed to endow quantifiers with their appropriate meaning. On the other hand, the introduction of concepts, as semantic correlate of predicates, smuggles a realist flavor in the overall semantic picture. In concluding the excursus (and with it the chapter), we stress Dummett’s will of developing a semantic picture free from this realist trait. In the second chapter, we present the idea of a proof-theoretic semantics. As for Frege true sentences denotes the truth-value True, so here closed' (i.e. categorical) valid argumentations denotes proofs. If a language contains implication-like operators, in order to characterize the condition of validity of a closed argumentation one has to introduce a notion of validity applying to ‘open’ (i.e. hypothetical) argumentations. We argue that this problem is analogous to the one posed by quantifiers in Frege-Tarksi’s style semantics. That is, implication forces one to introduce notion of validity for argumentations, which is more substantial than the correctness of the assertion of their conclusions. As we saw, the corresponding claim in the truth-based approach—that quantifiers require one to introduce a notion of truth, which is more substantial than the one of an assertion being correct—was the source of realism. Hence, Dummett proposes to reduce the semantic contribution of open argumentations to the one of their ‘closed instances’. In the truth-based perspective, this would correspond to the denial of the need of introducing concepts as the semantic correlates of predicates. We argue that Dummett’s fear, that an irreducible notion of function (represented by the need of ascribing validity to open argumentations) would lead to realism, turns out to be ill-founded. In the third chapter, we discuss the role played by the notion of truth in the anti-realist account. The notion of truth is what the anti-realist needs to cope with the so-called paradox of deduction. The analysis of the paradox yields to distinguishing between the truth of a sentence and the truth of a sentence being recognized. In terms of these conceptual couple, we reconsider the relationship between truth and assertion in an anti-realist perspective. Grounds are provided for a thesis (which was already advanced in chapter two), according to which the notion of the assertion of a sentence being correct is primarily connected only with the canonical means of establishing a sentence. The possibility of establishing a sentence by indirect means is conceptually dependent on the practice of establishing logical relationship of dependence among sentences. That is, the notion of a closed valid non-canonical argumentation is of any theoretical relevance only in presence of a notion of validity applying to open argumentations. In the fourth chapter, we discuss the possibility of characterizing in the proof-theoretic-semantics a notion of refutation. We develop an original characterization of refutations starting from an informal inductive specification of the condition of refutations of logically complex sentences. A sub-structural logic, called dual-intuitionistic logic, stands to this notion in the same relationship in which intuitionistic logic stands to the notion of proof so far consdered. All notions developed in chapter 2 have their corresponding (dual) ones in the framework developed. In particular, the distinctions canonical/non-canonical and closed/open argumentations. In the refutation based perspective, elimination rules have priority over introductions and the (only) assumption over the (many) conclusions. In the conclusions, we indicate the ingredients that an anti-realist approach to meaning should incorporate, in order to avoid the difficulties we registered. The core of an alternative view is a different conception of the relationship between categorical and hypothetical notions, in which the validity of open argumentations is not reduced to that of their instances, but rather it is directly defined. As a limit case, one would get a notion of validity applying to closed argumentations. (shrink)

We introduce relativized modal algebra homomorphisms and show that the category of modal algebras and relativized modal algebra homomorphisms is dually equivalent to the category of modal spaces and partial continuous p-morphisms, thus extending the standard duality between the category of modal algebras and modal algebra homomorphisms and the category of modal spaces and continuous p-morphisms. In the transitive case, this yields an algebraic characterization of Zakharyaschev’s subreductions, cofinal subreductions, dense subreductions, and the closed domain condition. As a consequence, we (...) give an algebraic description of canonical, subframe, and cofinal subframe formulas, and provide a new algebraic proof of Zakharyaschev’s theorem that each logic over K4 is axiomatizable by canonical formulas. (shrink)

We show the completeness of a Hilbert-style system LK defined by M. Valiev involving the knowledge operator K dedicated to the reasoning with incomplete information. The completeness proof uses a variant of Makinson's canonical model construction. Furthermore we prove that the theoremhood problem for LK is co-NP-complete, using techniques similar to those used to prove that the satisfiability problem for propositional S5 is NP-complete.

Propositional dynamic logic is complete but not compact. As a consequence, strong completeness requires an infinitary proof system. In this paper, we present a short proof for strong completeness of $$\mathsf{PDL}$$ relative to an infinitary proof system containing the rule from [α; β n ]φ for all $$n \in {\mathbb{N}}$$, conclude $$[\alpha;\beta^*] \varphi$$. The proof uses a universal canonical model, and it is generalized to other modal logics with infinitary proof rules, such as epistemic (...) knowledge with common knowledge. Also, we show that the universal canonical model of $$\mathsf{PDL}$$ lacks the property of modal harmony, the analogue of the Truth lemma for modal operators. (shrink)

We suggest an algebraic approach to proof-theoretic analysis based on the notion of graded provability algebra, that is, Lindenbaum boolean algebra of a theory enriched by additional operators which allow for the structure to capture proof-theoretic information. We use this method to analyze Peano arithmetic and show how an ordinal notation system up to 0 can be recovered from the corresponding algebra in a canonical way. This method also establishes links between proof-theoretic ordinal analysis and the (...) work which has been done in the last two decades on provability logic and reflection principles. Because of its abstract algebraic nature, we hope that it will also be of interest for non-prooftheorists. (shrink)

Following Fine [3], p. 20, we say that a normal propositional modal logic is canonical i all its theorems are valid on the frame of its canonical model . In this paper we prove that K1:1, i.e. S4+ J1 L p) p is not canonical y . We say that two points x and y in a frame are co-accessible i xRy; yRx, but x =6 y. Our proof proceeds by showing that A. The canonical (...) model for K1:1 contains a pair of co-accessible points; and B. J1 is not valid on any frame with a pair of co-accessible points. Clearly our result follows immediately from A and B. (shrink)

We present our calculus of higher-level rules, extended with propositional quantification within rules. This makes it possible to present general schemas for introduction and elimination rules for arbitrary propositional operators and to define what it means that introductions and eliminations are in harmony with each other. This definition does not presuppose any logical system, but is formulated in terms of rules themselves. We therefore speak of a foundational account of proof-theoretic harmony. With every set of introduction rules a (...) class='Hi'>canonical elimination rule, and with every set of elimination rules a canonical introduction rule is associated in such a way that the canonical rule is in harmony with the set of rules it is associated with. An example given by Hazen and Pelletier is used to demonstrate that there are significant connectives, which are characterized by their elimination rules, and whose introduction rule is the canonical introduction rule associated with these elimination rules. Due to the availabiliy of higher-level rules and propositional quantification, the means of expression of the framework developed are sufficient to ensure that the construction of canonical elimination or introduction rules is always possible and does not lead out of this framework. (shrink)

The logic $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ was introduced in Robles and Mendéz as a paraconsistent logic which is based on Gödel’s 3-valued matrix, except that Kleene–Łukasiewicz’s negation is added to the language and is used as the main negation connective. We show that $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ is exactly the intersection of $G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ and $G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$, the two truth-preserving 3-valued logics which are based on the same truth tables. We then construct a Hilbert-type system which has for $\to $ as its sole rule of inference, and is (...) strongly sound and complete for $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$. Then we show how, by adding one axiom or one new rule of inference, we get strongly sound and complete systems for $G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ and $G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$. Finally, we provide quasi-canonical Gentzen-type systems which are sound and complete for those logics and show that they are all analytic, by proving the cut-elimination theorem for them. (shrink)

Fix 2 < n < ω and let C A n denote the class of cylindric algebras of dimension n. Roughly, C A n is the algebraic counterpart of the proof theory of first-order logic restricted to the first n var...

This paper articulates and defends a conception of logical form as semantic form revealed by a compositional meaning theory. On this conception, the logical form of a sentence is determined by the semantic types of its primitive terms and their mode of combination as it relates to determining under what conditions it is true. We develop this idea in the framework of truth-theoretic semantics. We argue that the semantic form of a declarative sentence in a language L is revealed by (...) a (canonical) proof of its T- sentence in an interpretive truth theory for L. We give a precise characterization of sameness of logical form between any two declarative sentences in any two languages in terms of the notion of corresponding proofs in interpretive truth theories for the languages. We illustrate the utility of this approach with a number of examples. We then extend the characterization to non-declaratives in a generalization of truth-theoretic semantics that appeals to fulfillment conditions, of which truth conditions are one variety. On this approach, logical forms are not reified, and the notion of sameness of logical form is treated as conceptually basic. We discuss the relation of this conception of logical form to the project of identifying logical constants, reviewing two approaches, one of which takes topic neutrality as central, the other recursion. We argue that the project of identifying logical constants for the purposes of classifying together valid arguments is largely independent of that identifying logical form of sentences, and urge an ecumenical approach to extending talk of logical constants beyond where it is currently well-grounded. (shrink)

We investigate the degree spectra of computable relations on canonically ordered natural numbers $$(\omega,<)$$ ( ω, < ) and integers $$(\zeta,<)$$ ( ζ, < ). As for $$(\omega,<)$$ ( ω, < ), we provide several criteria that fix the degree spectrum of a computable relation to all c.e. or to all $$\Delta _2$$ Δ 2 degrees; this includes the complete characterization of the degree spectra of so-called computable block functions that have only finitely many types of blocks. Compared to Bazhenov (...) et al. (in: LIPIcs, vol 219, pp 8:1–8:20, 2022), we obtain a more general solution to the problem regarding possible degree spectra on $$(\omega,<)$$ ( ω, < ), answering the question whether there are infinitely many such spectra. As for $$(\zeta,<)$$ ( ζ, < ), we prove the following dichotomy result: given an arbitrary computable relation R on $$(\zeta,<)$$ ( ζ, < ), its degree spectrum is either trivial or it contains all c.e. degrees. This result, and the proof techniques required to solve it, extend the analogous theorem for $$(\omega,<)$$ ( ω, < ) obtained by Wright (Computability 7:349–365, 2018), and provide initial insight to Wright’s question whether such a dichotomy holds on computable ill-founded linear orders. This article is an extended version of Bazhenov et al. (in: LIPIcs, vol 219, pp 8:1–8:20, 2022). (shrink)

For a function $f$ with domain $[X]^{n}$, where $X\subseteq\mathbb{N}$, we say that $H\subseteq X$ is canonical for $f$ if there is a $\upsilon\subseteq n$ such that for any $x_{0},\ldots,x_{n-1}$ and $y_{0},\ldots,y_{n-1}$ in $H$, $f=f$ iff $x_{i}=y_{i}$ for all $i\in\upsilon$. The canonical Ramsey theorem is the statement that for any $n\in\mathbb{N}$, if $f:[\mathbb{N}]^{n}\rightarrow\mathbb{N}$, then there is an infinite $H\subseteq\mathbb{N}$ canonical for $f$. This paper is concerned with a model-theoretic study of a finite version of the canonical Ramsey (...) theorem with a largeness condition and also a version of the Kanamori–McAloon principle. As a consequence, we produce new indicators for cuts satisfying $\operatorname{PA}$. (shrink)

In this paper we investigate some families of decision problems associated with a restricted class of Post canonical forms, specifically, those defined over one-letter alphabets whose productions have single premises and contain only one variable. For brevity sake, we call any such form an RPCF (Restricted Post Canonical Form). Constructive proofs are given which show, for any prescribed nonrecursive r.e. many-one degree of unsolvability D, the existence of an RPCF whose word problem is of degree D and an (...) RPCF with axiom whose decision problem is also of degree D. Finally, we show that both of these results are best possible in that they do not hold for one-one degrees. (shrink)

At some step in proving the Liar Paradox in natural language, a sentence is derived that seems overdetermined with respect to its semantic value. This is complemented by Tarski’s Theorem that a formal language cannot consistently contain a naive truth predicate given the laws of logic used in proving the Liar paradox. I argue that proofs of the Eubulidean Liar either use a principle of truth with non-canonical names in a fallacious way or make a fallacious use of substitution (...) of identicals. Tarski never committed the first fallacy and may have himself considered it fallacious. Nevertheless, I clarify that it is fallacious. I then argue substitution of identicals needs to be restricted within the scope of the truth predicate. A logic for truth implementing this restriction is a monotonic extension of a classical first order logic, or indeed a formalizable fragment of natural language. Proofs of Tarski’s Indefinability of Truth theorem are invalid in this logic. This approach generalizes to invalidate proofs of Liar-like paradoxes, particularly the predicate form of the Knower paradox. Consequently, such a logic can be further extended in a way that avoids Montague’s theorem for such a system. Yet, the semantic status of a Liar sentence is not fully resolved. It is no longer overdetermined; it is now underdetermined. (shrink)

ABSTRACT E. M. Curley has said that Descartes’ cogito, ergo sum “is as obscure on examination as it is compelling at first glance.” Why should that be? Maybe because the cogito raises so many textual and interpretive questions. Is it an argument or an intuition? If it is an argument, does it require an additional premise? Is it best interpreted as a “performance?” Is it best seen as the discovery that any reason proposed for doubting its success entails the meditator’s (...) existence? And so on. But all these questions typically arise in the wake of worries about the cogency of the cogito when it is treated as an argument and worded in its canonical form, “I think, therefore I exist.” In this essay, I focus on what I take to be the most fundamental reason for questioning the cogito’s cogency when it is so treated—namely that the “I” in its premise is question-begging. I distinguish that reason from other reasons that are sometimes conflated with it, and I argue that it is not a good reason. I then comment on some of the questions mentioned above in light of my defense of the cogito seen in that traditional way. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:The Individualization of Crime in Medieval Canon LawVirpi Mäkinen and Heikki PihlajamäkiIn The Mourning of Christ (c. 1305, fresco at Cappella dell'Arena, Padua, Italy), Giotto di Bondone (c. 1267-1337) depicts the Virgin Mary embracing Christ for the last time after he has been taken down from the cross. Whereas his predecessors in the devotional Byzantine tradition concentrated on flat, still figures, Giotto emphasizes their humanity and individuality. The grief (...) on the Virgin's face is touching and convincing but in a slightly different way than the sorrow experienced by St. John or the other accompanying figures. Even the ten angels following the scene seem to grieve for the Redeemer in their own personal way. The individuality of Giotto's figures may not seem much if we compare it with the seventeenth-century Flemish masters. Giotto's Virgin and her company still show a restraint in their grief which does not seem entirely natural. In late medieval art, however, Giotto's approach was fresh and new, reflecting a trend toward individualization which was not peculiar merely to art but was taking over many other areas of late medieval life as well. Philosophy, theology, and law—the medieval scientiae—were all putting increasing emphasis on the rights and responsibilities of the individual.Nor does this trend leave criminal law and the law of evidence untouched. The medieval development of law was just as revolutionary as the development of other branches of knowledge. Starting in early twelfth-century Bologna, the Corpus Iuris Civilis became an object of systematic academic research and teaching for the first time in history. The development of canon law was perhaps even more striking. Positive, enacted law first became not only an object of academic studies but also an instrument of social engineering in the domain of church law. The hierarchical structure of the worldwide Catholic Church was built and run in conjunction with positive, enacted legislation.1 [End Page 525] The development of criminal law was just as innovative as the changes that took place in other branches of law, with canon lawyers taking the lead. Aspiring for universal power and competing for it with secular rulers, the Church was in need of an efficient system to control disobedient priests and monks and suppress heretical movements.2 The traditional system of criminal control was clearly not sufficient. Canon law, making use of the contemporary trend toward increased individualization in theology, philosophy, and Roman law, was developed to meet the church's need to master the situation.One of the most important and influential developments in thirteenth-century criminal law concerned the individual's criminal intention and responsibility. Before the change criminal responsibility was mainly based on the consequences of a crime. The canon lawyers began to determine different modes of subjective responsibility. In the law of criminal evidence the individual was also shifted from the margins to the center of attention. Earlier criminal evidence had been produced from sources external to the individuality of the defendant, such as oaths, compurgators, and ordeals. In the thirteenth century and with the development of the so-called statutory or legal theory of proof, increasing attention was paid to the stories of both the defendant (in the form of confessions) and the witnesses. The development of criminal law and criminal procedure in the thirteenth and fourteenth centuries can be understood in the context of the simultaneous trend toward individualization that took place in moral philosophy and theology as well as in canon law.3 These connections are not the only way of understanding the modernization of canon criminal law, for the prevailing view sees the transformation in conjunction with the twelfth-century hierarchization and centralization of church bureaucracy. The particular form that the criminal law and law of proof assumed in these changes did not arise out of a vacuum but, however, has to be understood in relation to the neighboring fields of thought.The Human Will and the Individual in Medieval Moral PhilosophyThe primus motor of medieval philosophy, Aristotelianism, encountered its first competing theories in the thirteenth century. One of the most far-reaching ideas concerning human psychology and behavior, developed by the Franciscans... (shrink)

In this article, I try to shed some new light onGrundgesetze§10, §29–§31 with special emphasis on Frege’s criteria and proof of referentiality and his treatment of the semantics of canonical value-range names. I begin by arguing against the claim, recently defended by several Frege scholars, that the first-order domain inGrundgesetzeis restricted to value-ranges, but conclude that there is an irresolvable tension in Frege’s view. The tension has a direct impact on the semantics of the concept-script, not least on (...) the semantics of value-range names. I further argue that despite first appearances truth-value names play a distinguished role as semantic “target names” for “test names” in the criteria of referentiality and do not figure themselves as “test names” regarding referentiality. Accordingly, I show in detail that Frege’s attempt to demonstrate that by virtue of his stipulations “regular” value-range names have indeed been endowed with a unique reference, can plausibly be regarded as a direct application of the context principle. In a subsequent section, I turn to some special issues involved in §10. §10 is closely intertwined with §31 and in my and Richard Heck’s view would have been better positioned between §30 and §31. In a first step, I discuss the piecemeal strategy which Frege applies when he attempts to bestow a unique reference on value-range names in §3, §10–§12. In a second step, I critically analyze his tentative, but predictably unsuccessful proposal to identify all objects whatsoever, including those already clad in the garb of value-ranges, with their unit classes. In conclusion, I present two arguments for my claim that Frege’s identification of the True and the False with their unit classes in §10 is illicit even if both the permutation argument and the identifiability thesis that he states in §10 are regarded as formally sound. The first argument is set out from the point of view of the syntax of his formal language. It suggests though that a reorganization of the exposition of the concept-script would have solved at least one of the problems to which the twin stipulations in §10 give rise. The second argument rests on semantic considerations. If it is sound, it may call into question, if not undermine the legitimacy of the twin stipulations. (shrink)