COLLECTED PAPERS OF STIG KANGER WITH ESSAYS ON HIS LlFEAND WORK Vol. I SYNTHESE LIBRARY STUDIES IN EPISTEMOLOGY, LOGIC, METHODOLOGY, AND PHILOSOPHY OF SCIENCE Managing Editor: JAAKKO HINTIKKA,Boston University, U.S.A. Editors: DIRK VANDALEN, University ofUtrecht, TheNetherlands DONALD DAVIDSON, University ofCalifornia, Berkeley, U.S.A. THEO A.F.KUIPERS, University ofGroningen, TheNetherlands PATRICKSUPPES, Stanford University, California, U.S.A. JAN WOLENSKI, Jagiellonian University,Krakow. Poland VOLUME 303 COLLECTED PAPERS OF STIG KANGER WITH ESSAYS ON HIS LIFE ANDWORK VoI. 1 Edited by GHITA HOLMSTROM-HINTIKKA Boston University, Boston, USA. STEN LINDSTROM Umea University, Umea, Sweden and RYSIEK SLIWINSKI Uppsala University, Uppsala, Sweden SPRINGER SCIENCE+BUSINESS MEDIA, B.V. A C.I.P. Catalogue record for this book is available from the Library of Congress. ISBN 978-1-4020-0022-5 ISBN 978-94-010-0500-5 (eBook) DOI 10.1007/978-94-010-0500-5 Printed on acid-free paper Ali Rights Reserved © 2001 Springer Science+Business Media Dordrecht Originally published by Kluwer Academic Publishers in 2001 Softcover reprint of the hardcover 1s t edition 200 1 No part of the material protected by this copyright notice may be reproduced or utilized in any form or by any means, electronic or mechanical, inc1uding photocopying, recording or by any information storage and retrieval system, without written permission from the copyright owner. TABLE OF CONTENTS Introduction vii PURE LOGIC A Note on Partial Postulate Sets for Propositional Logic 3 Provability in Logic 8 The Morning Star Paradox 42 A Note on Quantification and Modalities 52 On the Characterization of Modalities 54 A Simplified ProofMethod for Elementary Logic 58 EquivalentTheories 65 An Algebraic Logic Calculus 70 Equational Calculi and Automatic Demonstration 76 Entailment 82 The Paradox ofthe Unexpected Hanging, Regained Again 94 APPLIED LOGIC: OBLIGATIONS, RIGHTS AND ACTION New Foundations for Ethical Theory 99 Rights and Parliamentarism 120 Law and Logic 146 Some Aspects on the Concept of Influence 170 On Realization ofHuman Rights 179 Unavoidability 186 Unavoidability. Appendix 192 APPLIED LOGIC: PREFERENCE AND CHOICE Preference Logic 199 A Note on Preference-Logic 209 Choice and Modality 211 v vi Choice Based on Preference 214 Decision by Democratic Procedure 231 PHILOSOPHY OF SCIENCE Measurement: An Essay in Philosophy of Science 239 The Notion of a Phoneme 274 Published Writings of Stig Kanger 279 Index of Names 285 Subject Index 289 Photo:Rune Kanger Stig Kanger INTRODUCTION Stig Kanger (1924-1988) made important contributions to logic and formal philosophy. Characteristic ofKanger as a philosopher was his firm convic tion that philosophical problems can be clarified - and sometimes even solved - by means of exact logical and mathematical methods. His most substantial, and groundbreaking, contributions were in the areas ofgeneral proof theory, the semantics of modal and deontic logic, and the logical analysis of the concept of rights. But he contributed significantly to action theory, preference logic and the theory ofmeasurement as well.1 Kanger was Professor of Theoretical Philosophy at Uppsala University from 1968until his death in 1988. He was borninChina where helived with his parents, the Swedish missionaries Gustav and Sally Kanger, until he was thirteen. He received his higher education in Stockholm and obtained his Ph. D. from Stockholm University in 1957 under the supervision ofAnders Wedberg. Before being appointed to the Chair ofTheoretical Philosophy in Uppsala, Kanger was Docent at Stockholm University and Professor of Philosophy at Abo Academy inFinland. FordetaileddiscussionsandanalysesofvariousaspectsofKanger's work seethecritical essaysinVolumeIIofthepresentcollection.FortreatmentsofKanger'sworkingeneralproof theoryseeG.Sundholm, "TheProofTheoryofStigKanger:APersonalRecollection"andK. B.Hansen,"Kanger'sIdeasonNon-well-foundedSets:SomeRemarks".Hiscontributionsto theareaofeffectiveproofproceduresandautomatedreasoningarediscussedinD.Prawitz, "A Note on Kanger's Work on Efficient Proof Procedures" and in A. Degtyarev and A. Voronkov,"Kanger'sChoicesinAutomatedReasoning".JaakkoHintikka'spaper"TheProper TreatmentofQuantifiers inOrdinaryLogic" concerns Kanger's formalization of first-order logic as analgebraic logic calculus. Kanger's semantics for modal logic is discussed in S. Lindstrom, "AnExpositionandDevelopmentofKanger's EarlySemanticsfor Modal Logic" andhisapproach todeonticlogicinR.Hilpinen's "StigKangeronDeontic Logic".Kanger's theory of rights is dealt with in L. Lindahl, "Stig Kanger's Theory of Rights" and in L. Aqvist, "StigKanger'sTheoryofRights:BearersandCounterparties,Sources-of-law,andthe HanssonPetaluma Example".Kanger's contributions tothetheoryofactionaredescribed in G. Holmstrom-Hintikka, "Stig Kanger's Actions and Influence". Finally, Kanger's con tributions to the logic of preference are taken up by S. O. Hansson, "Kanger's Theory of Preference and Choice" andW. Rabinowicz, "Preference Logicand Radical Interpretation: Kanger MeetsDavidson". ix G.Holmstrom-Hintikka,S.Lindstromand R.Sliwinski Ieds.},Collected PapersofStig KangerwithEssays onhisLifeandWork,Vol.I. ix-xiv, © 2(0) AllRightsReserved.PrintedliyKluwerAcademicPublishers,theNetherlands. x INTRODUCTION Kanger's dissertation, Provability inLogic, 1957, was remarkably short, only 47 pages, but very rich in new ideas and results. By combining a Gentzen-style techniques from prooftheory witha model theory laTarski, Kanger gave a novel and elegant proofof Godel's completeness theorem for classical first-orderpredicate logic(withoutidentity).Fromthecompleteness proofhe could extract a simple semantical proofofGentzen's Hauptsatz as wellasaneffective proofprocedurefor predicate logic.The dissertation also contained thefirstfullydevelopedmodel-theoreticsemantics formodallogic. The basic idea of Kanger's completeness proof - an idea that was also developed around the same time in various versions by Beth, Hintikka and Schutte - is to view a proofofa logically valid formula as an unsuccessful attempt to find a counter-model to it. Kanger applied this idea directly to Gentzen's cut-free sequent calculus for classical predicate logic: given a sequent T - 11, the rules of the sequent calculus are appliedbackwards ina systematic search for a counter-model, i.e., a model in which all the for r mulas of are true and all the formulas of 11 are false. The backwards application of the rules yields a possibly infinite tree: all the formulas occurring in the sequents of the tree are subformulas of formulas in the r - original sequent. Ifthe sequent 11 is notprovable, the resulting tree has a maximal branch inwhich eachsequent ~I - ~2 satisfies thecondition ~I n ~2 = 0. Acounter-modeltothesequentI'- il canthen beconstructed from such a branch, essentially by assigning the value trueto an atomic sentence if itoccurs intheantecedent of a sequent inthe branch and the valuefalse if itoccurs inthe succedent. If, on the other hand, the sequent isprovable, the systematic search for a counter-model will be frustrated: each branch will terminate inan axiom of the form rl, A, r2 - ill' A, il2, and the resulting tree will be a proofin the Gentzen calculus of the initial sequent r il. => As an immediate corollary ofthe completeness theorem for the cut-free sequent calculus, Kanger obtained a simple model-theoretic (and non constructive) proof of Gentzen's Hauptsatz; i.e., the statement that any sequent that is provable inthe sequent calculus with the cut rule: r - r - r From il, A and A, il, infer -il is also provable in the calculus without the use of this rule. It is easily verified that thecut rule isasemantically valid rule. Hence, the system with thecut rule issemantically sound. Suppose nowthatr -il isprovable inthe system with the cut rule. Then the sequent is valid by the soundness ofthat r - system. It then follows by Kanger's completeness theorem that il is provable without the cut rule. INTRODUCTION xi As another byproduct of the completeness theorem, Kanger obtained a proofprocedure for classical logic that iseffective inthe sense ofproviding an algorithm for finding a proof of any given logically valid sequent (or formula): To construct a proof of a valid sequent r = fl, we start from below with the given sequent and construct a tree of sequents above it by meansofrepeated backwards applicationsoftherules ofthecut-free sequent calculus. We continue until theprocess terminates and we have reached an axiom atthe topofeach branch inthetree. The resulting tree isthena proof of the valid sequent that we started with. Kanger's completeness proof guarantees that theprocess terminates after finitelymany applications ofthe rules, provided, ofcourse,thatthesequent westarted withwasindeedvalid. Ifnot, the search for a proofmay go on indefinitely. Of course, Kanger's proofprocedure does not provide us with an effective method for deciding the validity ofany given formula offirst-order predicate logic. By the well known theorem due to Alonzo Church, we know that no such decision method exists. In the paper "A Simple Proof Procedure for Elementary Logic" Kanger describes how the proof procedure can be extended to predicate logic withidentityandhowitcan bemade more efficientfor actual implementation on a computer. The part ofKanger's dissertation that had the greatest impact, however, was the fifteen pages devoted to modal logic. There he gave the first development ofaviablemodel-theoreticsemantics formodallogic.Kanger's semantics has close affinities to the various versions of so-called possible worlds semantics developed by Jaakko Hintikka, Saul Kripke and Richard Montague. But there are also important differences between the various approaches. For one thing, Kanger's semantic ideas are closer in spirit to Tarski'sthantothemetaphysicallymoreloaded interpretations ofKripke and David Lewis. The idea of "metaphysically possible" possible worlds was certainly foreign to Kanger. Kanger's ambition wastoprovide alanguage L of quantified modal logic a withamodel-theoretic semantics laTarski. For thispurpose he introduced thenotionofasystem. Asystemisanorderedpair S = <Do,v>,where Do isa designated (non-empty) domainandv isa function which for every non empty domain D assigns an appropriate extension inD to every non-logical constant ofL InKanger's dissertation appears, forthe firsttimeinprint, asemanticsfor modal operators in terms ofwhat we nowadays call accessibility relations. Each modal operator 0 is associated with an accessibility relation Ro between systems in terms ofwhich the semantic evaluation clause for 0 is spelled out: