÷ƒ’À; è TeX output 1999.04.28:1456‹ ÿÿÿÿ ¿™¬ ýLfT‘ …rïhtml:ï html:ŽŽ •™¬ ýºL¾’ µk^óDÓít G® G® cmr17ºBorderlinesŽŸlÏ’ ¦ÛóX«Q cmr12»Gio¬rv‘ÿXäanna‘ê¨CepparelloŽŽŽŽŽ©ŒÏ’ ¼šH1–ê¨April“1999ŽŸ(lÏ’ Æl/óò"V
cmbx10ÇAbstractŽŸÙœ‘/…sóKñ`y
cmr10²In–]Zthis“papšGer“w¸ãe“try“to“describ˜e“ho¸ãw“Dynamic“Logic“made“it“p˜ossible“a“fruitful“in-Ž¤
™š‘ …rterpla•¸ãy›“bGet“w“een˜Informatics˜and˜Philosoph“y‘ÿ*ª.‘1/It˜did˜so˜b“y˜acting˜as˜a˜common˜language,Ž¡‘ …rspGok•¸ãen›ÊHb“y˜bGoth˜computer˜scien“tists˜and˜analytic˜philosophers.‘СIn˜this˜w“a“y‘ÿ*ª,‘ç…DynamicŽ¡‘ …rLogic–3€oered“the“hš¸ãumanistic“culture“a“new“pGossibilit˜y“of“digesting“and“elabGorating“theŽ¡‘ …rinformatic–UUrevš¸ãolution,“alternativ˜e“with“respGect“to“the“AI-based“approac˜h.ŽŸ"€A‘ …róÂÖN ff cmbx12ÉCon•ŒÌten“tsŽ¦‘ …rïhtml:óò"V
ó3
cmbx10Ê1Ž‘lÏIdola‘2spY‹ecusï html:’Ž2ŽŽ¦‘ …rïhtml:2Ž‘lÏSomething–2abY‹out“the“birth“of“computer“scienceï html:‘\0ÿ3ŽŽ¦‘ …rïhtml:3Ž‘lÏThe–2empirical“w•¦ta“y–2to“the“thinking“mac¦thinesï html:‘mÇ3ŽŽ¦‘ …rïhtml:4Ž‘lÏThe–2logical“foundations“of“programmingï html:’ „
]4ŽŽ¦‘ …rïhtml:5Ž‘lÏThe–2next“step:‘˜¼Dynamic“Logicï html:’ ¸¨P5ŽŽŽŸ ’ Ù¯‡óKñ`y
ó3
cmr10¹1ŽŽŒ‹ * ¿™¬ ýLfT‘ …rïhtml:ï html:ŽŽ •™¬‘ …r ýƒfTïhtml:ï html:© É1Ž‘LËIdola‘ffsps3ecusŽŸq‹¹Human–U!bšMÞeings“usually“lik²!e“to“b˜elong“to“a“group,‘ebb˜eing“it“a“race,‘eba“club“or“moreŽ¤
™šv‘ÿdDaguely–9mthe“extension“of“an“ideology›ÿe.‘¹ŠP•²!arado“xically˜,‘O8ev“en–9mthe“absolute“outsider,Ž¡the–ÉÉone“who“is“alw•²!a“ys–ÉÉagainst,‘¡will“bMÞe“probably“folloš²!wing“a“precise“clic˜h²"‘úÔDe,‘¡aŽ¡stereot•²!ypšMÞe,‘yLen“tering–Oimplicitly“a“so˜cial“group.‘ØAš²!t“the“same“time,‘yLw˜e“also“lik˜eŽ¡to–arrange“other“h²!uman“bšMÞeings“inside“groups,‘Æ©and“to“decipher“the“b˜eha²!viourŽ¡of–ˆMour“felloš²!w“creatures“using“soMÞcial“groups“as“a“k˜ey“of“lecture.‘ƒ’In“this“sense,Ž¡groups–†represenš²!t“a“kind“of“ó ý ':
ó3
cmti10Ëc–ÿp¹ate“gorization–†¹at“a“soMÞcial“lev˜el,‘½ìnecessary“in“orderŽ¡to–|}organize“informations“and“to“elabšMÞorate“opinions“ab˜out“our“en•²!vironmen“t‘|}andŽ¡abMÞout–ãÎourselvš²!es.‘–It“is“easy“and“comfortable“to“sa˜y“things“lik˜e“"Of“course“he“isŽ¡so–Ëßhard-w²!orking:›(Ïhe“is“german!"“or“"I'm“a“real“philosopher:˜I‘ËÕforgot“again“theŽ¡cakš²!e–gOin“the“o˜v˜en!".‘ —The“soMÞcial“realit˜y“is“so“complex“that“w˜e“probably“Ëne–ÿp¹e“d‘gO¹aŽ¡lter–µ¹in“order“to“handle“itïhtml:Ÿü¾ó|{Y cmr8¼1ŽŽ‘Àï html:¹.‘ÖObš²!viously‘ÿe,‘¹Žthis“kind“of“categorization“will“bMÞe“v˜eryŽ¡useful–¦fin“order“to“attribute“a“Ëvalue“¹to“pMÞeople“and“habits“around“us.Ž¡‘ Noš²!w,‘Dâthe–,reason“wh˜y“w˜e“ha˜v˜e“recalled“the“great“impšMÞortance“of“so˜cial“groupsŽ¡for–ÍLmen“and“wš²!omen,‘×is“the“follo˜wing:‘+©w˜e“think“that“the“same“mec˜hanism“is“inŽ¡some–wsense“at“wš²!ork“within“the“am˜bit“of“the“academic“w˜orld,‘€‡where“the“bMÞordersŽ¡among–7disciplines,‘MUdepartmenš²!ts“and“consequen˜tly“pMÞeople“in˜v˜olv˜ed“is“often“thic˜kŽ¡and–ÁÅproudly“cultiv‘ÿdDated.‘/ùManš²!y“in˜tellectuals“ha˜v˜e“a“strong“sense“of“mem˜bMÞershipŽ¡to–ˆÂa“givš²!en“cultural“comm˜unit˜y‘ÿe,‘Ž°and“this“has“eects“at“dieren˜t“lev˜els:‘Ïit“meansŽ¡to–Y3dress“in“a“certain“w•²!a“y‘ÿe,‘h£to–Y3read“certain“b•MÞo“oks–Y3and“ma²!ybMÞe“to“patronize“certainŽ¡caf²"‘úÔDes–»or“restauran²!ts.‘çIt“means“to“share“the“same“commonplaces“abMÞout“the“col-Ž¡leagues–×:of“the“nearbš²!y“departmen˜t“(one“of“the“nest“pleasures“of“life!).‘˜ÎBut,‘ ©mostŽ¡impMÞortanš²!tly‘ÿe,‘8½it–ycan“also“mean“to“cultiv‘ÿdDate“and“to“follo˜w“a“precise“professionalŽ¡training,›qor–ñ4in“other“w²!ords,˜to“teacš²!h“and“to“learn“an“ocial“kno˜w-ho˜w,‘qon“whic˜hŽ¡the–]future“researcš²!h“m˜ust“bMÞe“basedïhtml:Ÿü¾¼2ŽŽ‘Àï html:¹.‘ôThis“ocial“kno˜w-ho˜w“will“probably“setŽ¡also–7the“viable“links“with“other“disciplines“or“researcš²!h“areas“(and,‘Mconsequen˜tly‘ÿe,Ž¡with–):other“h²!uman“v‘ÿdDarieties),‘BCwhile“discouraging“the“connection“with“others.‘´$AsŽ¡I‘Oûsaid,›aUsoMÞcial–Pgroups“do“carry“a“v‘ÿdDalue.‘ÁBefore“Galileo,˜nob•MÞo“dy–Pthoughš²!t“of“pMÞoin˜t-Ž¡ing–€/the“telescopšMÞe“to“the“sky‘ÿe,‘‡Ôalthough“go˜o˜d“lenses“w²!ere“around“in“Europ˜e“sinceŽ¡the›ßXI•MÞI“I‘ºcen•²!tury‘ÿe.‘°The˜reason˜w“as˜that˜opticians˜w“ere˜considered˜as˜to“y-mak“ers,Ž¡and–¦fscience“did“not“tak²!e“them“toMÞo“seriously“for“a“long“time.Ž¡‘ Needless–w to“sa²!y‘ÿe,‘³µbreaking“the“bšMÞorders“among“disciplines“can“b˜e“a“real“ac•²!hiev“e-Ž¡men²!t.‘`It–á’can“raise“new“questions“and“opšMÞen“new“p˜ersp˜ectiv²!es.‘`It“means“to“dis-Ž¡solvš²!e–Çëthe“baconian“Ëidola‘ Àsp–ÿp¹e“cus¹,‘ÐLnamely–Çëthe“phan˜toms“of“our“ho˜v˜el.‘BkThe“pMÞoin˜tŽ¡w•²!e›CŒw“an“t˜to˜mak“e˜is˜that˜Dynamics˜(namely˜Dynamic˜Logic˜plus˜its˜manifoldŽ¡applications–$to“linguistics,–philosoph²!y‘ÿe,“economics›$etc..),“thanks˜to˜the˜w²!ork˜ofŽ¡some–´6opMÞen-minded“researcš²!hers,‘·ªhad“the“v˜ery“respMÞectable“role“of“breaking“someŽ¡cultural–¦fbMÞorders.‘ÝÝLet“us“see“ho²!w.ŽŸ€Aïhtml:ï html:Ÿff‰ ff –Q¸Ÿ
LÍ‘{ºŸü-=ó¹Aa¨ cmr6½1ŽŽŽ‘¦aïhtml:ó$o´‹Ç cmr9ÏTï html:his–TpAÇoinš¾9t“of“view“of“k‘ÿ|ran˜tian“
a˜v˜our“has“bAÇeen“theorized“for“instance“in“[ïhtml:1ï html:Ž‘Ÿþ].ŽŸ ‘{ºŸü-=½2ŽŽŽ‘¦aïhtml:ÏTï html:his–ŒXrecalls“the“Kuhn“theory“abšAÇout“scien¾9tic“theories,‘§¾that“are“to“b˜e“conceiv¾9ed“holisticallyŽ¦as–Kcunivš¾9erses“of“bAÇelief,‘Xçand“consequen˜tly“are“v˜ery“w˜ell“'fortied'“against“what“is“outside“themŽ¦(cf.‘p[ïhtml:5ï html:Ž‘Ÿþ]).ŽŽŸ ’ Ù¯‡¹2ŽŽŒ‹ Ô ¿™¬ ýLfT‘ …rïhtml:ï html:ŽŽ •™¬ ýŽfT‘ …rÉ2Ž‘8Ò=Something–ffabs3out“the“birth“of“computer“scienceŽ©q‹‘ …r¹Computer–öTscience“w²!as“bšMÞorn“under“the“patronage“of“cyb˜ernetics.‘ͨAccording“toŽ¤
™š‘ …rhis–4ýfounding“father,›K«NorbMÞert“Wiener,˜cybMÞernetics“is“the“discipline“studying“con-Ž¡‘ …rtrol–ëand“commš²!unication“in“mac˜hines“and“animals.‘,kIt“deals“with“the“question:Ž¡‘ …rhoš²!w–ëa“giv˜en“message“can“mošMÞdify“the“b˜ehaš²!viour“of“a“living“thing“or“of“a“mac˜hine.Ž¡‘ …rKubšMÞernetik²"‘úÔDe–´´is“in“fact“the“art“of“the“helmsman,‘¸Hof“the“one“who“elab˜orates“andŽ¡‘ …rorganizes–}¡commands.‘ÐFConcretely‘ÿe,‘…ÈcybMÞernetics“aims“to“the“study“and“the“math-Ž¡‘ …rematical–×Icš²!haracterization“of“biological“proMÞcesses,‘#in“order“to“build“mac˜hines,Ž¡‘ …rautomata.‘Ø+F‘ÿerom–O+this“short“denition“a“parallel“already“arises,‘y\whic²!h“will“bMÞe-Ž¡‘ …rcome–cÊa“kind“of“guide-metaphor“of“the“computer“culture:‘¼the“in²!triguing“parallelŽ¡‘ …rbMÞet•²!w“een›¤ømac“hines˜and˜living˜organisms.‘Ù“A“t˜a˜rst˜lev“el,‘äœmac“hines˜can˜em“u-Ž¡‘ …rlate–the“bMÞehaš²!viour“of“living“things,‘9‰and“giv˜e“the“appropriate“answ˜ers“to“giv˜enŽ¡‘ …rstim•²!uli.‘Õ³A“t–ùa“deepMÞer“lev•²!el,‘
ªmac“hines–ùcan“evš²!en“sim˜ulate“the“proMÞcesses“going“onŽ¡‘ …rwithin–ËÃliving“things“(cf.‘Mõfor“instance“[ïhtml:2ï html:Ž‘yš],‘Õwhere“the“authors“try“to“expMÞort“fromŽ¡‘ …rthe–¦fanimal“wš²!orld“to“the“mac˜hines“the“mec˜hanisms“of“recognitions“of“forms).Ž¡‘1…rThe–Þsecond“short“remark“abMÞout“the“origins“of“computer“science“is“the“follo²!w-Ž¡‘ …ring.‘(MMošMÞdern–‹computers“w²!ere“b˜orn“for“meeting“practical“needs.‘(MIf“clo˜cš²!ks“w˜ereŽ¡‘ …ralmost–5Unecessary“in“the“commercially“activš²!e“soMÞciet˜y“of“the“Renaissance,‘Kòso“w˜ereŽ¡‘ …rcalculators–_ñin“the“industrialized“soMÞcietš²!y“of“the“end“of“the“last“cen˜tury‘ÿe,‘nand“ev˜enŽ¡‘ …rmore–-in“the“daš²!wning“global“village“of“the“bMÞeginning“of“our“cen˜tury–ÿe.‘µiW“e–-cite“t˜w˜oŽ¡‘ …rsignicanš²!t–®historical“facts.‘öƒThe“rst“relev‘ÿdDan˜t“use“of“punc˜hed“cards“mac˜hinesŽ¡‘ …rdates–'Òbac²!ks“to“1890,‘A#when“Herman“Hollerith“applied“them“to“the“american“cen-Ž¡‘ …rsus.‘¥In–ü our“cen²!tury‘ÿe,›.the“golden“age“of“computers“starts“in“the“forties,˜during“theŽ¡‘ …rsecond–nwš²!orld“w˜ar,‘ and“this“circumstance“will“aect“in“part“the“empirical“na-Ž¡‘ …rture–5of“informatics:‘˜EWiener“devš²!elops“some“cen˜tral“ideas“abMÞout“calculators“whileŽ¡‘ …rattempting–úto“solvš²!e“the“problem“of“predicting“the“route“in“la˜ying“an˜ti-aircraftŽ¡‘ …rw²!eapMÞons.Ž‘ …rŸ¡Rïhtml:ï html:ŸÞïÉ3Ž‘LËThe–ffempirical“w•ŒÌa“y–ffto“the“thinking“macŒÌhinesŽ¦¹W‘ÿee–;Jthink“that“computer“science“has“bMÞeen“in“some“w•²!a“y›;Jmark“ed˜b“y˜these˜aspMÞectsŽ¡w•²!e›¦fha“v“e˜seen,˜namely:ŽŸ¡ïhtml:ï html:©
x‰‘
-1.ŽŽŽ‘the–parallel“bMÞet•²!w“een›mac“hines˜and˜living˜things,‘:µcoming˜from˜the˜cybMÞer-Ž¡‘netic‘¦fculture;ŽŸ!ïhtml:ï html:¦‘
-2.ŽŽŽ‘the–ä]empirical“researc²!h“program“that“acted“as“an“incubator“for“the“rstŽ¡‘computers;ŽŸšConcerning–ô³1),‘Eit“is“in²!teresting“to“see“that“from“the“bMÞeginning“informatics“ap-Ž¡p•MÞears›G!b“efore˜the˜public˜opinion˜as˜something˜v•²!ery˜m“uc“h˜link“ed˜with˜robMÞots˜andŽ¡similar.‘É^But–hèalso“at“a“more“serious“levš²!el,‘u4the“big“c˜hallenge“that“informatics“hasŽ¡issued–âto“the“culture“of“(part“of‘ Ú)“our“cenš²!tury“concerns“the“pMÞossibilit˜y“of“buildingŽ¡an›u„in•²!telligen“t˜mac“hineïhtml:Ÿü¾¼3ŽŽ‘Àï html:¹.‘Í’P“oin“t˜2)˜has˜a˜lot˜to˜do˜with˜what˜w“e˜ha“v“e˜said˜abMÞoutŽŸ
#2‰ ff –Q¸Ÿ
LÍ‘{ºŸü-=½3ŽŽŽ‘¦aïhtml:ÏNï html:otice–Š²that“while“Articial“Inš¾9telligence“w˜as“gro˜wing“up,‘è the“couple“mac˜hine-programŽ¤ turned–šout“not“to“bAÇe“so“adequate“in“order“to“in¾9terpret“the“most“complex“phenomena“ofŽ¡life–¸and“in•¾9ten“tionalit“y‘ÿ:«.‘€The–¸idea“of“a“programmable“macš¾9hine“is“not“able“to“accoun˜t“for“theŽŽŸ ’ Ù¯‡¹3ŽŽŒ‹ = ¿™¬ ýLfT‘ …rïhtml:ï html:ŽŽ •™¬ ýŽfT‘ …r¹idola–z°spšMÞecus:‘Ècomputers“w²!ere“b˜orn“in“a“certain“hš²!uman“en˜vironmen˜t,‘ƒnwhic˜h“hasŽ¤
™š‘ …rset–¦fthe“range“of“the“admissible“in²!tellectual“elabMÞorations.Ž¡‘1…r>F‘ÿerom–…the“comš²!bination“of“1)“and“2)“w˜e“can“dra˜w“a“simple“conclusion.‘®’Com-Ž¡‘ …rputer–9|science“has“bMÞeen“aimed“for“a“long“time“to“the“designing“of“mac²!hines“moreŽ¡‘ …rand–é×more“quicš²!k“and“compMÞeten˜t,‘more“'in˜telligen˜t'“in“a“broad“sense.‘ŸIn“this“dom-Ž¡‘ …rinanš²!t‘+p•MÞersp“ectiv˜e,‘-programs–+and“programming“languages“ha˜v˜e“bMÞeen“conceiv˜edŽ¡‘ …ras–Š¶instrumenš²!ts,‘ÃÉtotally“functional“to“their“task.‘ŠÌPrograms“as“instrumen˜ts“doŽ¡‘ …rnot–bÝneed“to“bMÞe“based“on“a“solid“theory‘ÿe,‘p_they“only“need“to“w²!ork;‘y`and“in“order“toŽ¡‘ …rc•²!hec“k–¦fthat“they“do“w²!ork“propMÞerly‘ÿe,“it“is“enough“to“test“them“and“kill“the“bugs.Ž‘ …rŸ¡Rïhtml:ï html:ŸÞïÉ4Ž‘LËThe–fflogical“foundations“of“programmingŽŸq‹¹Around–ìthe“end“of“the“sixties,‘97a“mo•²!v“emen“t–ìarises“within“the“in²!ternational“infor-Ž¡matics›âPcomm•²!unit“y˜that˜aims˜to˜pro“vide˜programming˜with˜a˜logical˜foundation.Ž¡Computers›Ìòha•²!v“e˜already˜en“tered˜oces,–”factories,“and˜their˜use˜is˜spreadingŽ¡rapidly‘ÿe.›§oThe–”AËinformatization“¹of“soMÞciet²!y“has“started.˜In“fronš²!t“of“this“gro˜wingŽ¡impMÞortance–ÿkof“computers,‘¬some“researcš²!h“groups“raise“the“question“of“c˜hec˜kingŽ¡in–Ñsome“w•²!a“y–Ñthe“theoretical“v‘ÿdDaliditš²!y“of“programming.‘]ÌIn“particular,‘´giv˜en“aŽ¡computer–D¦program“ó! b>
ó3
cmmi10Ìd“¹,‘l6they“try“to“see“if“it“is“pMÞossible“to“pro•²!v“e–D¦that“Ì‘©9¹satisesŽ¡the›Ppin•²!ten“tions˜of˜the˜programmer,‘a¡namely˜that˜Ì‘µ¹is˜correct.‘Á6The˜idea˜comes˜upŽ¡to–öšbuild“formal“languages“that“can“talk“abMÞout“programs,‘
§and“to“create“formalŽ¡systems–žG(axioms“and“rules)“to“pro•²!v“e–žGfacts“abšMÞout“them.‘Û(The“imp˜ortance“of“thisŽ¡question–&is“not“only“theoretical:‘•^the“consequences“of“a“wrong“program“can“bMÞeŽ¡incredibly–¦fbig.‘ÝÝQuoting“[ïhtml:3ï html:Ž‘yš]:Ž©š‘.–Ó3.“.“the–qõcost“of“error“in“certain“tš²!ypMÞes“of“program“ma˜y“bMÞe“almost“incal-Ž¡‘culable–žo-“a“lost“spacecraft,› a“collapsed“building,˜a“crashed“aeroplane,Ž¡‘or–¦fa“wš²!orld“w˜ar.Ž¦Giv²!en–òAthat,›8the“idea“of“Ëfounding“¹computer“programs,˜pro²!ving“their“metaprop-Ž¡erties,‘™vimmediately–hÙcaptures“the“inš²!terest“of“man˜y“researc˜hers.‘%7Therefore,‘™vtheŽ¡seminal–åèpapšMÞer“[ïhtml:3ï html:Ž‘yš]“will“b˜ecome“one“of“the“most“quoted“pap˜ers“in“the“history“ofŽ¡computer‘¦fscience.Ž¡‘ Easy––Úto“guess,‘Òöthis“great“researcš²!h“pro‘ ›»ject“started“some“30“y˜ears“ago“rep-Ž¡resenš²!ts–¾from“our“pMÞoin˜t“of“view“a“rst“impMÞortan˜t“step“for“breaking“the“originalŽ¡bMÞorders–E¦of“computer“science.‘½It“brings“computer“science“v²!ery“closed“to“the“mit-Ž¡teleuropMÞean–¢rmathematical“tradition:‘Ûãthe“Hoare“program“is“quite“similar“to“theŽ¡HilbšMÞert–gprogram!‘!)Here“is“again“an“imp˜ortan²!t“-“and“explicit“-“quotation“fromŽ¡[ïhtml:3ï html:Ž‘yš]:Ž¦‘In–Àthis“papMÞer“an“attempt“is“made“to“explore“the“logical“foundationsŽ¡‘of–Žcomputer“programming“bš²!y“use“of“tec˜hniques“whic˜h“w˜ere“rst“ap-Ž¡‘plied–Oin“the“study“of“geometry“and“ha•²!v“e–Olater“bMÞeen“extended“to“otherŽ¡‘brancš²!hes–8šof“mathematics.‘ ”zThis“in˜v˜olv˜es“the“elucidation“of“sets“ofŽŸff‰ ff –Q¸Ÿ
LÍÏorganization–ninside“a“living“thing;‘š…DNA,“for“instance,‘„Rcannot“bAÇe“explained“without“referringŽ¤ to–7±the“enzymatic“proteins“that“rule“its“transcription“and“translation,‘@Hbut“these“are“proAÇducedŽ¡b¾9y–Tthe“action“of“DNA“itself.ŽŽŸ ’ Ù¯‡¹4ŽŽŒ‹ (Ý ¿™¬ ýLfT‘ …rïhtml:ï html:ŽŽ •™¬ ýŽfT‘8œ~¹axioms–RÉand“rules“of“inference“whic²!h“can“bšMÞe“used“in“pro˜ofs“of“theŽ¤
™š‘8œ~propMÞerties–¦fof“computer“programs.Ž©š‘ …rAccordingly‘ÿe,‘šthe–ÁÃHoare“program“has“had“a“v‘ÿdDast“cultural“signicance.‘/õIt“hasŽ¡‘ …rtransformed–”programming“from“a“kind“of“handicraft“inš²!to“a“science,‘Êâin˜to“a“branc˜hŽ¡‘ …rof–ÃEmathematics.‘4yThe“big“moral“of“the“story“is“that“computer“programs“canŽ¡‘ …rbšMÞe–ñ£studied“at“a“metalev²!el,‘Dqas“pure“mathematical“ob‘ ›»jects.‘¿“They“cease“to“b˜eŽ¡‘ …rmere–ú÷instrumenš²!ts“to“reac˜h“a“task,‘or“defectiv˜e“imitations“of“h˜uman“inferen˜tialŽ¡‘ …rproMÞcesses.‘J¤Rather,›©they–uSacquire“an“autonomous“status,˜and“they“deserv²!e“theŽ¡‘ …rattenš²!tion–¦fof“in˜tellectuals“outside“the“informatic“comm˜unit˜y‘ÿe.Ž‘ …rŸ¡Rïhtml:ï html:ŸÞïÉ5Ž‘LËThe–ffnext“step:‘32Dynamic“LogicŽŸq‹¹A‘ƒòfew–„+yš²!ears“after“the“publication“of“[ïhtml:3ï html:Ž‘yš]“a“v˜ery“nice“truth“comes“to“the“ligh˜t:Ž¡that–?ÊHoare“calculus“can“bšMÞe“seen“as“a“m²!ultimo˜dal“logic.‘ªHere“is“a“quotation“IŽ¡lik²!e‘¦f([ïhtml:4ï html:Ž‘yš]):Ž¦‘In–ÜÍthe“spring“of“1974“I‘Ü}wš²!as“teac˜hing“a“class“on“the“seman˜tics“andŽ¡‘axiomatics–‰Áof“programming“languages.‘‡ïA²!t“the“suggestion“of“one“ofŽ¡‘the–ì²studen²!ts,›ÖR.“MoMÞore,˜I‘ìƒconsidered“applying“moMÞdal“logic“to“a“formalŽ¡‘treatmenš²!t–ʳof“a“construct“due“to“C.A.R.“Hoare,–ö¤Ìpó"!",š
ó3
cmsy10ÍfÌaÍgÌqd“¹,“whic˜h‘ʳexpressesŽ¡‘the–hnotion“that“if“Ìp“¹holds“bMÞefore“executing“program“Ìa“¹then“Ìq‘͹holdsŽ¡‘afterw•²!ards.‘¾Although›GI‘Füw“as˜sceptical˜at˜rst,‘Z$a˜w“eek“end˜with˜HughesŽ¡‘and–ì£Cresswš²!ell“con˜vinced“me“that“a“most“harmonious“union“bMÞet˜w˜eenŽ¡‘mošMÞdal–¦flogic“and“programs“w²!as“p˜ossible.Ž¦In–Xother“wš²!ords,‘g¼the“formalism“of“in˜tensional“logic“turns“out“to“bMÞe“ideal“in“orderŽ¡to›ø–pro•²!v“e˜metaprop•MÞerties˜of˜computer˜programs.‘ÔmAnd˜here˜the˜b“order˜reallyŽ¡collapses:‘Ý•computer–¥Öscience“shoš²!ws“a“deep,‘¥óessen˜tial“link“with“that“part“of“logicŽ¡that–½æmost“happily“marries“with“analytic“philosophš²!y“and“with“classical“w˜esternŽ¡philosophš²!y‘ÿe.‘³It–&is“again“the“leibnizean“pMÞossible“w˜orlds“that“w˜e“are“talking“abMÞout!Ž¡‘ Hoare–¬°Calculus“and“Dynamic“Logic“opMÞened“a“fruitful,‘®Binš²!teresting“w˜a˜y“fromŽ¡computer–=gscience“to“a“certain“area“of“hš²!umanities.‘ºÝThey“actually“oered“the“h˜u-Ž¡manistic–5Ðculture“a“new“pšMÞossibilit²!y“of“digesting“and“elab˜orating“the“informaticŽ¡rev•²!olution,‘³Âalternativ“e–wwith“respMÞect“to“the“Articial“Inš²!telligence-based“approac˜h.Ž¡In–~îa“slogan,‘†ÓAI‘~äpromotes“the“idea“that“in•²!telligen“t–~îphenomena“can“bMÞe“mimic•²!k“edŽ¡and–ÝYreproMÞduced“within“mac²!hines.‘šÙOn“the“other“hand,‘the“philosophical“messageŽ¡bMÞehind–ýXthe“dynamic“w•²!a“y–ýXis“that“the“formalisms“used“for“programming“mac²!hinesŽ¡can–ÄBbMÞe“emplo•²!y“ed–ÄBin“their“mathematical“pureness“as“kš²!eys“for“in˜terpreting“in˜tel-Ž¡ligenš²!t–¦fphenomena.‘ÝÝQuoting“[ïhtml:6ï html:Ž‘yš],“here“is“the“impMÞort“of“this“researc˜h“program:Ž¦‘In–årecenš²!t“y˜ears,‘t¨there“has“bMÞeen“a“gro˜wing“in˜terest“in“the“logicalŽ¡‘structure–5¤of“cognitivš²!e“actions“underlying“h˜uman“reasoning“or“nat-Ž¡‘ural– ‰language“understanding.‘ìET‘ÿeraditional“logic“and“philosophš²!y“ha˜v˜eŽ¡‘bšMÞeen– xmainly“concerned“with“the“pro˜ducts“of“these“actions,‘Þüsuc²!h“asŽ¡‘though²!ts,–cAprošMÞofs,“prop˜ositions.‘£But–=|in“v‘ÿdDarious“disciplines,‘cAincludingŽ¡‘philosoph²!y‘ÿe,›fûcomputer–@wscience“and“linguistics,˜the“mec²!hanisms“of“in-Ž¡‘formation–*ï
oš²!w“themselv˜es“are“bMÞecoming“primary“ob‘ ›»jects“of“study‘ÿe.ŽŽŸ ’ Ù¯‡5ŽŽŒ‹ 8: ¿™¬ ýLfT‘ …rïhtml:ï html:ŽŽ •™¬ ýŽfT‘8œ~¹This–Ê“in²!terest“re
ects“a“broader“cultural“in
uence“of“computationalŽ¤
™š‘8œ~paradigms‘¦f.–Ó3.“.ŽŸš‘ …rW‘ÿee–؈think“that“this“'cultural“in
uence“of“computational“paradigms'“on“the“philo-Ž¡‘ …rsophical–j tradition“has“bšMÞeen“made“p˜ossible“bš²!y“the“disco˜v˜ery‘ÿe,›šñso“to“spMÞeak,˜of“aŽ¡‘ …rcommon–fñlanguage,‘—spMÞokš²!en“at“the“same“time“b˜y“informatics“and“analytic“phi-Ž¡‘ …rlosoph²!y‘ÿe,‘¤and–qIthis“common“language“is“Dynamic“Logic.‘>…Dynamic“Logic“madeŽ¡‘ …rit–û˜pMÞossible“an“inš²!triguing“cultural“con˜tamination.‘ÝsThe“dynamic“in˜ternationalŽ¡‘ …rcomm•²!unit“y–¦fis“harv²!esting“the“appMÞealing“fruits.–Ó3.“.ŽŸ"€A‘ …rÉReferencesŽ‘ …rŸ×ñï html:ï html:ïhtml:ï html:Ÿ™š‘yš¹[1]ŽŽ‘‚$H.–˜CT‘ÿea‘ ›»jfel,›ÎJC.“Flamen²!t,˜M.“Billing,˜R.P‘ÿe.“Bundy“(1971),˜ËSo–ÿp¹cial‘òdCate“gorizationŽ¡‘‚$and›êêInter–ÿp¹gr“oup˜Behaviour¹,–¦fin:‘ÝÝEuropšMÞean“Journal“of“So˜cial“Psyc²!hology‘ÿe,“1.Ž©!ï html:ï html:ïhtml:ï html:Ÿ
x‰‘yš[2]ŽŽ‘‚$H.R.–rVMaturana,›ePJ.Y.“Lettvin,˜W.S.“McCulloMÞc²!h,˜W.H.“Pitts“(1960),Ž¡‘‚$ËA¸\natomy–ƒÁand“physiolo›ÿp¹gy“of“vision“in“the“fr˜o˜g¹,‘L±in:‘¥ÌJournal–6Dof“General“Ph²!ys-Ž¡‘‚$iology‘ÿe,‘¦f43.Ž¦ï html:ï html:ïhtml:ï html:Ÿ
x‰‘yš[3]ŽŽ‘‚$C.A.R.–*kHoare“(1969),›C7ËA¸\n–xÚAxiomatic“Basis“for“Computer“Pr–ÿp¹o“gr“amming¹,˜in:Ž¡‘‚$Commš²!unications–¦fof“the“A˜CM,“12.Ž¦ï html:ï html:ïhtml:ï html:Ÿ
x‰‘yš[4]ŽŽ‘‚$V.R.–D)Pratt“(1980),‘WÎËApplic›ÿp¹ation–‰of“Mo˜dal“L˜o˜gic“to“Pr˜o˜gr˜amming¹,‘WÎin:‘¬¾StudiaŽ¡‘‚$Logica,‘¦f39.Ž¦ï html:ï html:ïhtml:ï html:Ÿ
x‰‘yš[5]ŽŽ‘‚$T.S.–—Kuhn“(1962),‘šËThe–ÜÀstructur›ÿp¹e“of“Scientic“R˜evolutions¹,‘šThe‘—Univ•²!ersit“yŽ¡‘‚$of‘¦fChicago.Ž¦ï html:ï html:ïhtml:ï html:Ÿ
x‰‘yš[6]ŽŽ‘‚$J.–É0v‘ÿdDan“Ben²!them“(1996),‘âËExploring›öpL–ÿp¹o“gic“al˜Dynamics¹,‘âCSLI‘ÈæPublicationsŽ¡‘‚$and‘¦ffolli.ŽŽŸ ’ Ù¯‡6ŽŽŒø Gʃ’À; è¿™¬˜S6 ó$o´‹Ç cmr9ó"!",š
ó3
cmsy10ó! b>
ó3
cmmi10ó ý ':
ó3
cmti10óò"V
ó3
cmbx10óÂÖN ff cmbx12óò"V
cmbx10ó¹Aa¨ cmr6ó|{Y cmr8óX«Q cmr12óDÓít G® G® cmr17óKñ`y
ó3
cmr10óKñ`y
cmr10ù Pùßßßß