Citations of:
Add citations
You must login to add citations.


The standard natural deduction rules for the identity predicate have seemed to some not to be harmonious. Stephen Read has suggested an alternative introduction rule that restores harmony but presupposes secondorder logic. Here it will be shown that the standard rules are in fact harmonious. To this end, natural deduction will be enriched with a theory of definitional identity. This leads to a novel conception of canonical derivation, on the basis of which the identity elimination rule can be justified in (...) 



Multialgebras (or hyperalgebras or nondeterministic algebras) have been much studied in mathematics and in computer science. In 2016 Carnielli and Coniglio introduced a class of multialgebras called swap structures, as a semantic framework for dealing with several Logics of Formal Inconsistency (or LFIs) that cannot be semantically characterized by a single finite matrix. In particular, these LFIs are not algebraizable by the standard tools of abstract algebraic logic. In this paper, the first steps towards a theory of nondeterministic algebraization of (...) 

Hilbert’s choice operators τ and ε, when added to intuitionistic logic, strengthen it. In the presence of certain extensionality axioms they produce classical logic, while in the presence of weaker decidability conditions for terms they produce various superintuitionistic intermediate logics. In this thesis, I argue that there are important philosophical lessons to be learned from these results. To make the case, I begin with a historical discussion situating the development of Hilbert’s operators in relation to his evolving program in the (...) 

The article deals with the question of correct reconstruction of and solutions to the ancient paradoxes. Analyzing one contemporary example of a reconstruction of the socalled Crocodile Paradox, taken from Sorensen’s A Brief History of Paradox, the author shows how the original pattern of paradox could have been incorrectly transformed in its meaning by overlooking its adequate historical background. Sorensen’s quoting of Aphthonius, as the author of a certain solution to the paradox, seems to be a systematic failure since the (...) 

There are many ontologies of the world or of specific phenomena such as time, matter, space, and quantum mechanics1. However, ontologies of information are rather rare. One of the reasons behind this is that information is most frequently associated with communication and computing, and not with ‘the furniture of the world’. But what would be the nature of an ontology of information? For it to be of significant import it should be amenable to formalization in a logicogrammatical formalism. A candidate (...) 

In this paper we discuss the distinction between sentence and proposition from the perspective of identity. After criticizing Quine, we discuss how objects of logical languages are constructed, explaining what is Kleene’s congruence—used by Bourbaki with his square—and Paul Halmos’s view about the difference between formulas and objects of the factor structure, the corresponding boolean algebra, in case of classical logic. Finally we present Patrick Suppes’s congruence approach to the notion of proposition, according to which a whole hierarchy of congruences (...) 



The paper concentrates on the problem of adequate reflection of fragments of reality via expressions of language and intersubjective knowledge about these fragments, called here, in brief, language adequacy. This problem is formulated in several aspects, the most being: the compatibility of language syntax with its bilevel semantics: intensional and extensional. In this paper, various aspects of language adequacy find their logical explication on the ground of the formallogical theory T of any categorial language L generated by the socalled classical (...) 



In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([71], 19101912) and Church's simply typed λcalculus of 1940. We first argue that the concept of types has always been present in mathematics, though nobody was incorporating them explicitly as such, before the end of the 19th century. Then we proceed by describing how the logical paradoxes entered the formal systems of Frege, Cantor and Peano concentrating on Frege's (...) 

Because formal systems of symbolic logic inherently express and represent the deductive inference model formal proofs to theorem consequences can be understood to represent sound deductive inference to true conclusions without any need for other representations such as model theory. 



Natural deduction is the type of logic most familiar to current philosophers, and indeed is all that many modern philosophers know about logic. Yet natural deduction is a fairly recent innovation in logic, dating from Gentzen and Ja?kowski in 1934. This article traces the development of natural deduction from the view that these founders embraced to the widespread acceptance of the method in the 1960s. I focus especially on the different choices made by writers of elementary textbooks?the standard conduits of (...) 

Various natural deduction formulations of classical, minimal, intuitionist, and intermediate propositional and firstorder logics are presented and investigated with respect to satisfaction of the separation and subformula properties. The technique employed is, for the most part, semantic, based on general versions of the Lindenbaum and Lindenbaum–Henkin constructions. Careful attention is paid to which properties of theories result in the presence of which rules of inference, and to restrictions on the sets of formulas to which the rules may be employed, restrictions (...) 







Kanger [4] gives a set of twelve axioms for the classical propositional Calculus which, together with modus ponens and substitution, have the following nice properties: (0.1) Each axiom contains $\supset$ , and no axiom contains more than two different connectives. (0.2) Deletions of certain of the axioms yield the intuitionistic, minimal, and classical refutability1 subsystems of propositional calculus. (0.3) Each of these four systems of axioms has the separation property: that if a theorem is provable in such a system, then (...) 

In his 1964 note, ‘Two Additions to Positive Implication’, A. N. Prior showed that standard axioms governing conjunction yield a nonconservative extension of the pure implicational intermediate logic OIC of R. A. Bull. Here, after reviewing the situation with the aid of an adapted form of the Kripke semantics for intuitionistic and intermediate logics, we proceed to illuminate this example by transposing it to the setting of modal logic, and then relate it to the propositional logic of what have been (...) 



