; TeX output 1996.01.16:1211m܍3$(܍'Z(9DtGGcmr17Elemenqtary7tLogicReviewo cmr9(basedTonG&Nnotation)`LogicT&Arti cialIn9telligence,Spring'95lύ+XQ cmr12SelmerBringsjordύ/ Janruary16,1996.A67"Vff cmbx101NFirst-OrderLanguagesq6"K`y 3 cmr10Ab rst-orderlanguage,recall,isformedinthestandard\t!wophase"manner 6('"V 3 cmbx10terms rst,fthenatomiclformtulas,thenform!ulas|orw s|ingeneral)6fromFl$!", 3 cmsy10Q`vdDariablesFlQ`objectfconstan!ts(orconstants)FlQ`functionfconstan!ts(orfunctors)FlQ`relationfconstan!ts(orrelationsymbMols)FlQ`theftruth-functionalconnectiv!esFlQ`theft!woquanti ersFlQ`punctuationfsym!bMolsGFeorQvexample,|9giv!ensomepredictableconstitutentsfromthislist,|9\The 6only.baseballpla!yer.into!wnismarriedtooneofJeremy'sdaughters"(which6w!e}'sawearlierinTearski'sWorld2cmmi8T.:M)couldbMe(withpunctuationstreamlined)Q`9# b> 3 cmmi10x[Bxn^8yd(Byo:) x=yd)n^B9z{I(M1xz5^DMzjb^9zz |{Ycmr81(DMzz1j^nz6= zz1))^>8vd(M1xvo:) v=z{I)]C31*m܍3$(܍3$62NFormalSeman=tics񍍑60N cmbx122.1TInterpretations6Aneintterpretationisamappingfromelemenen!tsofthelanguagetoele- 6men!ts^ofaconceptualization.مWeerepresentthemappingbythefunction6I(d),whereV9isanelemen!tofthelanguage.jThedomainorunivtersehof6discourseYisdenotedb!yjIj.Aninterpretationmustsatisfythefollowing6threefconditions:Cb%1.Q`iff isaconstan!t,thendI>2 jIj;Cb%2.Q`iff isann-aryfunctor,thendI>: jIjnd !jIj;Cb%3.Q`iffisann-aryrelationsym!bMol,thenI jIjnP.R62.2TVariableandTermAssignment6LetnUmapvdDariablestojIj.7sThenaterm(assignmenttTIU|isafunction 6fromftermstotheuniv!erseofdiscoursede nedbyCb%1.Q`iffisaconstan!t,thenTIU i(=O) =I();Cb%2.Q`iffisavdDariable,thenTIU i(=O) =U1();Cb%3.Q`ifVisatermoftheformd(z1;1:::l;1znP)andI() =fKandVTIU i(zid)=xzi,Q`thenfTIU i(=O) =f-(xz1;1:::l;1xznP).R62.3TSatisfaction,g cmmi12:::6Thek!eyideahereisthatofagivenformulabMeingtrue+onsomeintter-6pretationI.}(Weealsosa!ythataninterpretationIsatis esaformula.)6Thisiswrittenasj,=I[U1].Theten-clausede nitionisgiv!enonpage25of6G&N.fTheonlyin!terestingclausesarethe naltwo,viz.,FlQ`j,=I(8r)[U1]i foralld 2jIjit'sthecasethatj=I[Vn]whereV(r) =dQ`andfVn() =U1()for6=r;FlQ`j,=I $(9r)[U1] i forsomedT2jIj it'sthecasethatj=I $[Vn]whereQ`Vn(r) =dfandV() =U1()ffor 6=r.C32m܍3$(܍3$GSomeimpMortan!t,,arelatedconcepts:derivdDationasoneofasortdonehereatRensselaerinthecourse%': 3 cmti10Lpogicand6A\rpgument)w!esaythatisprovdDablefrom,) writtenas`.Thesetof6naturaldeductionrulesused,"forexample,inThe LpogicBookconstitute(if6augmen!tedmnwithsomealgorithmforenumeratingtheproMofs)asoundand6completer[inferenceproMcedure.AThatis,XwherePXisthisprocedure,Xand6is#asetof rst-orderw s,C`ifsomeislogicallyimpliedb!y,thenP wwill6ev!entually ndacorrespMondingproof(completeness),andif=`,then6 j,=.64NDecidabilit=y5 b>ff cmmi10:fd::q6A1iset1isdecidable,recall,i ,for1abac!kgroundalphabMetA,thereis6somealgorithm(orTeuringMac!hine,orcomputerprogram,etc.)whic!hcan6tellwhetherornotu#2,9)forev!eryu#2AK cmsy8.~Feora xedsetofw s,6theWproblemofdecidingwhetheraform!ulaislogicallyimpliedbyis6undecidable.First-order^logicisundecidable,minthesensethatthesetofall6vdDalidfform!ulas(givensome xed rst-orderlanguage)isundecidable.GA"theory"TGis nitelyaxiomatizablei thereisa niteTsuc!h6thatfev!erymembMerofTnislogicallyimpliedby.C33*;m9DtGGcmr177"Vff cmbx105 b>ff cmmi100N cmbx12,g cmmi12+XQ cmr12'"V 3 cmbx10%': 3 cmti10$!", 3 cmsy10# b> 3 cmmi10"K`y 3 cmr10o cmr9K cmsy82cmmi8 |{Ycmr8