Logic Reduced To Bare (Proof-Theoretical) Bones
What is a minimal proof-theoretical foundation of logic? Two different ways to answer this question may appear to offer themselves: reduce the whole of logic either to the relation of inference, or else to the property of incompatibility. The first way would involve defining logical operators in terms of the algebraic properties of the relation of inferencewith conjunction \(\hbox {A}\wedge \hbox {B}\) as the infimum of A and B, negation \(\lnot \hbox {A}\) as the minimal incompatible of A, etc. The second way involves introducing logical operators in terms of the relation of incompatibility, such that X is incompatible with \(\{\lnot \hbox {A}\}\) iff every Y incompatible with X is incompatible with {A}; and X is incompatible with \(\{\hbox {A}\!\wedge \!\hbox {B}\}\) iff X is incompatible with {A,B}; etc. Whereas the first route leads us naturally to intuitionistic logic, the second leads us to classical logic. The aim of this paper is threefold: to investigate the relationship of the two approaches within a very general framework, to discuss the viability of erecting logic on such austere foundations, and to find out whether choosing one of the ways we are inevitably led to a specific logical system.
inference incompatibility intuitionistic logic proof theory