数理逻辑：第2版

　　Whatisamathematicalproof?Howcanproofsbejustified?Aretherelimitationstoprovability?Towhatextentcanmachinescarryoutmathematicalproofs?

　　Onlyinthiscenturyhastherebeensuccessinobtainingsubstantialandsatisfactoryanswers.Thepresentbookcontainsasystematicdiscussionoftheseresults.Theinvestigationsarecenteredaroundfirst-orderlogic.OurfirstgoalisGodelscompletenesstheorem，whichshowsthattheconsequencerelationcoincideswithformalprovability：Bymeansofacalculusconsistingofsimpleformalinferencerules，onecanobtainallconsequencesofagivenaxiomsystem(andinparticular，imitateallmathematicalproofs)

Preface
PARTA
ⅠIntroduction
1.AnExamplefromGroupTheory
2.AnExamplefromtheTheoryofEquivalenceRelations
3.APreliminaryAnalysis
4.Preview
ⅡSyntaxofFirst-OrderLanguages
1.Alphabets
2.TheAlphabetofaFirst-OrderLanguage
3.TermsandFormulasinFirst-OrderLanguages
4.InductionintheCalculusofTermsandintheCalculusofFormulas
5.FreeVariablesandSentences
ⅢSemanticsofFirst-OrderLanguages
1.StructuresandInterpretations
2.StandardizationofConnectives
3.TheSatisfactionRelation
4.TheConsequenceRelation
5.TwoLemmasontheSatisfactionRelation
6.Somesimpleformalizations
7.SomeremarksonFormalizability
8.Substitution
ⅣASequentCalculus
1．SequentRules
2．StructuralRulesandConnectiveRules
3．DerivableConnectiveRules
4．QuantifierandEqualityRules
5．FurtherDerivableRulesandSequents
6．SummaryandExample
7．Consistency
ⅤTheCompletenessTheorem
1．Henkin’STheorem．
2．SatisfiabilityofConsistentSetsofFormulas（theCountableCasel
3．SatisfiabilityofConsistentSetsofFormulas（theGeneralCase）
4．TheCompletenessTheorem
ⅥTheLSwenheim-SkolemandtheCompactnessTheorem
1．TheL6wenheim-SkolemTheorem．
2．TheCompactnessTheorem
3．ElementaryClasses
4．ElementarilyEquivalentStructures
ⅦTheScopeofFirst-OrderLogic
1．TheNotionofFormalProof
2．MathematicsWithintheFrameworkofFimt—OrderLogic
3．TheZermelo-FraenkelAxiomsforSetTheory．
4．SetTheoryasaBasisforMathematics
ⅧSyntacticInterpretationsandNormalForms
1．Term-ReducedFormulasandRelationalSymbolSets
2．SyntacticInterpretations
3．ExtensionsbyDefinitions
4．NormalForms
PARTB
ⅨExtensionsofFirst-orderlogic
ⅩLimitationsoftheFormalMethod
ⅪFreeModelsandLogicProgramming
ⅫAnAlgebraicCharacterizationofElementaryEquivalence
ⅩⅢLindstrom’sTheorems
References
SymbolIndex
SubjectIndex