Perspectives in Formal Induction, Revision and Evolution Wei Li Yuefei Sui R-Calculus, III: Post Three-Valued Logic Perspectives in Formal Induction, Revision and Evolution Editor-in-Chief WeiLi,Beijing,China SeriesEditors JieLuo,Beijing,China YuefeiSui,InstituteofComputingTechnology,ChineseAcademyofSciences, Beijing,China PerspectivesinFormalInduction,RevisionandEvolutionisabookseriesfocusing onthelogicsusedincomputerscienceandartificialintelligence,includingbutnot limited to formal induction, revision and evolution. It covers the fields of formal representation, deduction, and theories or meta-theories of induction, revision and evolution,wheretheinductionisofthefirstlevel,therevisionisofthesecondlevel, andtheevolutionisofthethirdlevel,sincetheinductionisattheformulastratum, therevisionisatthetheorystratum,andtheevolutionisatthelogicstratum. Inhisbook“TheLogicofScientificDiscovery”,KarlPopperarguesthatascien- tificdiscoveryconsistsofconjecture,theory,refutation,andrevision.Somescientific philosophersdonotbelievethatareasonableconjecturecancomefrominduction. Hence, induction, revision and evolution have become a new territory for formal exploration. Focusing on this challenge, the perspective of this book series differs fromthatoftraditionallogics,whichconcernsconceptsanddeduction. The series welcomes proposals for textbooks, research monographs, and edited volumes,andwillbeusefulforallresearchers,graduatestudents,andprofessionals interestedinthefield. · Wei Li Yuefei Sui R-Calculus, III: Post Three-Valued Logic WeiLi YuefeiSui BeihangUniversity InstituteofComputingTechnology Beijing,China ChineseAcademyofSciences Beijing,China ISSN 2731-3689 ISSN 2731-3697 (electronic) PerspectivesinFormalInduction,RevisionandEvolution ISBN 978-981-19-4269-3 ISBN 978-981-19-4270-9 (eBook) https://doi.org/10.1007/978-981-19-4270-9 JointlypublishedwithSciencePress TheprinteditionisnotforsaleinChina(Mainland).CustomersfromChina(Mainland)pleaseorderthe printbookfrom:SciencePress. ©SciencePress2022 Thisworkissubjecttocopyright.AllrightsaresolelyandexclusivelylicensedbythePublisher,whether thewholeorpartofthematerialisconcerned,specificallytherightsofreprinting,reuseofillustrations, recitation,broadcasting,reproductiononmicrofilmsorinanyotherphysicalway,andtransmissionor informationstorageandretrieval,electronicadaptation,computersoftware,orbysimilarordissimilar methodologynowknownorhereafterdeveloped. Theuseofgeneraldescriptivenames,registerednames,trademarks,servicemarks,etc.inthispublication doesnotimply,evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevant protectivelawsandregulationsandthereforefreeforgeneraluse. Thepublishers,theauthors,andtheeditorsaresafetoassumethattheadviceandinformationinthisbook arebelievedtobetrueandaccurateatthedateofpublication.Neitherthepublishersnortheauthorsor theeditorsgiveawarranty,expressedorimplied,withrespecttothematerialcontainedhereinorforany errorsoromissionsthatmayhavebeenmade.Thepublishersremainneutralwithregardtojurisdictional claimsinpublishedmapsandinstitutionalaffiliations. ThisSpringerimprintispublishedbytheregisteredcompanySpringerNatureSingaporePteLtd. The registered company address is: 152 Beach Road, #21-01/04 Gateway East, Singapore 189721, Singapore Preface to the Series Classicalmathematicallogics(propositionallogic,first-orderlogicandmodallogic) andappliedlogics(temporallogic,dynamiclogic,situationcalculus,etc.)concern deduction, a logical process from universal statements to particular statements. Descriptionlogicsconcernconceptswhichanddeductioncomposeofgenerallogics. Induction and belief revision are the topics of general logics and philosoph- icallogics,andevolutionisanewresearchareaincomputerscience.Toformalize induction,revisionandevolutionisagoalofthisseries. Revisionisomnipresentinsciences.Anewtheoryusuallyisarevisionofanold theory or several old theories. Copernicus’ heliocentric theory is a revision of the Tychonicsystem;thetheoryofrelativityisarevisionoftheclassicaltheoryofmove- ment;thequantumtheoryisarevisionofclassicalmechanics;etc.TheAGMpostu- lates is a set of conditions a reasonable revision operator should satisfy. Professor Li proposed a calculus for first-order logic, called R-calculus, which is sound and completewithrespecttomaximalconsistentsubsets.R-calculushasseveralvariants which can be used in other logics, such as nonmonotonic logics, can propose new problemsintheclassicallogics,andwillbeusedinbigdata. Popper proposed in his book The Logic of Scientific Discovery that a scien- tificdiscoveryconsistsoffouraspects:conjecture,theory,refutation,andrevision. Somescientificphilosophersrefutedthatareasonableconjectureshouldcomefrom induction. Hence, induction, revision and evolution becomes a new territory to be discoveredinaformalway. An induction process is from particular statements to universal statements. A typical example is the mathematical induction, which is a set of nontrivial axioms in Peano arithmetic which makes Peano arithmetic incomplete with respect to the standardmodelofPeanoarithmetic.Alogicforinductionisneededtoguidedata- mininginartificialintelligence.Data-miningisacanonicalinductionprocess,which minesrulesfromdata. In biology, Evolution is change in the heritable traits of biological populations oversuccessivegenerations.Insciences,Darwin’sevolutiontheoryisanevolutionof intuitivetheoriesofplantsandanimals.Inlogic,anevolutionisageneratingprocess ofcombiningtwologicsintoanewlogic,wherethenewlogicshouldhavethetraits v vi PrefacetotheSeries oftwologics.Hence,weshoulddefinethecorrespondingheritabletraitsoflogics, sets of logics, and sequences of logics. Simply speaking, predicate modal logic is an evolution of propositional modal logic and predicate logic, and there are many new problems in predicate modal logic to be solved, such as the constant domain semanticsandthevariantdomainsemantics,etc. The series should focus on formal representation, deduction, theories or meta- theoriesofinduction,revisionandevolution,wheretheinductionisofthefirstlevel, the revision is of the second level, and the evolution is of the third level, because theinductionisattheformulastratum,therevisionisatthetheorystratum,andthe evolutionisatthelogicstratum. Thebooksintheseriesdifferinlevel:someareoverviewsandsomehighlyspecial- ized.Here,thebooksofoverviewsareforundergraduatedstudents,andthehighly specializedonesareforgraduatedstudentsandresearchersincomputerscienceand mathematicallogic. Beijing,China LiWei October2016 LuoJie SongFangming SuiYuefei WangJu ZhuWujia Preface Post three-valued logic has sound and complete tableau proof systems, Gentzen deductionsystemsforsequentsandGentzen-typeddeductionsystemsformultise- quents,whichotherthree-valuedlogicsdonothave. ForPostthree-valuedlogictherearedeductionsystemsatdifferentlevels:atthe theory level, at the sequent level and at the multisequent level. At each level, the validityhascomplementaryvalidityanddualvalidity,andcorrespondinglythereare sound and complete deduction systems for validity, co-validity and dual validity, respectively. Correspondingly, there are R-calculi at the three levels. At each level, an R- calculushasacomplementaryR-calculusandadualR-calculus,whichareproved to be sound and complete. Therefore, we have the following table for all levels of deductionsystemsandR-calculi: Deduction Dualdeduction R-calculus DualR-calculus Theories T*[=] S*[(cid:2)=] R*[=] Q*[(cid:2)=] T ((cid:2)=) S (=) R ((cid:2)=) Q (=) * * * * Sequents G*[(cid:2)=V=] F*[=V(cid:2)=] E*[(cid:2)=V=] D*[=V(cid:2)=] G*(=V(cid:2)=) F*((cid:2)=V=) E*(=V(cid:2)=) D*((cid:2)=V=) Multisequents M= L(cid:2)= K= J(cid:2)= M(cid:2)= L= K(cid:2)= J= where ∗ ∈ {t,m,f}, [=] denotes the revision preserving validity and (=) denotes therevisionpreservingsatisfiability. vii viii Preface Other kinds of multisequents are considered. For uniform quantifiers, there are eightkindsofvaliditiesandR-calculi: M= , L(cid:2)= , K= , J(cid:2)= QQQ QQQ QQQ QQQ MQQQ, LQQQ, KQQQ, JQQQ (cid:2)= = (cid:2)= = Asquantifiersarenotuniform,therearemanykindsofvaliditiesandR-calculi: M= , L(cid:2)= , K= , J(cid:2)= Q1Q2Q3 Q1Q2Q3 Q1Q2Q3 Q1Q2Q3 M(cid:2)=Q1Q2Q3, L=Q1Q2Q3, K(cid:2)=Q1Q2Q3, J=Q1Q2Q3 ThesedeductionsystemsandR-calculiwillbeprovedtobesoundandcomplete. Beijing,China WeiLi October2021 YuefeiSui Contents 1 Introduction .................................................. 1 1.1 Three-ValuedLogics ...................................... 1 1.2 DeductionSystems ....................................... 2 1.3 R-Calculi ............................................... 4 1.4 More ................................................... 8 1.5 BasicDefinitions ......................................... 10 1.5.1 PostThree-ValuedLogic ........................... 10 1.5.2 PostThree-ValuedDescriptionLogic ................ 15 1.5.3 Remarks ......................................... 23 1.6 TypesofDeductionRules ................................. 25 1.7 Notations ............................................... 32 References .................................................... 33 2 Many-PlacedSequents ......................................... 35 2.1 Zach’sTheorem .......................................... 36 2.2 AnalysisofZach’sTheorem ............................... 40 2.3 TableauProofSystems .................................... 43 2.3.1 TableauProofSystemTt .......................... 43 2.3.2 TableauProofSystemTm .......................... 44 2.3.3 TableauProofSystemTf .......................... 45 2.4 IncompletenessofDeductionSystemT(cid:5)(cid:5) ..................... 46 References .................................................... 47 3 ModalizedThree-ValuedLogics ................................ 49 3.1 BochvarThree-ValuedLogic ............................... 49 3.1.1 BasicDefinitions ................................. 49 3.1.2 MultisequentDeductionSystemMb ................. 51 3.2 KleeneThree-ValuedLogic ................................ 54 3.2.1 BasicDefinitions ................................. 54 3.2.2 GentzenDeductionSystemGk ..................... 55 ix