Helmut Schwichtenberg - 2004 - Mathematical Logic

《Helmut Schwichtenberg - 2004 - Mathematical Logic》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、MathematicalLogicHelmutSchwichtenbergMathematischesInstitutderUniversit¨atM¨unchenWintersemester2003/2004ContentsChapter1.Logic11.FormalLanguages22.NaturalDeduction43.Normalization114.NormalizationincludingPermutativeConversions205.Notes31Chapter2.Models331.StructuresforCla

2、ssicalLogic332.Beth-StructuresforMinimalLogic353.CompletenessofMinimalandIntuitionisticLogic394.CompletenessofClassicalLogic425.UncountableLanguages446.BasicsofModelTheory487.Notes54Chapter3.Computability551.RegisterMachines552.ElementaryFunctions583.TheNormalFormTheorem644

3、.RecursiveDefinitions69Chapter4.G¨odel’sTheorems731.G¨odelNumbers732.UndefinabilityoftheNotionofTruth773.TheNotionofTruthinFormalTheories794.UndecidabilityandIncompleteness815.Representability836.UnprovabilityofConsistency877.Notes90Chapter5.SetTheory911.CumulativeTypeStructu

4、res912.AxiomaticSetTheory923.Recursion,Induction,Ordinals964.Cardinals1165.TheAxiomofChoice1206.OrdinalArithmetic1267.NormalFunctions1338.Notes138Chapter6.ProofTheory139iiiCONTENTS1.OrdinalsBelowε01392.ProvabilityofInitialCasesofTI1413.NormalizationwiththeOmegaRule1454.Unpr

5、ovableInitialCasesofTransfiniteInduction149Bibliography157Index159CHAPTER1LogicThemainsubjectofMathematicalLogicismathematicalproof.Inthisintroductorychapterwedealwiththebasicsofformalizingsuchproofs.ThesystemwepickfortherepresentationofproofsisGentzen’snaturaldeduc-tion,fro

6、m[8].Ourreasonsforthischoicearetwofold.First,asthenamesaysthisisanaturalnotionofformalproof,whichmeansthatthewayproofsarerepresentedcorrespondsverymuchtothewayacarefulmathematicianwritingoutalldetailsofanargumentwouldgoanyway.Second,formalproofsinnaturaldeductionarecloselyr

7、elated(viatheso-calledCurry-Howardcorrespondence)totermsintypedlambdacalculus.Thisprovidesusnotonlywithacompactnotationforlogicalderivations(whichother-wisetendtobecomesomewhatunmanagabletree-likestructures),butalsoopensuparoutetoapplyingthecomputationaltechniqueswhichunder

8、pinlambdacalculus.Apartfromclassicallogicwewillalsodealwithmoreconstructivelogics: