Quasi-N4-Lattices

Within the Nelson family, two mutually incomparable generalizations of Nelson constructive logic with strong negation have been proposed so far. The first and more well-known, Nelson paraconsistent logic , results from dropping the explosion axiom of Nelson logic; a more recent series of papers considers the logic (dubbed quasi-Nelson logic ) obtained by rejecting the double negation law, which is thus also weaker than intuitionistic logic. The algebraic counterparts of these logical calculi are the varieties of N4-lattices and quasi-Nelson algebras . In the present paper we propose the class of quasi- N4-lattices as a common generalization of both. We show that a number of key results, including the twist-structure representation of N4-lattices and quasi-Nelson algebras, can be uniformly established in this more general setting; our new representation employs twist-structures defined over Brouwerian algebras enriched with a nucleus operator. We further show that quasi-N4-lattices form a variety that is arithmetical, possesses a ternary as well as a quaternary deductive term, and enjoys EDPC and the strong congruence extension property.

BUNDER’S PARADOX

Systems of illative logic are logical calculi formulated in the untyped λ-calculus supplemented with certain logical constants.1 In this short paper, I consider a paradox that arises in illative logic. I note two prima facie attractive ways of resolving the paradox. The first is well known to be consistent, and I briefly outline a now standard construction used by Scott and Aczel that establishes this. The second, however, has been thought to be inconsistent. I show that this isn’t so, by providing a nonempty class of models that establishes its consistency. I then provide an illative logic which is sound and complete for this class of models. I close by briefly noting some attractive features of the second resolution of this paradox.

PEIRCE’S CALCULI FOR CLASSICAL PROPOSITIONAL LOGIC

This article investigates Charles Peirce’s development of logical calculi for classical propositional logic in 1880–1896. Peirce’s 1880 work on the algebra of logic resulted in a successful calculus for Boolean algebra. This calculus, denoted byPC, is here presented as a sequent calculus and not as a natural deduction system. It is shown that Peirce’s aim was to presentPCas a sequent calculus. The law of distributivity, which Peirce states in 1880, is proved using Peirce’s Rule, which is a residuation, inPC. The transitional systems of the algebra of the copula that Peirce develops since 1880 paved the way to the 1896 graphical system of the alpha graphs. It is shown how the rules of the alpha system reinterpret Boolean algebras, answering Peirce’s statement that logical graphs supply a new system of fundamental assumptions to logical algebra. A proof-theoretic analysis is given for the connection betweenPCand the alpha system.

Logic in the 17th and 18th centuries

Logic in the seventeenth century was characterized by attempts to reconcile older viewpoints, such as those of Ramus and Melanchthon, and by criticism of the nature and scope of traditional logic. F. Bacon indicated induction, rather than deduction, as the object of logic, thus opening the way for a logic of the empirical sciences. Descartes proposed to replace the complicated precepts of old logic by simple rules of method. However, even the authors of the Port-Royal Logic, who were influenced by Descartes, could not follow him all the way and continued to teach traditional doctrines, albeit with a new attention to the doctrine of ideas. Other logicians, following Locke, tried to modernize logic by concentrating on an analysis of human cognitive faculties, of the idea–word relation and of other than certain knowledge, thus broadening the scope of logic so as to account for probability. Another suggestion for the improvement of logic came from those who thought that logic should assume mathematics as an example either for its axiomatic-deductive method or for the inventive techniques of algebra. The last of these suggestions prompted research in the area of logical calculi. But this kind of research benefited from the doctrines devised by non-mathematically oriented authors who thus provided the logical framework in which algebraic techniques would be tried. This general background accounts not only for the exceptional logic of Leibniz, but also for some logical calculi worked out in the eighteenth century.

Formal languages and systems

Formal languages and systems are concerned with symbolic structures considered under the aspect of generation by formal (syntactic) rules, that is, irrespective of their or their components’ meaning(s). In the most general sense, a formal language is a set of expressions. The most important way of describing this set is by means of grammars. Formal systems are formal languages equipped with a consequence operation yielding a deductive system. If one further specifies the means by which expressions are built up (connectives, quantifiers) and the rules from which inferences are generated, one obtains logical calculi of various sorts, especially Frege–Hilbert-style and Gentzen-style systems.

Gentzen, Gerhard Karl Erich (1909–45)

The German mathematician and logician Gerhard Gentzen devoted his life to proving the consistency of arithmetic and analysis. His work should be seen as contributing to the post-Gödelian development of Hilbert’s programme. In this connection he developed several logical calculi. The main device used in his proofs was a theorem in which he proved the eliminability of the inference known as ‘cut’ from a variety of different kinds of proofs. This ‘cut-elimination theorem’ yields the consistency of both classical and intuitionistic logic, and the consistency of arithmetic without complete induction. His later work was aimed at providing consistency proofs for less restricted systems of arithmetic and analysis.