Methodologies for Integrated Information Management Systems

TheoreticalInformationFoundationsforO\",t.MIr,jz_q0_-,,0u__ou_RepresentationandoP_ConstraintSpecificationf=,-.¢3=3ChristopherP.MenzelRichardJ.MayerKnowledgeBasedSystemsLaboratoryTexasA&MUniversityMarch5,1991<_--,o,__,,,,,)EC<_>-Zl--t--u_ZZ_0EC_r_0uJUJ_--_CooperativeAgreementNCC9-16_Z_.}COC__\"3ResearchActivityNo.IM.06:MethodologiesforIntegratedInformationManagementSystemsI7_(_.0NASAJohnsonSpaceCenterInformationSystemsDirectorateInformationTechnologyDivision¢.,r)s©©ResearchInstituteforComputingandInformationSystemsLakeUniversityofHouston-Clear_=.._TECHNICAL\"%.:REPARTTheRICISConceptTheUniversityoTHouston-ClearLakeestabIlshedtheResearchInstituteforComputingandInformationSystems(RICIS)in1986toencouragetheNASAJohnsonSpaceCenter{JSC)andlocalindustrytoactivelysupportresearchinthecomputingandinformationsclences.Aspartofthisendeavor,UHCLproposedapartnershipwithJSCtoJointlyde[meandmanageanIntegratedprogramofresearchInadvanceddataprocessingtechnologyneededforJSC'smainmissions,includingadministrative,engineeringandscienceresponsi-billtles.JSCagreedandenteredintoacontinuingcooperativeagreementwlthUHCLbeglnninginMay1986,toJointlyplanandexecutesuchresearchthroughRICIS.Additionally,underCooperativeAgreementNCC9-16,computingandeducationalfacilitiesaresharedbythetwoinsUtuUonstoconducttheresearch.TheUHCL/RICISmissionIstoconduct,coordinate,anddisseminateresearchandprofessionalleveleducationincomputingandInformationsystemstoservetheneedsofthegovernment,industry,communityandacademia.RICIScombinesresourcesofUHCLanditsgatewayaffiliatestoresearchanddevelopmaterials,prototypesandpublicationsontopicsofmutualinteresttoitssponsorsandresearchers.WithinUHCL,themissionIsbeingImplementedthroughinterdisciplinaryinvolvementoffacultyandstudentsfromeachofthefourschools:BusinessandPublicAdministration,Educa-Uon,HumanSciencesandHumanities,andNaturalandAppliedSciences.RICISalsocoUaborateswlthindustryinacompanionpro_.ThisprogramIsfocusedonservingtheresearchandadvanceddevelopmentneedsofindustry.Moreover,UHCLestablishedrelationshipswithotheruniversitiesandre-searchorganizations,havingcommonresearchinterests,toprovideaddi-tionalsourcesofexpertisetoconductneededresearch.Forexample,UHCLhasenteredintoaspecialpartnershipwithTexasA&MUniversitytohelpoverseeRICiSre_han-Ieducatlonprograms,whileotherresearchorganizationsareinvolv__athe\"gateway\"concept.AmajorroleofRICiSthenIstofindthebestmatchofsponsors,researchersandresearchobjectivestoadvanceknowledgeinthecomputingandinforma-Lionsciences.RICIS,worktngjoinflywithitssponsors,advisesonresearchneeds,recommendsprincipalsforconductingtheresearch,providestech-rdealandadmlnistraUvesupporttocoordinatetheresearchandintegratestechnicalresultsintothegoalsofUHCL,NASA/JSCandindustry.ilJJmijiJ=m_mimmll:.rwwww_mxwTheoreticalFoundationsforInformationRepresentationandConstraintSpecification/J_i\"J_mmmmmUgITI-mmmRiIIIwJmE_ImIImuBIL!imlRICISPrefacem.-mThisresearchwasconductedunderauspicesoftheResearchInstituteforComputingandInformationSystemsbyDr.ChristopherP.MenzelandDr.RichardJ.MayerofTexasA&MUniversity.Dr.PeterC.BishopservedasRICISresearchcoordinator.FundingwasprovidedbytheAirForceArmstrongLaboratory,LogisticsResearchDivision,Wright-PattersonAirForceBaseviatheInformationSystemsDirectorate,NASA/JSCthroughCooperativeAgreementNCC9-16betweentheNASASpaceCenterandtheUniversityofHouston-ClearLake.TheNASAtechnicalmonitorforthisresearchactivitywasRobertT.SavelyoftheInformationTechnologyNASA/JSC.Theviewsandconclusionscontainedinthisreportarethoseoftheauthorsandnotbeinterpretedasrepresentativeoftheofficialpolicies,eitherexpressorofRICIS,NASAortheUnitedStatesGovernment.JohnsonDivision,shouldimplied,mfmINL_IIItmmm_J.iE_WnIWm_fNm_mmmmWm_mH-ImIBr'HIirEalw_m.=r_Ef_WuTheoreticalFoundationsforInformationRepresentationandConstraintSpecificationChristopherMenzeiandRichardJ.MayerKnowledgeBasedSystemsLaboratoryTexasA&MUniversityMarch5,1991PrefaceThispaperdescribestheresearchaccomplishedattheKnowledgeBasedSystemsLaboratoryoftheDepartmentofIndustrialEngineeringatTexasA&MUniversity.Fundingforthelab'sresearchinIntegratedInformationSystemDevelopmentMethodsandToolshasbeenprovidedbytheAirForceHumanResourcesLaboratory,AFHRL/LRL,Wright-PattersonAirForceBase,Ohio45433,underthetechnicaldirectionofUSAFCaptainMichaelK.Painter,undersubcontractthroughtheNASARICISProgramattheUniversityofHouston.Theauthorsandthedesignteamwishtoacknowl-edgethetechnicalinsightsandideasprovidedbyCaptainPainterintheperformanceofthisresearchaswellashisassistanceinthepreparationofthisreport.WumzmmmgmqwJWIJnm_m|mimij,imi!ml_=n•I|ISummary5_.d_HvE_mAmethodcanbethoughtofasadistillationofgoodpracticeforaparticu-larsystemdevelopmentsituation.Formalizationofasuccessfulengineering,management,production,orsupporttechniqueintoamethodisdoneinhopesofraisingtheperformanceofthenovicepractitionertoalevelcom-pariblewiththatofanexpertthroughtheappropriateuseofthemethod.Individualmethodsarenormallyaccompaniedbyaspecialpurposegraphi-callanguagethatservestoprovidefocusmaddisplayemphasisforthemajorconceptsthatneeddiscovery,consensus,ordecisionrelativetoaspecificsys-temdevelopmentlifecycleactivity.Experiencehasproventhatthepersonalandorganizationalpreferencesforparticularmethodsarelikelytomakeitnecessarytoisolatetheinformationgatheredanddisplayedbyonemethodinsuchawaythatitcanbeusedinotherstagesofthelifecycleorbedisplayedinalternativeforms.ThispaperoutlinesthetheoreticalfoundationsnecessarytoconstructaNeutralInformationRepresentationScheme(NIRS)whichwillallowforau-tomateddatatransferandtranslationbetweenmodellanguages,proceduralprogramminglanguages,databaselanguages,transactionandprocesslan-guages,andknowledgerepresentationandreasoningcontrollanguagesforinformationsystemspecification.ContentsIntroduction51Motivation52First-orderLanguages62.1Vocabulary............................72.2Grammar.............................103First-orderSemantics133.1StructuresandInterpretations..................133.1.1InterpretationsofConstantsandFunctionSymbols..133.1.2InterpretationsofPredicates...............143.2Truth...............................153.2.1VariableAssignments...................153.2.2TruthUnderanAssignment...............163.2.3Truth...........................194Logic194.1PropositionalLogic........................194.1.1AxiomsforPropositionalConnectives..........204.1.2RulesofInference:ModusPonens............214.2PredicateLogic..........................224.2.1AxiomsfortheQuantifiers................224.2.2RulesofInference:Generalization............244.3Identity........254.3.1IdentityandExpressivePower..............254.3.2AxiomsforIdentity....................2fi5ConstraintLanguages285.1BasicSetTheory........................295.1.1Membership........................295.1.2BasicSetTheoreticAxioms...............30=....:,:•5.1.3FinitudeandtheSetofNaturalNumbers........345.1.4Difference,Intersection,andtheEmptySet......34WmmmmmBB.ImJm\"Um!mm-iJ,mmJmWIiiw5.1.55.1.6FunctionsTheandOrderedSemantics:n-tuplesThe.............CumulativeHierarchy35Intendedwtwz=tV,W,.r_LofSets5.2ConstraintsRevisited.......................5.3InformationStructures:AnIntuitiveAccount6SummaryAppendixA-AnOverviewofIDEF1AppendixB-FormalInformationStructures.........363738414356IntroductionThisdocumentpresentsthetheoreticalfoundationsforinformationrepre-sentationlanguagesofbothgraphicalandtextualvarieties.Itisintendedtoserveasaframeworkforprovidingrigoroussyntaxandsemanticsofex-istingandproposedinformationanalysis,design,andengineeringmethods.Thepurposeofsuchaframeworkistoprovideinformationrepresentationlanguagedesignerswiththe_idancenecessaryto_0Wforautomatedinter-modeldatatransferandtranslationlThus,thisdocumentshouldbeviewedasthestructureforaninformationmodeldataexchangespecification.Fi-nallythistheoryismotivated_g3_l{e-ne_d:for'ageneralthe0ryofinformationrepresentation.Thus,thistheoryservesasthefirststeptowardsachievementofaNeutralInformationRepresentationScheme(NIRS)foranIntegratedDevelopmentSupportEnvironment(IDSE)thatcanserveastheplatformforaseamlessComputerAidedSoftwardEngineering(CASE)environment.Sec-tion1ofthisdocumentdescribesthemotivationsandconsiderationsbehindtheproposedtheory.Section2introducesarestrictedfirst-orderlanguagesyntaxthatisproposedastheboundingsyntacticstructureforinforma-tionmodelinglanguages.Section3providesamodeltheoreticsemanticsforthoselanguages,andSection4acorrespondinglogic.Section5describestheapplicationoftheseconceptstoconstraintlanguages.1MotivationTheAirForceIntegratedInformationSystemsEvolutionEnvironment(IISEE)projectrepresentsacomprehensiveresearchefforttodeveloptech-nologiescriticaltoeffectivelymanage,control,andexploitinformationasaresource._Theresultingdevelopmentswillprovideintegrationsupportmethodologies,frameworks,andexperimentaltoolstosupportintegratedinformationmanagementsystemsdevelopmentandevolution.Oneofthekeypremisesonwhichthisprogramisbasedistherecogni-tionoftheneedforasuiteofinformationmodelingmethodstoservicethelargenumberoftasksanduser/developerrolesinanevolutionaryintegratedinformationsystemdevelopmentprocess.Eachmethodinthissuiteisde-mJag.!BW|w!mw/m.mmWWmm_zWmWrdmmt,tm¢wm_LvTwsignedtoserveaparticularclassofhumanusersperformingspecifictasksordecisionprocesses.Theindividualmethodsnormallyareaccompaniedbyaspecialpurposegraphicallanguagethatservestoprovidefocusanddisplayemphasisforthemajorconceptsthatneeddiscovery,consensus,ordecisionrelativetothattask.Theproblemwiththisapproachisthatthesesyntacticfeaturesrestricttheinformationthatcanbestatedinthelanguage.TheseamlessCASEconceptisfocusedondevelopmentofthetechnologi-ca]componentsandmanagementmethodsforseamlesssoftwareengineeringenvironments.Theterm\"seamless\"ismeanttoconveytheintegratednatureofthemethodsaridtoolsprovidedtothesoftwareimplementer.Theplural-izationoftheterm\"environments\"ismeanttoconveythefactthatdifferentseamlesscaseenvironmentswillbedefinedfordifferentsoftwaretypes.Thisparticulardocumentistheresultofresearchwhichbeganasanef-forttodefineaconstraintspecificationlanguageforaparticularinformationmodelingmethodknownasIDEF1.1Anoverviewofthemethodanditsfor-malizationarefoundinAppendicesAandB.Astheeffortprogressed,itwasrecognizedthattheemerginglanguagestructuresweresimilartothosebeinginvestigatedfortheconceptualschemarepresentationlanguagefortheIDSEseamlessCASEenvironmentandfortheNeutralInformationRepresentationSchemetobeusedtoprovidethebasisforanevolvingsystemdescriptioncapableofsupportingautomatedknowledgebasedmodeltranslation.Thetheorypresentedinthisreporthasbeenusedastheformalfoundationforafamilyoflanguagesthatwillservetheabovedescribedpurposes.ThisfamilyofInformationSystemconstraintlanguages(ISyCL)isdescribedin[1].2First-orderLanguagesThebasisofouraccountwillbethenotionofafirst-orderlanguage.First-orderlanguagesareflexible,expressivelyquiterich,andextremelywellun-derstood.Theyareusedextensivelyinmathematics,linguistics,philosophy,1See,e.g.,[2]and[3]._IDEF\"wasoriginallyanacronymfor\"ICAMDctlnitionLan-guage,\"butthesuiteofIDEFmethodshassinceevolvedindependentlyofitsICAMorigins.Hence,like\"NCR\"(formerlyanacronymfor\"NationalCashRegister\"),'IDEF\"isnowsimplyanamelike\"George,\"andanacronymnolonger.6/andcomputersciencewheneverclarityofexpressionisespeciallyimportant.Manyfamiliarmathematicaltheoriessuchasthetheoryofsets,booleanalge,bra,topology,etc.,canbedegantlyexpressedinfirst-orderterms.Morere-centlyfirst-orderlanguageshavefoundtheirwayintothedomainofartificialintelligence,wherefirst-orderlanguagesfindstraightforwardrepresentationinfamiliarAIprogramminglanguageslikeLISPandPROLOG.Indeed,first-ordermathematicallogicistheformalfoundationofPROLOG-anacronymforPROgramminginLOGic.z)Generallyspeaking,afirst-orderlanguage£isaformallanguage.Thatis,itisaformalstructureconsistingofafixedsetofbasicsymbols,oftencalledthevocabularyof£,andaprecisesetofsyntacticrules,itsgrammar,forbuildingupthepropersentences,orformulas,ofthelanguagethatarecapableofbearinginformation.2.1VocabularyThebasicvocabularyofafirst-orderlanguageconsistsofseveralkindsofsymbols:•Constants•Variables•Functionsymbols•Predicates•Logicalsymbols.Constantsaresymbolsthatcorrespondtonamesinordinarylanguage.Formanypurposes,itisusefultouseabbreviationsofnamesstraightoutofordinarylanguageforconstants,e.g.,jforJohn,wpforWright-Patterson,vforVenus,oforOhio,etc.Whenwearedescribinglanguagesingeneralandhavenospecificapplicationinmind,wewillsimplyusethelettersa,b,c,andd,perhapswithsubscripts;wewillassumethatwewilladdnomorethan2s¢¢,e.g.,[4].7II4DIim,miimtlim,JIII:mIW!mmvwt_finitelymanysubscriptedconstantstoourlanguage.3Constantsareusu-allylowercaseletters,withorwithoutsubscripts,butthisisnotnecessary.Indeed,itisoftenusefultouseuppercase.Wewilloftenwanttosaythingsaboutan\"arbitrary\"constantasawayoftalkingaboutallconstants,muchasonemighttalkaboutanarbitrarytriangleABCingeometryasawayofprovingsomethingaboutalltrianglesingeneral.Forthispurposeitwillnotdototalkspecificallyaboutagivenconstant,asay,sincewewantwhatwesaytoapplytoa/lconstantsgenerally.Thisrequiresthat,whenwearetalkingaboutourlanguage,weusespecialmetavariableswhoserolesaretoserveasplaceholdersforarbitraryconstantsofourlanguage,muchas\"ABC\"aboveservesasaplaceholderforarbitrarytriangles.Thus,metavariablesarenotthemselvespartofourfirst-orderlanguage£,butratherpartoftheextendedEnglishweareusingtotalkabouttheconstantsthatareinthelanguage.Wewillusethelowercasesansserifcharactersa,b,cforthispurpose.Nextarethevariables,whosepurposewillbedarifiedindetailbelow.Thelowercaselettersz,V,andz,possiblywithsubscripts,willplaythisrole,andwewillsupposetheretobeanunlimitedstoreofthem.Wewillusethecharactersx,yandzasmetavariablesoverthestoreofvariablesinourlanguage.Third,wehavefunctionsymbols.Thesesymbolscorrespondmostcloselyinnaturallanguagetoexpressionsoftheform\"TheXof,\"whereXisacommonnounphraselike\"color,\"\"yearlysalary,\"\"mother,\"etc.,orexpres-sionsoftheform\"TheY-estXin,\"whereYisanadjectivelike\"smart\"or\"mean,\"andXonceagainbyacommonnounphrase.Commonnounphrasestypicallyexpressgeneralproperties.ForanycommonnounphraseCNP,theresultofreplacingXwithCNPineitheroftheaboveforms(togetherwithanadjectiveforYinthesecondform)intuitivelynamesafunctionfthat,whenappliedtoagivenobjecta,yieldstheappropriateinstancef(a)ofthepropertyexpressedbytheCNPforthatobject.Thus,whereXis\"color,\"theresultingfunctioninthefirstformyieldsthecoloroftheobjecttowhichitisapplied;whereitis\"yearlysalary,\"theresultingfunctionyieldsanap-8Therestrictiontoafinitenumberofconstantshereisnotatallessential,butconstraintlanguagesingeneralwilluseonlyfinitelymany;thesameholdsforpredicatesandfunctionnamesbelow.propriatedollaramount.Similarly,\"Thesmartestwomanin\"expressesafunctionthattakesplaces--e.g.,cities,universities,etc.--andyieldsforeachsuchplacethesmartestwomantherein.Forthemostpartwewillconfineourattentionto\"one-place\"functionssuchasthoseabovethattakeasingleobjecttoanotherobject.Butaswewillseethereareoccasionswhenwewillwanttorepresentfunctionsofmorethanoneargumentaswell.Examplesofexpressionsthatstandfortwo-placefunctionsare\"Theonlychildof...and...\"and\"Thesumof...and....\"Intuitively,theformerexpressesapartialfunction4fromcoupleswithasinglechildtothatchild,andthelattersimplyexpressestheadditionfunction,whichtakestwogivennumberstoafurthernumber,viz.,theirsum.Aswithconstants,inpracticeitisoftenconvenienttoabbreviaterelevantordinarylanguagefunctionalexpressionsindefiningthefunctionsymbolsofaformallanguage.Again,wewillusethelettersf,g,andh,possiblywithsubscripts,forourbasicfunctionsymbols,andcorrespondingsansserifchar-actersasmetavariables.Functionsymbolsdesignedtostandforfunctionsofmorethanoneargumentwillbeindicatedwithanappropriatenumericalsuperscript.Asabove,wewillsupposethereareonlyfinitelymanyofthesesymbolsinourlanguage.Wealsointroducethesymbole,andstipulatethatwheregstandsforanyn-placefunctionsymbolinourlanguage,andfstandsforanyone-placefunctionsymbol,thenf•gisann-placefunctionsymbolaswell.Thiscorrespondsinordinarylanguagetothefactthatwecannestfunctionalexpressions,e.g.,\"Thesalaryofthefatherofthesmartestwomaninlargestuniversityin...,or\"Thesuccessorofthesumof...and....\"--7Thefourthgroupofsymbolsinourlanguageconsistsofr_-placepredi-cates,n>1.One-placepredicatescorrespondroughlytoverbphrasesllke\"isacomputerscientist,\"\"hasinsomnia,,\"\"isanemployee,\"andsoforth,allofwhichexpressproperties.Two-placepredicatescorrespondroughlytotransitiveverbslike\"loves,\"\"isanelementof,\"\"islessthan,\"\"begat,\"and41.e.,afunctionthat_mightnotbedefinedoneveryelementofitsdomain.E.g.,thesquarerootfunctionisonlyapartialfunctiononthenaturalnumbers,sinceitisnotdefinedonthosenumberswhicharenotsquaresofothernumbers.Thefunctioninthetexthereispartialbecauseitsintuitivedomainisthesetofpairsofhumans,andnoteverysuchpairhasasinglechild.9m=:msmim4lwi_mmtDl|wmImnmq_mWBiI;i|WIwm7mwiih¢wv\"liveswith,\"whichexpresstwo-placerelationsbetweenthings.Therearealsothree-placerelations,suchasthoseexpressedby\"gives\"and\"between,\"andwithalittleworkwecouldcomeupwithrelationsofmorethanthreeplaces,butinpracticeweshallhavelittlecausetogomuchbeyondthis.WewilluseuppercaseromanletterssuchasP,Q,andRforpredicates,andagaincorrespondingsansserifcharactersasmetavariablesoverpred-icates.Occasionallypredicateswillappearwithnumericalsuperscriptstoindicatethenumberofplacesoftherelationtheyrepresent,artdifnecessarywithsubscriptstodistinguishthosewiththesamesuperscripts.Itisoftenusefultoabbreviaterelevantnaturallanguageexpressions.Mostlanguagescontainadistinguishedpredicateforthetwo-placerelation\"isidenticaJto.\"Wewillusethesymbol_forthispurpose.Todrivehomethedifferenceatthispointbetweenpredicatesandfunc-tionsymbols,notethatafunctionsymbolcombineswithnamestoyieldyetanothername-like(i.e.,referring)expression:e.g.,todrawonordinarylan-guage,thefunctionsymbol\"thehusbandof\"combineswiththename\"Di\"toyieldthenewreferringexpression(ordefinitedescription,assuchareof_tencalled)\"thehusbandofDi.\"Ontheotherhand,a(one-place)predicatecombineswithanametoformasentence,somethingthatcanbetrueorfalse,notaname-likeexpression.Thus,thepredicateexpression\"ishappy\"combineswiththename\"Di\"toyieldthesentence\"Diishappy.\"Thesameiseasilyseentoholdforn-placepredicatesgenerally.Thelastgroupofsymbolsconsistsofthebasiclogicalsymbols:--,A,V,D,=,theexistentialquantifer3,andtheuniversalquantifierV,aboutwhichweshallhavemoretosayshortly.Wewillalsoneedparenthesesandperhapsothergroupingindicatorstopreventambiguity.2.2GrammarNowthatwehaveourbasicsymbols,weneedtoknowhowtocombinethemintogrammaticalunits,orwell-formedformulas,theformalcorrelatesofsen-tences.Thesewillbetheexpressionsthatcanencodethesortofinformationwewillwanttoexpressinourtheory(andmore).Thisisdonerecursively10Wasfollows,lwsFirst,wewanttogroupallname-likeobjectsintoasinglecategoryknownasterms.Thisgroupwillofcourseincludetheconstants,andforreasonsbelow,itwillincludethevariablesaswell.Butrecallthediscussionoffunctionsymbolsabove.Therewesawthatanexpressionlike\"Theyearlysalaryof\"seemstonameafunctiononobjects.Butthevaluesoffunctionsareobjectsaswell.Thus,whenweattachaname,\"Fred,\"say,tothefunctionalexpressionabove,theresult\"TheyearlysalaryofFred\"isasortofnameforFred\"syearlysalary.Thus,wecounttheresultofattachingafunctionalsymboltoanappropriatenumberofconstantsand/orvariablesasatermaswell;andsuchtermscanalsobeamongthetermsthatafunctionsymbolattachesto.Thus,moreexactly,lettingh,t2,..,standforarbitrarytermsandfstandforanarbitraryfunctionsymbol,iftl,...,t,,aretermsandfisann-placefunctionsymbol,thenf(tl,...,t,_)isatermaswell.Termsformedoutofcertainfamiliartwo-placefunctionsymbols,exam-plesofwhichwillbeintroducedbelow,aremorecommonlywrittenin_n-fixnotation,ratherthantheprefixnotationjustdefined,withthefunctionsymbolflankedbythetwoterms,ratherthanprecedingthem.Thus,foratwo-placefunctionsymbolfandtermst,t',thetermf(t,t')canalsobewrittenasfit'.So,forexample,+(2,3)canbewrittenas2+3.Nextwedefinethebasicformulasofourlanguage.Justasverbphrasesandtransitiveverbsinordinarylanguagecombinewithnamestoformsen-tences,soinourformallanguagepredicatescombinewithtermstoformformulas.Specifically,ifI0isanyn-placepredicate,andh,...,t,_areanynterms,thenPt_...t_isaformula,and_-nparticularanatomicformula.Toillustratethis,ifHabbreviatestheverbphrase\"ishappy,\"andathename\"Annie,\"thentheformulaHaexpressesthepropositionthatAnnieishappy.Again,ifLabbreviatestheverb\"loves,\"bthename\"Bob,\"cthename\"Charlie,\"andftheexpression\"thefianceof,\"thentheformulaLbf(c)expressesthepropositionthatBoblovesCharlie'sfiance.OftenwhenoneisusingmoreelaboratepredicatesdrawnfromnaturalSThatis,thedefinitionisgiveninsuchawaythatcomplexcasesoftheclassbeingdefinedaredefinedintermsofsimplercasesofthesameclass.Recursivedefinitionsthusoftenlookcircular,buttheyarenot,astheyalwaysbeginwithwell-groundedinitialcasesnotdefinedintermsofothermembersoftheclassbeingdefined.11iqpimEWmigmWmiiimiWii'lit:mBmWg:wvwm,mw•im==v=m--=7language,e.g.,ifwehadusedLOVESinsteadofLinthepreviousexample,itismorereadabletouseparenthesesaroundthetermsinatomicformulasthatusethepredicateandseparatethembycommas,e.g.,LOVES(b,ve)insteadofLOVESbx.Thus,moregenerally,anyatomicformulaPtl..._canbewrittenalsoasP(tl,...,t,,).Furthermore,atomicformulasinvolvingsomefamiliartwo-placepredicateslike_,andafewothersthatwillbeintroducedbelow,aremoreoftenwrittenusinginfixratherthanprefixnotation.Forexample,weusuallyexpressthataisidenticaltobbywritinga_bratherthan_ab.Thus,westipulatethatformulasoftheformPtt'canalsobewrittenastPt'.Nowwebeginintroducingthelogicalsymbolsthatallowustobuildupmorecomplexformulas.Intuitively,thesymbol-_expressesnegation;i.e.,itstandsforthephrase\"itisnotthecasethat.\"Sincewecannegateanydeclarativesentencebyattachingthisphrasetothefrontofit,wehavethecorrespondingruleinourformalgrammarthatif_isanyformula,thensois-_0.ThesymbolsA,V,D,and=standroughlyfor\"and,\"\"or,\"\"if...then,\"and\"ifandonlyif,\"whicharealso(amongotherthings)operatorsthatformnewsentencesoutofoldintheobviousways.Unlikenegation,though,eachtakestwosentencesandformsanewsentencefromthem.Thus,wehavethecorrespondingrulethatif_and_areanytwoformulasofourlanguage,thensoare(_oA_),(_0V_k),(_oD_k),and(_o=¢).Finally,weturntothequantifiers3andV.Recallthatweintroducedvariableswithoutexplanationabove.Intuitively,3andVstandfor\"some\"and\"every,\"respectively;thejobofthevariablesisto\"enablethemtoplaythisroleinourformallanguage.Considerthedifferencebetween\"Annieishappy,\"\"Someindividualishappy,\"and\"Everyindividualishappy.\"Inthefirstcase,aspecificindividualispickedoutbythename\"Annie\"andthepropertyofbeinghappyispredicatedofher.Inthesecond,allthatisstatedisthatsomeunspecifiedindividualorotherhasthisproperty.Andinthethird,itisstatedthateveryindivklual,whetherspecifiableornot,hasthisproperty.Thislackofspecificityinthelattertwocasescanbemadeexplicitbyrephrasingthemlikethis:forsome(resp.,every)individualz,zishappy.Sincetheruleforbuildingatomicformulascountedvariablesamongtheterms,wehavethemeansforrepresentingtheseparaphrases.LetHabbreviate\"ishappy\"onceagain;thenwecanrepresenttheparaphrases12as3zHzandVxHzrespectively.Accordingly,weaddthefinalruletoourgrammar:if_oisanyformulaofourlanguageandxisanyvariable,thenEx_oandVx_,areformulasaswell.Insuchacasewesaythatthevariablezisboundbythequantifier3(resp.,V),andwesaythattheformula_oisthescopeofthequantifer3in_0,anditisthescopeofthequantifierVinV×_0.8First-orderSemantics3.1StructuresandInterpretationsWehavemotivatedtheconstructionofourgrammarbyreferringtotheintendedmeaningsofthelogicalsymbolsand:bylettingourconstantsandvariablesabbreviatemeaningfulexpressionsoutofordinarylanguage.Butfromapurelyformalpointofview,allwehaveinalanguageisuninterpretedsyntax;wehavenotdescribedin-anyformalwayhowtoassignmeaningtotheelementsofafirst-orderlanguage.Wewilldosonow.Astructureforafirst-orderianguage_consistssimplyoftwoelements.\"asetDcalledthedomainof{hestructure,andafunction_\"knownasaninterpretationfunctionfor£.Intuitively,Disthesetofthingsoneisdescribingwiththeresourcesof£,e.g.,thenaturalnumbers,majorleaguebaseballteams,thepeopleandobjectsthatmakeupanairforcebase,ortherecordsinsideadatabase.Thepurposeof.7\"istofixthemeaningsofthebasicelementsof£intermsofobjectsinorconstructedfromD.3.1.1InterpretationsofConstantsandFunctionSymbolsTheinterpretationfunctionworksfi-kethislFirstwedealwithterms.Webeginbynotingthatvariableswillnotreceivean!nterpretation,sincetheirmeaningscanvary(theyarevariablesafterall)withinastructure.Theywillbetreatedwiththeirownspecialsemanticapparatusbelow.Constantsontheotherhan'fl,beingtheformalanaloguesofnameswithfixedmeanings,areassignedmembersofDonceandforallastheirinterpretation;insymbols,forallconstants_of£,Y-(s)•_P.13itmg=IItitwJII|imiIiwi1m'WiJvmItF11Wmgwvwr--J_Ew_Todealwithtermsformedfromfunctionsymbols,weneedfirsttoin-terpretthefunctionsymbolsthemselves.Tobeginwith,eachbasicfunctionsymbolaisassignedafunction._'(a)from79into79.Asindicatedabove,thefunctionsexpressedinordinarylanguageareoftenpartial;thatis,theyareoftennotdefinedeverywhere.Forexample,thefunctionexpressedby\"Thesalaryof\"isnotdefinedwhenappliedtoaconveyerbeltoragardenvegetable.Thissuggeststhatweoughttoletthefunctionsfrom79into79thatinterpretourfunctionsymbolsbepartial.Thisleadstocertaininel-eganciesinourformalapparatus,however,soweoptinsteadtoincludeadistinguishedobject_1_inourdomain79whosesolepurposeistobethevalueoffunctionsappliedtoobjectsonwhichtheyareintuitivelyundefined.Thus,ifwehaveafunctionsymbolfabbreviating\"Thesalaryof,\"andifourdomain79containsbothpersonsandconveyerbelts,thentheinterpretationoffwillbethefunctionthattakeseachpersontohisorhersalaryindollars,andeveryotherkindofobjecttoourdistinguishedobject/.Formally,then,forallbasicn-placefunctionsymbolsaof£,.TL-(a)E{4'Iq':7Y_-----'79};thatis,theinterpretationofabasicn-placefunctionsymbolaof£isgoingtobeandementofthesetofalln-placefunctionsfromthesetofn-tuplesofthedomain79into7).Nowweneedtoaddressthenonbasicfunctionsymbols,i.e.,thoseoftheforma•/9whichcorrespondtonestedfunctionalexpressionsinordinarylanguagelike\"Thesalaryofthefatherof.\"Intuitively,wewant.7\"(a•fl)tobethecompositionof.Tr(/_)with$-(a),i.e.,_(a)o$'(/3),whereingeneral(q,o$)(x)=q'($(x))S--intermsofourexample,thecompositionofthefunctionexpressedby\"Thesalaryof\"withthefunctionexpressedby\"thefatherof.\"Noticethatbyourtrickwith_1_,thecompositionofanytwofunctionswillalwaysbetotal.3.1.2InterpretationsofPredicatesFinally,foranyone-placepredicateP,welet.7\"(P)beasubsetof79--intuitively,thesetofthingsthathavethepropertyexpressedbyP.Andforanyn-placepredicateR,n>1,welet._\"(R)beasetofn-tuplesofde-SNotethatoisametalinguisticsymbolofourextendedEnglishthatexpressesthemeaningofourobjectlanguagesymbole,viz.,thecompositionfunction.14mentsofD--intuitively,thesetofn-tuplesofobjectsinDthatstandintherelationexpressedbyR.Thus,forexample,ifwewantLtoabbreviatetheverb\"loves,\"thenifourdomainDconsistsofthepopulationofTexas,thenY(L)willbethesetofallpairs(a,b)suchthatalovesb.Formally,then,foralln-placepredicatesP,._'(P)C_D'_JIfonewishestoincludetheidentitypredicateminone'slanguage,andhaveitcarryitsintendedmeaning,thenonen_dsan_additional,morespe-dficsemanticalruledesignedtociothis.Identity,ofcourse,isarelationthatholdsbetweenanyobjectanditself,butnotbetweenitselfandanyotherobject.Thisadditionalsemanticalconstraintiseasytoexpressformally:ifourlanguage£contains_,thentheinterpretationOf_isthesetofallpairs(o,o)suchthatoisanelementofthedomainD,i.e.,moreformally,={(o,o)Iocv}.3.2Truth3.2.1VariableAssignmentsGivenastructureM:/D,Y)for£_(cf.thedefinitionatthebeginningofSection3.1)wecandefinewhatitisforaformulaof£tobetrueinM.Asusual,thisisdonerecursively.Firstweneedtointroducethenotionofanassignmentaforthevariables,whichisasortofaddendumtoourinter-pretationfunction:itassignsmembersofthedomaintovariables.Relativetoanassignmentfunctiona,wecandefinetheinterpretationofacomplextermf(h,...,t,,),foranyfunctionsymbolfandanytermsh,...,t,,.Aninterpretationfunction_alonedoesnotsu_ceforthissincecomplexfunc-tionaltermsmightcontainvariables,e.g.,thetermf(z),whichareignoredbyinterpretationfunctions.Butifwesupplement_withanassigmentc_forthevariables,thenwehavesomethingforthefunction._'(f)toworkon.Specifically,theinterpretationofthetermf(x)undera,2\isjustthefunction._'(f)appliedtoa(z),thevalueassignedtozbya.---7_ere-bi\"=D._d--D-_;i-=----D_X9;i.e.,D'isjust9itself,9_isthesetofallpairsofmembers(i.e.,theCartesianproduct9xD)ofD,_Y_thesetofalltriplesofmembersofD,andingeneralD\"isthesetofall_tuplesofmembersofD.15I2_IDmImiHmmIIIIIpigW!umwmmimDIpl-JwmWwwww=E•Ingeneral,then,let.$'obetheresultofaddingzttof.sThentheinterpre-tation._',,(f(tl,...,t,_)ofacomplextermf(h,...,t,,)underaissimplytheresultofapplyingthefunction2\"=(f)(whichisjustY-(f),sincefisafunctionsymbol)totheobjects_',,(tl),...,._\"_.(t,_),i.e.,.7\"_.(f)(_,(t_),...,_,_(t,,)).3.2.2TruthUnderanAssignmentAtomicFormulasOurgoalinthissectionistodefinethenotionofaformulabeingtrueinastructureM.Todoso,wewillfirstdefineacloselyrelatednotion,viz.,thatoftruthunderartassignmentct.Forconvenience,wewillsometimesspeakofaformulabeing\"true,,inM\"insteadofbeing\"trueinMundera.\"Westartbydefiningthisnotionforatomicformulas.Solet_beanatomicformulaPtl...t,,.Then_0istrue,,inMjustincase/_',,(t,),...,Y-,,(t,_))¢Y'_(P).Intuitively,then,wheren=1,Ptistrue_inMjustincasetheobjectinDthattdenotesisinthesetofthingsthathavethepropertyexpressedbyP.Andforn>1,Pt_...t_istrue=justincasethen-tupleofobjects(o_,...,o,,)denotedbytl,...,t,_respectivelyisinthesetofn-tupleswhosemembersstandintherelationexpressedbyP,i.e.,justincasethoseobjectsstandinthatrelation.Letusactuallyconstructasmalllanguage£*andbuildasmallstructureM*toillustratetheseideas.Supposewehavefournamesa,b,c,d,asinglefunctionsymbolh(intuitively,toabbreviate\"thehusbandof\"),aone-placepredicateH(intuitively,toabbreviate\"ishappy\"),andathree-placepredicateT(intuitively,toabbreviate\"istalkingto...about\").Letusalsoincludethedistinguishedpredicate_,thoughwewillmakenorealuseofituntillater.Wewillusez,y,andzforourvariables.ForourstructureM*,wewilltakeourdomain_tobeasetofthreeindividuals,{Beth,Charlie,Di},andourinterpretationfunction_willbedefinedasfollows.Forourconstants,9(a)=_(b)=Beth,_(c)=Charlie,and_(d)=Di.(Beththushastwonamesinourlanguage;thisistoillustrateapointtobemadeseveralsectionshence.)Forourfunctionsymbolh,welet9(h)(Beth)=_(h)(Charlie)=3_(sothat_(h)is\"undefined\"onBethandCharlie),and_(h)(Di)=Charlie.ForourpredicatesHandT,Sl.e.,if_isaconstant,functionsymbol,orpredicate,_'_(_)=_(_),andif_isavariable,thenY'o(_)=a(_).16welet_(H)={Beth,Di}(so,intuitively,BethandDiarehappy),and_(T)={(Beth,Di,Charliel,/Charlie,Charlie,Di)}(so,intuitively,Bethistalkingto_aboutChariie,andCliarlieistaikingtohimselfaboutDi).Followingtherulefor_,welet_(_)={(Beth,Beth},(Charlie,Charlie),(Di,Di)}.Finally,forourassignmentfunction/3,letusletfl(z)=B(V)=Charlie,and3(z)=Di.LetusnowcheckthatHdandTbdh(z)aretrueinM*under/3.Inthefirstcase,bytheabove,Hdistrue_inM*justincase_7_(d)E_(H),i.e.,justincaseDiisandementoftheset{Beth,Di},whichsheis.SoHdistrueainM*.Similarly,Tbdh(z)istrue_inM*justincase(_a(b),_(d),(_(h(z)))ECa(T),i.e.,justincase(_(b),¢(d),G(h)(_(z)))E_(T),i.e.,justincase(Beth,Di,{7(h)(Di)E{(Beth,Di,Charlie),(Charlie,Charlie,Di)}i.e.,justincase(Beth,Di,Charlie)E{(Beth,Di,Chariie),(Charlie,Charlie,Di)}.Sincethisobviouslyholds,theformulaTbdh(z)istrueainM*.Aformulaisfalse`,inastructureM,ofcourse,justincaseitisnottrue,,inM.Itiseasytoverifythat,forexample,Hh(b),H_:,andTdbcareallfalse_inM*under/3.Conjunctions,_Negations,etc.Nowforthemorecomplexcases.Sup-posefirstthat_isaformulaOftheform-,¢'ThenWistrue`,inastructureMjustinCase=_//_iS_nottrue,_in=M.Insodefiningtruth=for_negatedformulasweensurethatthesymbol--,meanswhatwehaveintended.Thingsaremuchthesameforthe_0therSymbols.ThuslSuppose_is_aformuiaoftheform¢A0.Then_istrue`,inMjustin:case:both¢and0are.if_pisaformulaoftheform¢V8,then_istrue,,inMjustincaseeither¢orOis.If_isaformulaoftheform_bD8,then¢istrue=inMjustincaseeither¢isfalseinMor6istrue,,inM.Andif_isaformulaoftheform¢=8,then_istrue`,inMjust:{ncase¢andOhavethesametruth_iueinM.TKe_reader'_shouid_esthisOrhercomprehensiono_hes_eroles\"byverifying_that-Hh(b)and(Tbdh(z)ATccy)DHdarebothtrueinM*under3.QuantifiedFormulasLast,weturntoquantifiedformulas.Whenwein-troducedthequantifiersabove,wenotedthat\"Someindividualishappy,\"i.e.,3zHz,canbeparaphrasedas\"forsomevalueofthevariable'z,'theexpression'zishappy'istrue.\"Thisisessentiallywhatourformalseman-17WmtIiiIDBJlmmImzq_mmm!mmmm!-mWwmwl,ssmrJvv_sss-r.mticsforexistentiallyquantifiedformulaswillcometo.Toanticipatethingsabit,3xHzwillbetrueinastructureMunderc,,roughly,justincasetheunquantifiedformulaHxistrueinMundersome(ingeneral,new)assign-menta'suchthata'(x)isintheinterpretationofH.ItiseasytoverifythatthisformulaistrueinourlittlestructureM*underfl,whenwelookatanewassignmentfunction/3'thatassignseitherBethorDitothevariablez.Thus,3xHzshouldcomeouttrueinM*under/3.Butwehavetobealittlemorecareful,becausesomeformulas--Tcxz,forexample--containmorethanoneunquantifiedvariable.Thus,whenweareevaluatingaquantificationofsuchaformula--3zTczz,say--wehavetobesurethatthenewassignmentfunctiona'doesnotchangethevalueofanyoftheunquantifiedvariables--inthiscase,thevariablex.Otherwisewecouldchangethesenseoftheunquantifiedformulainmid-evaluation.Undertheassignmentfunction/3above,3zTczzintuitivelysaysthatCharlieistalkingtohimselfaboutsomeone(recallthat/3(x)=Charlie),andthisshouldturnouttobetrue_inM*sinceCharlieistalkingtohimselfaboutDi,i.e.,(Charlie,Charlie,Di)eCa(T).Butsupposeallwerequireisthattherebesomenewassignmentfunction_'suchthat/3'(z)isDi.Thenitcouldturnoutalsothat3'(_)isBeth.ButthentheformulaTcxzwouldnotbetrueinM*under/3,sinceCharlieisnottalkingtoBethaboutDi,i.e.,(Charlie,Beth,Di)¢Ca(T),andhencewewouldnotbeabletocount3zTc.zzastrueinM*under/3afterallasweshouldlike.Allthatisneededisasimpleandobviousrestriction:whenevaluatingtheformula3zTcxz,thenewassignmentfunctionthatweusetoevaluateTcoczmustnotbeallowedtodifferfrom/3onanyvariableexceptz(andeventhenitneedn'tdifferfrom/3;inwhichcaseit/s/3).Moregenerally,weputthematterlikethis:if_oisanexistentiallyquantifiedformula3x¢,then_0istrueinastructureMunderajustincasethereisanassignmentfunctiona'justlikeaexceptperhapsinwhatitassignstoxsuchthattheformula¢istrueinMundera'.If_0isauniversallyquantifiedformulaV×¢,then_oistrueinMunderajustincaseforeveryassignmentfunctiona'justlikeaexceptperhapsinwhatitassignsto×theformula¢istrueinMundera'.Thatis,inessence,_oistrueinMjustincase¢istrueinMnomatterwhatvalueinthedomainweassigntox(whilekeepingallothervariableassignmentsfixed).18Thereadercanonceagaintesthisorhercomprehensionbyshowingindetailthat3zTzbh(z)isfalseinM*under/_andthatVz(HzVTbdz)istrueinM*under/_.3.2.3TruthNow,finally,wecandefineaformulatobe_tteinastructureMsimplicilerjustincaseitistrue,,inMforallassignmentsa,andfalseinMjustincaseitisfalse,,inMforalla.Note,onthisdefinition,thatformostanyinterpretation,therewillbeformulasthatareneithertruenorfalseintheinterpretation.Ourexample3zTbzzabove,forinstance,isneithertruenorfalseinM*,sincethereareassignments_onwhichitcomesouttrue=--allthoseonwhichc_(x)=Di--andassignmentsaonwhichitcomesoutfalse=-allthoseonwhichct(z)#Di.Suchformulaswillalwayshavefreevariables,sinceitisthesemanticindeterminacyofsuchvariablesthatisresponsibleforthisfact.However,notethatsomeformulaswithfreevariableswillbetrueorfalseinsomemodels,thoughthesewilltypicallybelogicaltruths(orfalsehoods)likeHzA--,Hz,i.e.,formulaswhicharenotcapableoftrue(resp.,false)interpretation.4Logic4.1PropositionalLogicNowthatwehavethenotionofafirst-orderlanguageanditssemantics,wewanttocapturethemeaningsofthelogicalconstants--,,A,V,D,=,V,and3asexplicatedinthesemantics.Wewilldothisintheusualwaybydevelopingarigorousandpreciselogic.Alogic,inthesenserelevanthere,isasystematiccharacterizationofcorrectprinciplesofreasoningwithre-specttoagivendusterofconcepts.Theconceptsherearethoseexpressedbythelogicalconstantsabove,correspondingroughly,onceagain,totheordinarylanguageconceptsofnegation(not,oritisnotthecasethat),con-junction(and),disjunction(or),materialimplication(if...then),materialequivalence(ifandonlyif),existentialquantification(some),anduniversalquantification(every,ora/l).Theformsuchasystemtakesusuallyconsists19imwmmImVilipmezU'=nmqllmltmmI•m!litw_Jwrv=oftwocomponents:aziomsandrulesofinference.Westartwiththeaxiomsforthepropositionalconnectives.4.1.1AxiomsforPropositionalConnectivesTheaxiomsforthepropositionalconnectives-,,A,V,D,and=constitutethebasisofpropositionallogicandcanbethoughtofascharacterizingtheirmeanings.Therearemanyequivalentaxiomatizationsforpropositionallogic,butthefollowing,whichmakesuseofthenotionofanaxiomschema,isoneoftheeasiest.Anaxiomschemaisnotitselfanaxiom,butratherasortoftemplate,ageneralformanyinstanceofwhichisanaxiom.Axiomschemasarethusnotthemselvesactuallypartofthelanguage.Thus,where_,_b,and0areanyformulas,anyinstanceofanyofthefollowingschemasisanaxiom:A3v3InEnglish,A1saysessentiallythatifasentence_istrue,thenforanyothersentence_b,if_bistruethen_,isstilltrue.A2saysthatifasentence_pimpliesthatif_bistruethensois0,thenif_implies_b,thenitalsoimplies0.Finally,A3saysessentiallythatifasentence_impliesanothersentence_b,thenif,,bisalsoimpliedbythenegationof_,then_bistruenomatterwhat(sincetither_oritsnegationistruenomatterwhat).Theseaxiomsseemtrivial.However,likethedementarytruthsofarithmeticorgeometrythataresecondnaturetousnow,theymustbeexplicitlystatedasabasisforderivingother,lessobvioustruths;theycannotbeconjuredoutofthinair.Noticethataxiomschemasonlyusethetwoconnectives--,andD.Eventhoughwehavebeenusingtheotherpropositionalconnectivesallalong,of_ciallywewillconsiderthesetobeourtwo\"primitive\"connectives;theotherscanbedefinedintermsofthemasfollows(wherethesymbol=4,means\"isdefinedas\"):2OIBmlmDZil_ga!lII!lWIPqw!Wmlii!gjiD_IBlW=wwFFDef1:(_oV_)=4,(-_oD_)Def2:(_oA,_)=_/-_(-_oV-_)Def3:(_o-_)=d/(_oD_)A(_D_o)Thereadercanagaintestcomprehensionbyshowingthat,nomatterwhattruthvaluesareassignedto_,¢,and0,thetwosidesofeachdefinitionwillalwayshavethesametruthvalueswhenevaluatedinaccordwiththesemanticalrulesgivenabovefortheconnectivesinSection3.2.2.4.1.2RulesofInference:ModusPonensAlogicisnotmuchgoodwithoutrulesofinference,whicharerulesthatallowustomovefromstatementsthatweknoworassumetobetrueattheoutset(e.g.,ouraxioms),tonewstatementsthatfollowlogicallyfromthem(calledtheorems).Withoutthem,allwecoulddoiswritedownaxioms;therewouldbenowaytoinfernewtruthsfromthosealreadygiven.Thereisonlyoneruleofinferenceinpropositionallogic:ModusPonens(MP):Iftheformulas_and___followfromtheaxiomsofpropositionallogic,thenwemayinferthat_doesaswell.9Asasimpleexampleusingourlanguage£:*,considerthefollowingproofofHd2Hal,i.e.,thestatementIfDiishappy,thenDiishappy.Notethat,trivialasitis,HdDHdisnotaninstanceofanaxiomschema,andhenceifitistobeatheoremofoursystem,itmustbederivablefromtheaxiomsusingourruleofinferenceMP.Thisisinfactthecase.Asaninstanceofkl,wehaveHdD((HdDHd)DHd).AsaninstanceofA2wehave(HdD((HdDHd)DHd))D((HdD(HdDHd))D(HdDHd))._Giventhis,thenotionoftheoremhoodcanbedefinedpreciselyasfollows.Af_rmulaisatheoremofpropositionallogicifandonlyifthereisasequence_1,.--,_nsuchthat_,is_andeach_,iseither_maxiomorfollowsf_ompreviouslinesbyMP,thatis,therearepreviousformulas_,_k,3,k35ADRINKS_BEER(z).Letususethenotation{_[TEXAN(z)Aage_o]'(z)>35ADRINKSBEER(t)}tonamethisset,andingeneralthenotation{xI_}tonamethesetofthingsthatsatisfythedescription_.Now,intuitively,onewouldthinkthatanysuchdescription_withasingleunboundvariablepicksoutacorrespondingsetcomprisingthethingsthatfitthedescription.Forafterall,asetisjustacollectionofthings;soinparticu-larthecollectionsatisfyingacertaindescriptionisaset.Russellfoundthat,intuitionstothecontrary,thisisnotalwaysso.Considerthedescription\"setthatdoesnothaveitselfasamember,\"i.e.,s¢s.(Rememberthatsisasetvariable.)Intuitively,thereareallsortsofsetsthatsatisfythisdescription:thesetofhorsesisnotahorseandhenceisnotamemberofitself,thesetofsolarplanetsisnotaplanet,andsoon.Bytheintuitiveprincipleabove,thereisasetofallsetsthatsatisfiesthisdescription,i.e.,thereisthesetr={sIs_s}.Butnowaskyourself:isramemberofitselfornot?Ifitis,thensinceristhesetofallsetsthatarenotmembersofthemselves,itfollowsthatitisnotamemberofitselfafterall.Ifontheotherhanditisnotamemberofitself,thenitsatisfiestheconditionformembershipinr,i.e.,itactually/samemberofitself.Eitherwaywecontradictourselves.Sotherecannotbesuchasetasrafterall,despitewhatourintuitionstellus.TheAxiomsThelessonhereisthatnotjustanycollectionofthingsweisaset.Hencetheneedforaxiomsthatdonotgetusintothesamesortoftrouble.Forourpurposes,weneedsurprisinglyfew:fouraxiomsandoneaxiomschema.Thefirstaxiom,extensionality,tellsuswhentwoapparentsetsareinfactidentical,viz.,whentheyhaveexactlythesamemembers:sTIvrw(v ( er=•s)ri.e.,forallsetsrands,ifforanyobject_,zisamemberofrifandonlyifitisamemberofs,thenrandsarethesameset.Thesecondaxiom,pairing,isthatanytwoobjects(withinagivendo-31main)formaset:ST2v, vy3 ( where\"{x,y}\"isanameforthesetthatcontainsexactlytheobjectsdenotedbyzandy.(Byextensionality=therecanbeonlyOnesuchset.)Thus,tomakethisproper,weneedtoaddtoourvocabularytheleftandrightbraces{,},andtoourgrammartherulethatifh,...,t,,areanyterms,thentheexpression{tl,...,t,,}isatermaswell.TMThenextaxiomdeclaresthattheunionofanysetrexists,i.e.,thesetwhoseeiementsareexactlythemembersofthemembersof_r:ST3Vr3sVy(yEs=3t(tErAyCt)),inEnglish,foranysetrthereexistsasetssuchthatforanyobjecty,yisamemberofsifandonlyifthereisasettsuchthattisamemberofrandtheobjectyisamemberoft.Foragivensetr,wewillletUrstandfortheunionofr.(Uisthusadistinguishedtwo-placefunctionsymbol,denotingthe(partial)functionthattakesanysettoitsunion.)WewillusuallywriterusforU{r,Whenonesetaisasubsetofanotherb(i.e.,whenallthemembersofaaremembersofb)weexpressthiswithadistinguishedpredicateC_asaC_b.Thefourthaxiomsaysthatthesetofallsubsetsofanygivensetexists:ST4YrSsVx(xEs=zC_r),thatis,foranysetrthereisasetssuchthatforanyobjectz,zisamemberofsjustincasezisasubsetoft.IfaC_banda_b,wesaythataisapropersubsetofb,andweexpressthisasaCb.Foranygivenseta,thesetofallitssubsetsiscalledthepowersetofa.The(partial)functionthattakeseachsettoitspowersetwillbedenotedbythedistinguishedfunctionsymbolpow,andthusthepowersetofawillbedenotedbypow(a).14Strictlyspeaking,wecanthinkofourselvesasaddinginfinitelymanynewfunctionsymbolsfl,.f2,..,toourlanguage,whereeachf,,isann-placefunctionsymbol,eachofwhichcanbyconventionberewrittenusingthebracenotation.Therewrittenformofeachf,,isthusevidentbythefactthattherearentermsbetweenthebraces,e.g.,{a,b,c}istherewrittenformoffsabc.32imIrWJuiltimNJgW!D!mIJBwmIgi!!NiP!!i;rmareFinallywecometoouronesettheoreticaxiomschema,so-calledbecauseitactuallystandsforinfinitelymanyaxiomsofthesamegeneralform,oneforeachformulaofourlanguage.Itiscalledtheaxiomschemaofseparation,orsubsets.Theideaisquitesimple:givenacertainsetaandsomedescription_,inourlanguage,wecanseparateoutthesetofallthemembersofathatsatisfythedescription.Formally,foranyformula_,,STS_'¢r3s'CzEr(zEs--_(z)),where_(z)istheresultofreplacinganyunboundvariablein_withz.isRussell'sParadoxRevisitedGiventheseparationaxiomschemaweaxeabletoreintroduceinarestrictedformthenotationforsetsusedinthebriefdiscussionofRussell'sparadoxabove.Theparadoxariseswhenoneassumesonecangeneratesetsarbitrarilywithanygivenformula.Separationallowsonetousearbitraryformulasonlytoformsetsfromthemembersofpreviously9ivensets,andthiseliminatestheproblem;inthislight,inRussell'sargument,foranygivensetaalreadyprovedtoexist,oneisallowedtoassumeonlytheexistenceoftheset{sIsEaAs_s},andthiscausesnoproblemsatall.Thus,wecansafelyaddthefollowinggrammaticalrule:isif_isanyformula,tanyterm,andxanyvariable,then{x]xEtA_}isatermaswell.Similartowhatweallowedwithcertaintypesofquantifiedformulas,suchtermscanalsobewrittenas{×Et]_}.lSAssumingofcoursezdoesnotbecomeboundintheprocess;ifitdoes,wecanalwaysreplaceitintheaboveschemawithanewvariablenotoccurringin_.1SOtmorecautiously,itappearsthatwecandososafelyforallwecantell.DuetoG/kiel'sfamoussecondincompletenesstheo1\"em,thereisnowaytoprovethatthereatenototherhithertoundiscoveredparadoxeshrkinginthetheoryofsets;thatis,wecannotproveitsconsistency(atleast,notwithoutbeggingthequestionbyprovingitinatheorythatisatleastasdubious).Thegreatsuccessofthetheoryoverthepasteighty-fiveyears,however,andtheabsenceofanynewparadoxesdespiteextensiveuseandscrutinyofthetheory,hasgivenlogiciansgreatconfidencethatitisinfactconsistent,evenifweshallneverknowthiswithuttercertainty....._._:_._..._:--=335.1.3FinitudeandtheSetofNaturalNumbersAsnoted,weareassumingtheexistenceofthenaturalnumbers.Itwillproveveryusefulthentoassumeinadditionthattheyjointlyformaset;thisisnotprovablefromtheaboveaxioms.Theeasiestwaytodothisisjusttoaddanaxiomthatdeclaresthisexplicitly:NNSsW:(x•s=_NUM(z)),i.e.,thereexistsasetssuchthatforartyobject_:,zisanelementofsifandonlyifxisanaturalnumber.Bytheaxiomofextensionality,therecanbeonlyonesuchset.WewillcallitA/'.Wearenowabletodefineanotherusefulnotion.Asnoted,thestructureswewillexaminewillbefinite.Nonetheless,itwillstillbeimportanttobeabletosayexplicitlythattheyarefinite,andhenceweneedtobeabletoexpresstheconceptoffinitude.WecandothiswiththehelpofthesetA/'.Specifically,Def5:FINITE(s)=4t3n•A/(s--_{m•A/\"trn[EMPLOYEE\"]!!(SSN)SalarySexEMPLOYEE[42Figure2:CardfileinterpretationofanIDEF1entityclass.TheIDEF1languagedoesnotprovideameansofrepresentingtheindi-vidualentitiesonlygroupsofentitieswhichshareexactlythesametypesofattributes.ThesegroupsfromanIDEF1viewarecalledclasses.Ausefulmemoryaidforthisnotionistothinkoftheentityclassasalayoutforacardfile(SeeFigure??).Anentityclasshasanameandauniqueiden-tificationnumberassociatedwithit,alongwithaglossaryentryandalistofsynonyms.Anentityclassisrepresentedbyarectangularboxwiththelabeloftheentityclasslocatedinthelowerleftcorneroftheentityclasssurroundedbyasmallerrectangleandwiththeentityclassnumberlocatedinthelowerrightcornerofthelargerbox.Anentityclassisactuallydefinedbythesetofattributeclassesthatdefinethecharacteristicsofallthepossibleentitiesinallofitsextensions.Itisimportanttonotethatthesetofattributesismoreimportantthatthe47lEMP#SSN/ADDRESS(SSN)SalaryAddressfEMP_)IEMPL]42Figure3:Bucketanalogynotionconveyedbythelabelontheentityclassname!Inotherwords,onecanthinkoftheentityclassassimplyalabeledbucketwithnomeaningbeyondthatofthec_ollectionofattributeclassesitcontains(seeFigure77).Infact,itisconsideredgoodpracticetouseanentityclasslabelthatdoesnotnameaphysicalordataobjectinthedomainsincethatcouldconfuseanuninformedreader.ThelabelsoftheattributeclassesthatdefineanentityclassaresirnplylistedintheentityclassboxbelowthekeyclassdesignatorsandabovetTheentitycl_slabel...Theoccurrence0fthesameattributeclassinmultipleentityclassdefini-tionsdefinesarelationshipbetweenthoseentityclasses.Inordertoestablishtheexistencedependencybetweensuchentityclasses,oneentityclassmustbedeterminedtobetheownerofthesharedattributeclass.EveryattributeclassthatendsupbeingapartofanIDEF1modelhasexactlyoneowner48UWgUlmgWtIIUmUm!UEmimIIBB!'__B°IIIiIrh_w=Docsn'!b_Iong,_|_STUDENT#,345>hca:boc_u_'it_I_[•iI(S|D)(SID)][(sin)GPRGPRASSOCSTUDENTFigure4:ExampleoftheNo-Nullrule.entityclass.Whendecidingontheadditionofanattributeclasstoanentityclass,tworulesmustbefollowed.ThefirstisreferredtoastheNo-NullRule.Thisrulestatesthatnomemberofanentityclasscantakeanullvalueforitsattributethatcorrespondstotheaddedattributeclass(Figure??).Thesecondrule,theNo-Repeatrule,statesthatnomemberofanentityclasscantakemorethanonevalueatatimeforitsattributethatcorrespondstotheaddedattributeclass(Figure??).Eachentityclasshasassociatedwithitatleastonekeyclass.Akeyclassisjustaspecialsubsetoftheattributeclasseswhichdefinetheentityclass.Whatmakessuchkeyclasssubsetsspecialisthatitcanbedeterminedthatforanyinstance,thevaluesoftheattributesofthatinstance(whichcorrespondtotheattributeclassesinakeyclass),collectively,willuniquelyidentifythatinstanceoftheentityclassfromallotherinstances.InanIDEF149Whichonegoeshere?0),back(l_)=front(li+l).2°ThenCLmeetsthecondition2°Theideaisthatahappysequencerepresentsachainofconnectedlinktypessuchthatthebackofeachlinktype(savetheonebeginningthechain)isthefrontoftheprecedingoneinthechain.Nowinfact,theactualdefinitionhererepresentsthisideabackwards:theintuitivebeginningofsuchaconnectedchainisactuallyasdefinedthelastmemberintheformalrepresentation(11,...,l,_}.However,thisdefinitionmirrorsdirectlythecorrespondingIDEF1syntaxforsuchchains,andhenceinthelongrunmakesforasimplersemantics.57igCI:CL_C{s[sisahappysequenceofbasiclinktypes}.Giventhis,thefunctionsbackandfrontcanbeextendedsuchthat,Def6:ForcompositelinksL=(ll,.-.,In),•back(L)= ba k(t );•front(L)=d /ront(tl).Thedefinitionsofdomainandcodomaincanthenbebroadenedtoincludethesenewlydefinedextensionsintheobviouswayaswell.Henceforth,letL=BLLICL.Thecompositenatureofcompositelinktypescanbehighiightedbydefininganoperator@onLsuchthat,Def7:Forbasiclinksl,l',andcompositelinksL,L',•l@l'=al(l,l'),if(l,I')ECL;otherwisel@l'isundefined;•l@L=aj(l).--.L,if(1),--,LECL;otherwiseI@Lisundefined;21•L@l=d/L_.(1),ifL,-,(liECL;otherwiseL@li_undefined;•L@L'=d/L_,L',ifL_L'ECL;otherwiseL@L'isundefined.Informally,then,XQYsignifiesthecompositionofthelinktypeXwiththelinktypeY._....Intuitively,aninheritedattributeisthecompositionofalinktypewithanownedattribute.Thus,modelingcompositionintermsofsequencesasweare,wespecifythatthesetIAofinheritedattributesmeettheconditionC2:IAC_{X[forsomeaEOAeitherforsomelEBL,X=(a,l),orforsomeLGCL,X=(a},--L}.Thatis,amemberofIAmustbeeither,intilesimplestcase,apairconsistingofanownedattribute(i.e.,amember_of-OA)andabasiclinktype(i.e.,a21Wheres---s'isconcatenation,i.e.,theresultoftackingthesequences_ontotheendofthesequences.58iJJmgD__zIiB--Ii!=m||iiIm!j_mim|L_memberofBL),orelsetheresultoftackinganownedattributeontothebeginningofacompositelinktype.Wethenextendthedefinitionof_suchthat,Def8:ForaEOA,IEBL,LECL,•a@l=a!(a,I),if(a,I)EIA,andundefinedotherwise;•a@L=e¢(a).-.L,if(a).--LEIA,andundefinedotherwise.Giventhis,wehaveDef9:ForanyinheritedattributeA=aQL,•owned-attr(A)=d!a,•link(A)=#L.Wecanthenextendthedefinitionofthefunctionownertoafunctiong-owner(for\"generalizedowner\")onthesetofallattributesA=OAUIAsuchthat,DeflO:ForaEOA,g-owner(a)=dSowner(a);forAEIA,g-owner(A)=dSback(link(A)).Thatis,theg-ownerofagivenownedorinheritedattribute,viewedasafunction,isitsdomain.ThelastelementkcofF,isafunctionfromentityclassesetosetsofsubsetsofA-intuitively,thekeyclassesofe-thatmeetsthefollowingcondi-tions:C3:ForallEEE,kc(E)#0,thatis,thesetofkeyclassesforanygivenentityclassmustbenonempty,i.e.,everyentityclassmusthaveatleastonekeyclass.C4:ForallEEE,andforallK,K'Ekc(E),K_.K'.2222C,recall,signifiesthepropersubsetrelation.Notethatthisconditionrulesoutthepossibilityofanemptykeyclass,sincetheemptysetisasubsetofeveryset,includingitself.59C5:ForallEEE,andforallAEUkc(E),g-owner(A)=E,thatis,theattributesineverykeyclassofagivenentityclassEmustbeownedbyE,i.e.,haveEastheirdomain.Nowwedefinetheimportantnotionofawalkandrelatedconcepts.Thesewillbeusedmostdirectlytodefineinformationstructures.Def11:LetE=(E_,...,E,,)beasequenceofentityclasses,letA=(ll,...,l,_-1)beasequenceofbasiclinktypes,andletW=(E,A/.Then•Wisawalk(fromE1toEn)iffforalli

因篇幅问题不能全部显示，请点此查看更多更全内容

查看全文