Logic Proofs- Through Ideal Inclusions

LogicProofs-ThroughIdealInclusionsR.GermundssonDepartmentofElectricalEngineeringLinkopingUniversityS-58183LinkopingSWEDENEmail:[e-mail]1991-09-07Abstract:Thetwoapproachesofpropositionallogic(semanticandprooftheoretic)arefoundtohaveequivelentformulationsincommutativealgebraoverniteelds.Inparticularthesemanticapproachcorrespondtoanalgebrogeometricformulationandtheprooftheoreticcorrespondtoanidealtheoreticframework.Basedonthiscorrespondenceanewcompletenessproofisgiven.AnimplementationofthisproofsysteminMathematicaisalsogiven.Keywords:Sematics,ProofTheory,Ideal,AlgebraicGeometry,Variety,GrobnerBases1IntroductionThissectionpresentsthemajorresultsandthedispositionofthereport.Thebasicideaofthisreportisthatyoucanusealgebraicmethodstodo(propositional)logicproofs.Morespecicallylogicpropositionsmaybemappedtopolynomialsinsuchawaythattruthvaluesarepreserved.Byusingthisrepresentationonecansimulatelogicproofsineitheroftwomodes:Semantic:Thesemanticapproachtologicproofsbasicallyexaminestruthval-uesandreasonsfromthatstandpoint.Thisapproachiscloselyrelatedtoalgebraicgeometryandtheexactrelationisgivenintheorem4.2ProofTheoretic:Theprooftheoreticapproachessentiallymeansusingproofrulesoftheform!andthenwecanconclude.Eventhoughit1isfarlessobvious,thisapproachiscloselyrelatedtodeterminingwetherornotanidealisincludedinanotherideal.Seetheorem5.1fortheexactrelationship.Theidealinclusiondecisionisthenreallydeterminedthroughpolynomialremaindercalculation,seesection7forexactresultsandexamples.Byusingtheequivalencestatedaboveandapurelyalgebraicresult,namelytheorem2.2,wecanprovethatthetwomodesarereallyequivalent,commonlyknownascompletenesswithinlogic.Pictoriallythisreportmaybepresentedasthefollowingresult:SemanticProofTheoreticmmAlgebraicGeometry,IdealTheoreticInthenotationsoflogicandcommutativealgebra(denedlater)theexactresultis:Let=f1;:::;ngbeasetofpropositionsandletbesinglepropositioninallcasesusingpropositionsymbolsx1;:::;xn.Letgi=P(i)andf=P()wherePmapspropositionstopolynomialsinsuchawaythattruthvaluesarepreserved,seedenition4.2,then:j=‘mmV(g1:::gm)V(f),(g1gm)(f)Thedispositionofthereportisasfollows:AlgebraicResultscontainsthealgebraicresultsneededinthesubsequentsections,suchasnotationandtheconnectionbetweenidealsandvarieties.LogicConceptsintroducesthemostfundamentallogicalconcepts,e.g.for-mulasandinductionoverformulas.Semanticsmakesthepreciseconnectionbetweenalgebraicgeometryandlog-icalsemantics.ProofTheorymakesthecorrespondingconnectionbetweenprooftheory(oflogic)andidealtheory.Completenesstiestogetherthealgebraicgeometryandidealtheoryandbe-causeoftheprevioussectionsthismeansthatsemanticsandprooftheoryareconnected.ImplementationcontainsanexampleimplementationinMathematicaofboththegeometricandidealtheoreticapproaches.Italsocontainsexamples.FutureWorkdescribessomepathstofollowafterthistheseresults.AppendixcontainsfullMathematicacodeusedforthispaper.22AlgebraicResultsInthissectionwewillintroducethealgebraicresultsneededinsubsequentsections.Basicallywewillintroducetheconceptsofpolynomialring,idealandvariety.Moreextensivestudiesofthesemaybefoundin[6,8,1,9,12,14,10].Themainresultsofthissection{anextensiontoHilbert’sNullstellenSatztoalgebraicallynonclosedeldsofnitecharacteristic{hassofarnotbeenfoundinanyofthereferences.Themainobjectsthatweworkwith-inactualcomputations-arepoly-nomialsinseveralvariables.Supposeweworkwithpolynomialsinvariablesx1;:::;xn,thenamonomialissomethingoftheform:x11xnn=x;=[1;:::;n]2NnUsingthemultiindexnotationabovewecaneasilywriteamultivariablepoly-nomialpas:p=X2Nncxwhereonlynitelymanycarenonzero.Wehavenotyetspeciedwhereourcoecientslie,butinthisarticletheywillalwayscomefromaeldK(i.e.wecansum,multiplyanddivide).ThesetofallsuchpolynomialsisdenotedbyK[x1;:::;xn],i.e.K[x1;:::;xn]=fX2Nncx:c2Knitelymanyc6=0gDenition2.1Letp1;:::;pl2K[x1;:::;xn].IdealTheidealageneratedbyp1;:::;plisa=fX1ilfipi:fi2K[x1;:::;xn]gVarietyThevarietyAofp1;:::;plistheset:A=fu2Kn:pi(u)=0;i=1;:::;lg2DenotethesetofallidealsinK[x1;:::;xn]byIdeals(K[x1;:::;xn]).Theidealgeneratedbyp1;:::;plisusuallydenotedby(fp1;:::;plg)or(p1;:::;pl).Thevarietyassociatedwithp1;:::;plisthesameasthevarietyassociatedwith(p1;:::;pn).ThisvarietyisusuallydenotedbyV((p1;:::;pn)),i.e.V:Ideals(K[x1;:::;xn])!Pow(Kn)3wherePow(Kn)isthesetofsubsetsofKn.SymmetricallywecanconsiderI:Pow(Kn)!Ideals(K[x1;:::;xn])denedby:I(A)=fp2K[x1;:::;xn]:p(u)=08u2AganditisreadilyveriedthatI(A)isanideal.Thefollowingaremoreorlessdirectconsequencesofthesedenitions:Theorem2.1Leta1;a22Ideals(K[x1;:::;xn])thenV((0))=Kn(1)V((1))=;(2)V(a1\a2)=V(a1)[V(a2)(3)V(a1+a2)=V(a1)\V(a2)(4)a1a2)V(a1)V(a2)(5)LetA1;A22Pow(Kn)thenI(Kn)=(0)(6)I(;)=K[x1;:::;xn](7)A1A2)I(A1)I(A2)(8)Andcombiningthesewehave:(a2Ideals(K[x1;:::;xn]),A2Pow(Kn))I(V(a))a(9)V(I(A))A(10)I(V(I(A)))=I(A)(11)V(I(V(a)))=V(a)(12)2Theseresultsmaybefoundin[12].Itisworthnotingthat(1)=K[x1;:::;xn]InthisarticlewewillutilizeK=Z2,i.e.theintegersmodulo2.Theorem2.2(MainTheorem)Letpbeprimethen8A2Pow(Znp)V(