Intuitionistic logic formalises the foundational ideas of L.E.J. Brouwer’s mathematical programme of intuitionism. It is one of the earliest non-classical logics, and the difference between classical and intuitionistic logic may be interpreted to lie in the law of the excluded middle, which asserts that either a proposition is true or its negation is true. This principle is deemed unacceptable from the constructive point of view, in whose understanding the law means that there is an effective procedure to determine the truth of all propositions. This understanding of the distinction between the two logics supports the view that negation plays a vital role in the formulation of intuitionistic logic.

Nonetheless, the formalisation of negation in intuitionistic logic has not been universally accepted, and many alternative accounts of negation have been proposed. Some seek to weaken or strengthen the negation, and others actively supporting negative inferences that are impossible with it.

This thesis follows this tradition and investigates various aspects of negation in intuitionistic logic. Firstly, we look at a problem proposed by H. Ishihara, which asks how effectively one can conserve the deducibility of classical theorems into intuitionistic logic, by assuming atomic classes of non-constructive principles. The classes given in this section improve a previous class given by K. Ishii in two respects: (a) instead of a single class for the law of the excluded middle, two classes are given in terms of weaker principles, allowing a finer analysis and (b) the conservation now extends to a subsystem of intuitionistic logic called Glivenko’s logic. This section also discusses the extension of Ishihara’s problem to minimal logic.

Secondly, we study the relationship between two frameworks for weak constructive negation, the approach of D. Vakarelov on one hand and the framework of subminimal negation by A. Colacito, D. de Jongh, and A. L. Vargas on the other hand. We capture a version of Vakarelov’s logic with the semantics of the latter framework, and clarify the relationship between the two semantics. This also provides proof-theoretic insights, which results in the formulation of a cut-free sequent calculus for the aforementioned system.

Thirdly, we investigate the ways to unify the formalisations of some logics with contra-intuitionistic inferences. The enquiry concerns paraconsistent logics by R. Sylvan and A. B. Gordienko, as well as the logic of co-negation by G. Priest and of empirical negation by M. De and H. Omori. We take Sylvan’s system as basic, and formulate the frame conditions of the defining axioms of the other systems. The conditions are then used to obtain cut-free labelled sequent calculi for the systems.

Finally, we consider L. Humberstone’s actuality operator for intuitionistic logic, which can be seen as the dualisation of a contra-intuitionistic negation. A compete axiomatisation of intuitionistic logic with actuality operator is given, and comparisons are made for some related operators.

Abstract prepared by Satoru Niki.

E-mail: [email protected]