The aim of this paper is to provide a proof-theoretic characterization of relevant logics including fusion and fission connectives, as well as Ackermann’s truth constant. We achieve this by employing the well-established methodology of labelled sequent calculi. After having introduced several systems, we will conduct a detailed proof-theoretic analysis, show a cut-admissibility theorem, and establish soundness and completeness. The paper ends with a discussion that contextualizes our current work within the broader landscape of the proof theory of relevant logics.

In a previous work we introduced the algorithm \SQEMA\ for computing first-order equivalents and proving canonicity of modal formulae, and thus established a very general correspondence and canonical completeness result. \SQEMA\ is based on transformation rules, the most important of which employs a modal version of a result by Ackermann that enables elimination of an existentially quantified predicate variable in a formula, provided a certain negative polarity condition on that variable is satisfied. In this paper we develop several extensions (...) of \SQEMA\ where that syntactic condition is replaced by a semantic one, viz. downward monotonicity. For the first, and most general, extension \SSQEMA\ we prove correctness for a large class of modal formulae containing an extension of the Sahlqvist formulae, defined by replacing polarity with monotonicity. By employing a special modal version of Lyndon's monotonicity theorem and imposing additional requirements on the Ackermann rule we obtain restricted versions of \SSQEMA\ which guarantee canonicity, too. (shrink)

This paper presents a range of new triviality proofs pertaining to naïve truth theory formulated in paraconsistent relevant logics. It is shown that excluded middle together with various permutation principles such as A → (B → C)⊩B → (A → C) trivialize naïve truth theory. The paper also provides some new triviality proofs which utilize the axioms ((A → B)∧ (B → C)) → (A → C) and (A → ¬A) → ¬A, the fusion connective and the Ackermann constant. (...) An overview over various ways to formulate Leibniz’s law in non-classical logics and two new triviality proofs for naïve set theory are also provided. (shrink)

In the 1920s, David Hilbert proposed a research program with the aim of providing mathematics with a secure foundation. This was to be accomplished by first formalizing logic and mathematics in their entirety, and then showing---using only so-called finitistic principles---that these formalizations are free of contradictions. ;In the area of logic, the Hilbert school accomplished major advances both in introducing new systems of logic, and in developing central metalogical notions, such as completeness and decidability. The analysis of unpublished material presented (...) in Chapter 2 shows that a completeness proof for propositional logic was found by Hilbert and his assistant Paul Bernays already in 1917--18, and that Bernays's contribution was much greater than is commonly acknowledged. Aside from logic, the main technical contribution of Hilbert's Program are the development of formal mathematical theories and proof-theoretical investigations thereof, in particular, consistency proofs. In this respect Wilhelm Ackermann's 1924 dissertation is a milestone both in the development of the Program and in proof theory in general. Ackermann gives a consistency proof for a second-order version of primitive recursive arithmetic which, surprisingly, explicitly uses a finitistic version of transfinite induction up to www . He also gave a faulty consistency proof for a system of second-order arithmetic based on Hilbert's &egr;-substitution method. Detailed analyses of both proofs in Chapter 3 shed light on the development of finitism and proof theory in the 1920s as practiced in Hilbert's school. ;In a series of papers, Charles Parsons has attempted to map out a notion of mathematical intuition which he also brings to bear on Hilbert's finitism. According to him, mathematical intuition fails to be able to underwrite the kind of intuitive knowledge Hilbert thought was attainable by the finitist. It is argued in Chapter 4 that the extent of finitistic knowledge which intuition can provide is broader than Parsons supposes. According to another influential analysis of finitism due to W. W. Tait, finitist reasoning coincides with primitive recursive reasoning. The acceptance of non-primitive recursive methods in Ackermann's dissertation presented in Chapter 3, together with additional textual evidence presented in Chapter 4, shows that this identification is untenable as far as Hilbert's conception of finitism is concerned. Tait's conception, however, differs from Hilbert's in important respects, yet it is also open to criticisms leading to the conclusion that finitism encompasses more than just primitive recursive reasoning. (shrink)

Introduction to mathematical logic. Part 2.Textbook for students in mathematical logic and foundations of mathematics. Platonism, Intuition, Formalism. Axiomatic set theory. Around the Continuum Problem. Axiom of Determinacy. Large Cardinal Axioms. Ackermann's Set Theory. First order arithmetic. Hilbert's 10th problem. Incompleteness theorems. Consequences. Connected results: double incompleteness theorem, unsolvability of reasoning, theorem on the size of proofs, diophantine incompleteness, Loeb's theorem, consistent universal statements are provable, Berry's paradox, incompleteness and Chaitin's theorem. Around Ramsey's theorem.

This work studies some problems connected to the role of negation in logic, treating the positive fragments of propositional calculus in order to deal with two main questions: the proof of the completeness theorems in systems lacking negation, and the puzzle raised by positive paradoxes like the well-known argument of Haskel Curry. We study the constructive com- pleteness method proposed by Leon Henkin for classical fragments endowed with implication, and advance some reasons explaining what makes difficult to extend this constructive (...) method to non-classical fragments equipped with weaker implications (that avoid Curry's objection). This is the case, for example, of Jan Lukasiewicz's n-valued logics and Wilhelm Ackermann's logic of restricted implication. Besides such problems, both Henkin's method and the triviality phenomenon enable us to propose a new positive tableau proof system which uses only positive meta-linguistic resources, and to mo- tivate a new discussion concerning the role of negation in logic proposing the concept of paratriviality. In this way, some relations between positive reasoning and infinity, the possibilities to obtain a ¯first-order positive logic as well as the philosophical connection between truth and meaning are dis- cussed from a conceptual point of view. (shrink)

‎A universal schema for diagonalization was popularized by N. S‎. ‎Yanofsky (2003)‎, ‎based on a pioneering work of F.W‎. ‎Lawvere (1969)‎, ‎in which the existence of a (diagonolized-out and contradictory) object implies the existence of a fixed-point for a certain function‎. ‎It was shown that many self-referential paradoxes and diagonally proved theorems can fit in that schema‎. ‎Here‎, ‎we fit more theorems in the universal‎ ‎schema of diagonalization‎, ‎such as Euclid's proof for the infinitude of the primes and new proofs (...) of G. Boolos (1997) for Cantor's theorem on the non-equinumerosity of a set with its powerset‎. ‎Then‎, ‎in Linear Temporal Logic‎, ‎we show the non-existence of a fixed-point in this logic whose proof resembles the argument of Yablo's paradox (1985‎, ‎1993)‎. ‎Thus‎, ‎Yablo's paradox turns for the first time into a genuine mathematico-logical theorem in the framework of Linear Temporal Logic‎. ‎Again the diagonal schema of the paper is used in this proof; and it is also shown that G. Priest's inclosure schema (1997) can fit in our universal diagonal / fixed-point schema‎. ‎We also show the existence of dominating (Ackermann-like) functions (which dominate a given countable set of functions‎, ‎such as primitive recursive functions) in the schema. (shrink)