Basic Proof Theory

Thisintroductiontothebasicideasofstructuralprooftheorycontainsathoroughdiscussionandcomparisonofvarioustypesofformalizationoffirst-orderlogic.Examplesaregivenofseveralareasofapplication,namely:themetamathematicsofpurefirst-orderlogic(intuitionisticaswellasclassical);thetheoryoflogicprogramming;categorytheory;modallogic;linearlogic;first-orderarithmeticandsecond-orderlogic.Ineachcasetheaimistoillustratethemethodsinrelativelysimplesituationsandthenapplythemelsewhereinmuchmorecomplexsettings.Therearenumerousexercisesthroughoutthetext.Ingeneral,theonlyprerequisiteisastandardcourseinfirst-orderlogic,makingthebookidealforgraduatestudentsandbeginningresearchersinmathematicallogic,theoreticalcomputerscienceandartificialintelligence.Forthenewedition,manysectionshavebeenrewrittentoimproveclarity,newsectionshavebeenaddedoncutelimination,andsolutionstoselectedexerciseshavebeenincluded.