《直觉模态逻辑的语义》由会员分享，可在线阅读，更多相关《直觉模态逻辑的语义（219页珍藏版）》请在金锄头文库上搜索。
1、TheProofTheoryandSemanticsofIntuitionisticModalLogicAlexK?SimpsonDoctorofPhilosophyUniversityofEdinburgh?AbstractPossibleworldsemanticsunderliesmanyoftheapplicationsofmodallogicincomputerscienceandphilosophy?Thestandardtheoryarisesfrominterpretingthesemanticde?nitionsintheordinarymeta?theoryofinform
2、alclassicalmathematics?If?however?thesamesemanticde?nitionsareinterpretedinanintuitionisticmeta?theorythentheinducedmodallogicsnolongersatisfycertainintuitionisticallyinvalidprinciples?Thisthesisinvestigatestheintuitionisticmodallogicsthatariseinthisway?Naturaldeductionsystemsforvariousintuitionisti
3、cmodallogicsarepresented?Fromonepointofview?thesesystemsareself?justifyinginthatapossibleworldinterpretationofthemodalitiescanbereado?directlyfromtheinferencerules?Atechnicaljusti?cationisgivenbythefaithfulnessoftranslationsintointuitionistic?rst?orderlogic?Itisalsoestablishedthat?inmanycases?thenat
4、uraldeductionsystemsinducewell?knownintuitionisticmodallogics?previouslygivenbyHilbert?styleaxiomatizations?Themainbene?tofthenaturaldeductionsystemsoveraxiomatizationsistheirsusceptibilitytoproof?theoretictechniques?Strongnormalization?andcon?uence?resultsareprovedforallofthesystems?Normalizationis
5、thenusedtoestablishthecompletenessofcut?freesequentcalculiforallofthesystems?anddecidabilityforsomeofthesystems?Lastly?techniquesdevelopedthroughoutthethesisareusedtoestablishthatthoseintuitionisticmodallogicsproveddecidablealsosatisfythe?nitemodelproperty?Forthelogicsconsidered?decidabilityandthe?n
6、itemodelpropertypresentedopenproblems?iAcknowledgementsIowemuchtomysupervisor?GordonPlotkin?Notonlyhashetaughtmeagreatdeal?buthehasbeenenormouslysupportivethroughoutmy?randomwalk?towardsathesis?Iamindebtedtomyformercolleagues?FaustoGiunchigliaandLucianoSer?a?ni?forprovokingmyinitialinterestinmodallo
7、gic?Theyhaveremainedrichsourcesofideasandintellectualstimulation?Theworkinthisthesishasbene?tedgreatlyfromdiscussionswithValeriadePaiva?DavidPymandColinStirling?Thepresentationofthethesishasbene?tedfromtheuseofPaulTaylor?sLatexdiagrampackage?TheLaboratoryfortheFoundationsofComputerSciencehasprovided
8、averystimulating?anddistracting?environmentforresearch?Ithasbeenmypleasuretodiscussmanysubjectswithmanypeople?ImentioninparticulartheBenAlderteam?JohnLongley?SaviMaharajandPeteSewell?Ialsothankmyo?cemates?PietroCenciarelli?ChristopheRa?alliandAndrewWilson?fortoleratingthemanymoodsofwritingup?Aboveal
9、l?Ithankmyfamilyandfriendsfortheirloveandsupportoverthelastthreeyears?Thisthesisisdedicatedtothememoryofmygrandfather?TomEdwardLewis?iiDeclarationThisthesiswascomposedbymyself?andtheworkreportedhereinismyown?iiiTableofContents?Introduction?Motivation?Synopsis?Intuitionisticlogic?Naturaldeductionfori
10、ntuitionisticlogic?Thenaturaldeductionsystem?Normalization?Thesemanticsofintuitionisticlogic?Geometrictheoriesinintuitionisticlogic?Intuitionisticmodallogic?Modallogic?Whatisintuitionisticmodallogic?Previousapproachestointuitionisticmodallogic?Ourapproachtointuitionisticmodallogic?Naturaldeductionfo
11、rintuitionisticmodallogics?Motivation?Thebasicmodalnaturaldeductionsystem?iv?Conditionsonthevisibilityrelation?Theconsequencerelation?Soundnessrelativetomodalmodels?Discussion?Meta?logicalcompleteness?Meta?logicalsoundness?Asemanticsforintuitionisticmodallogics?Completeness?Discussion?Axiomatization
12、s?CorrespondencewithIK?Axiomatizationsofothermodallogics?Problemswithamoregeneralscheme?Discussion?Normalizationanditsconsequences?StrongnormalizationforN?T?Acut?freesequentcalculus?Decidability?Thestructureofsequents?Apreorderonsequents?Irredundantderivationsanddecidability?Discussion?Birelationmodelsandthe?nitemodelproperty?InterpretingN?inbirelationmodels?Completeness?Soundness?ExtensiontoN?T?The?nitemodelproperty?Constructingaboundedmodel?Quotientingabirelationmodel?Applyingthequotientingtechnique?Discussion?Conclusionsandfurtherwork?Conclu
