Research output

Conference Paper (in Formal Publication) ()

Classical Logic through the Looking-Glass

Milne P (2016) Classical Logic through the Looking-Glass In: Arazim P, Dancak M (ed.) Logica Yearbook 2015, London: College Publications. Logica 2015, 15.6.2015 - 19.6.2015, Hejnice, Czech Republic.

In Lewis Carroll’s Through the Looking Glass and What Alice Found There, Alice enters through a mirror into the realm reflected. It is, of course, left-right reversed but this is only the start of the fun and games when Alice explores the world on the other side of the mirror. Borrowing, if only in part, Carroll’s theme of inversion, my aim is to take a look at classical logic in something of an inverted way, or, to be more exact, in three somewhat inverted ways. Firstly, I come at proof of the completeness of classical logic in the Lindenbaum-Henkin style backwards: I take for granted the existence of a set Σ for which it holds, for some formula φ, that ψ !in Σ if, and only if, Σu{ψ} |- φ  then read off the rules of inference governing connectives and quantifiers that most directly yield the desired (classical) semantic properties. We thus obtain general elimination rules and what I have elsewhere called general introduction rules. Secondly, the same approach lets us read off a different set of rules: those of the cut-free sequent calculus S' of (Smullyan, 1968). Smullyan uses this calculus in proving the Craig-Lyndon interpolation theorem for first-order logic (without identity and function symbols). By attending very carefully to the steps in Smullyan’s proof, we obtain a strengthening: if φ |- ψ,  /|- ¬φ and /|- ψ then there is an interpolant χ, a formula employing only the non-logical vocabulary common to φ and ψ, such that φ entails χ in the first-order version of Kleene’s 3-valued logic and χ entails ψ in the first-order version of Graham Priest’s Logic of Paradox. The result, which is hidden from view in natural deduction formulations of classical logic, extends, I believe, to firstorder logic with identity. Thirdly, we look at a contraction-free “approximation” to classical propositional logic. Adding the general introduction rules for negation or the conditional leads to Contraction being a derived rule, apparently blurring the distinction between structural and operational rules.

Completeness proof for classical first-order logic; Lindenbaum-Henkin construction; general elimination rules; general introduction rules; Craig interpolation lemma; Kleene’s strong three-valued logic; Logic of Paradox; Łukasiewicz’s infinite-valued logic; Contraction

EditorArazim P, Dancak M
AuthorsMilne Peter
Publication date2016
Date of public distribution06/2015
Date accepted by journal31/03/2016
PublisherCollege Publications
Place of publicationLondon
ISBN 978-1-84890-213-8
© University of Stirling FK9 4LA Scotland UK • Telephone +44 1786 473171 • Scottish Charity No SC011159
My Portal