This paper is concerned with De Morgan?s explanation of the validity of arguments that involve relational notions. It discusses De Morgan?s expansion of traditional logic aimed at accommodating those inferences, and makes the point that his endeavour is not successful in that the rules that made up his new logic are not sound. Nevertheless, the most important scholarly work on De Morgan?s logic, and contrary to that De Morgan?s mistake is not beyond repair. The rules that determine his new logic (...) 



The purpose of this work is to present Gentzenstyle formulations of S5 and S4 based on sequents of higher levels. Sequents of level 1 are like ordinary sequents, sequents of level 1 have collections of sequents of level 1 on the left and right of the turnstile, etc. Rules for modal constants involve sequents of level 2, whereas rules for customary logical constants of firstorder logic with identity involve only sequents of level 1. A restriction on Thinning on the right (...) 

A natural deduction formulation is given for the intermediate logic called MH by Gabbay in [4]. Prooftheoretic methods are used to show that every deduction can be normalized, that MH is the weakest intermediate logic for which the Glivenko theorem holds, and that the CraigLyndon interpolation theorem holds for it. 

Comparing technical notions of communication and computation leads to a surprising result, these notions are often not conceptually distinguishable. This paper will show how the two notions may fail to be clearly distinguished from each other. The most famous models of computation and communication, Turing Machines and (Shannonstyle) information sources, are considered. The most significant difference lies in the types of statetransitions allowed in each sort of model. This difference does not correspond to the difference that would be expected after (...) 



We present a sequent calculus for the modal logic S4, and building on some relevant features of this system we show how S4 can easily be translated into full propositional linear logic, extending the GrishinOno translation of classical logic into linear logic. The translation introduces linear modalities only in correspondence with S4 modalities. We discuss the complexity of the decision problem for several classes of linear formulas naturally arising from the proposed translations. 



Evidence is given that implication (and its special case, negation) carry the logical strength of a system of formal logic. This is done by proving normalization and cut elimination for a system based on combinatory logic or λcalculus with logical constants for and, or, all, and exists, but with none for either implication or negation. The proof is strictly finitary, showing that this system is very weak. The results can be extended to a "classical" version of the system. They can (...) 

We investigate logical consequence in temporal logics in terms of logical consecutions. i.e., inference rules. First, we discuss the question: what does it mean for a logical consecution to be 'correct' in a propositional logic. We consider both valid and admissible consecutions in linear temporal logics and discuss the distinction between these two notions. The linear temporal logic LDTL, consisting of all formulas valid in the frame 〈L, ≤, ≥〉 of all integer numbers, is the prime object of our investigation. (...) 

The implicational fragment of the logic of relevant implication, $R_\to$ is known to be decidable. We show that the implicational fragment of the logic of ticket entailment, $T_\to$ is decidable. Our proof is based on the consecution calculus that we introduced specifically to solve this 50year old open problem. We reduce the decidability problem of $T_\to$ to the decidability problem of $R_\to$. The decidability of $T_\to$ is equivalent to the decidability of the inhabitation problem of implicational types by combinators over (...) 



This paper introduces a new method of interpreting complex relation terms in a secondorder quantified modal language. We develop a completely general secondorder modal language with two kinds of complex terms: one kind for denoting individuals and one kind for denoting nplace relations. Several issues arise in connection with previous, algebraic methods for interpreting the relation terms. The new method of interpreting these terms described here addresses those issues while establishing an interesting connection between λ and ε calculi. The resulting (...) 

The paper consists of two parts. In the first one I present some general remarks regarding the history of negation and attempt to answer the philosophical question concerning the essence of negation. In the second part I resume the theological teaching on the degrees of certainty and point to five forms of negation – known from other areas of research  as applied in the framework of theological investigations. 

Logic is usually thought to concern itself only with features that sentences and arguments possess in virtue of their logical structures or forms. The logical form of a sentence or argument is determined by its syntactic or semantic structure and by the placement of certain expressions called “logical constants.”[1] Thus, for example, the sentences Every boy loves some girl. and Some boy loves every girl. are thought to differ in logical form, even though they share a common syntactic and semantic (...) 



The standard notion of formal theory, in logic, is in general biased exclusively towards assertion: it commonly refers only to collections of assertions that any agent who accepts the generating axioms of the theory should also be committed to accept. In reviewing the main abstract approaches to the study of logical consequence, we point out why this notion of theory is unsatisfactory at multiple levels, and introduce a novel notion of theory that attacks the shortcomings of the received notion by (...) 





We present some prooftheoretic results for the normal modal logic whose characteristic axiom is \. We present a sequent system for this logic and a hypersequent system for its firstorder form and show that these are equivalent to Hilbertstyle axiomatizations. We show that the question of validity for these logics reduces to that of classical tautologyhood and firstorder logical truth, respectively. We close by proving equivalences with a Fitchstyle proof system for revision theory. 

In the past century the received view of definition in mathematics has been the stipulative conception, according to which a definition merely stipulates the meaning of a term in other terms which are supposed to be already well known. The stipulative conception has been so absolutely dominant and accepted as unproblematic that the nature of definition has not been much discussed, yet it is inadequate. This paper examines its shortcomings and proposes an alternative, the heuristic conception. 



An lhemiimplicative semilattice is an algebra \\) such that \\) is a semilattice with a greatest element 1 and satisfies: for every \, \ implies \ and \. An lhemiimplicative semilattice is commutative if if it satisfies that \ for every \. It is shown that the class of lhemiimplicative semilattices is a variety. These algebras provide a general framework for the study of different algebras of interest in algebraic logic. In any lhemiimplicative semilattice it is possible to define an (...) 







