On focusing and polarities in linear logic and intuitionistic logic Chuck Liang

Description

Niveau: Supérieur, Doctorat, Bac+8
On focusing and polarities in linear logic and intuitionistic logic Chuck Liang Hofstra University Hempstead, NY Dale Miller INRIA & LIX/Ecole Polytechnique Palaiseau, France Draft: December 15, 2006 Abstract There are a number of cut-free sequent calculus proof systems known that are complete for first-order intuitionistic logic. Proofs in these different systems can vary a great deal from one another. We are interested in providing a flexible and unifying framework that can collect together important aspects of many of these proof systems. First, we suggest that one way to unify these proof systems is to first translate intuitionistic logic formulas into linear logic formulas, then assign a bias (positive or negative) to atomic formulas, and then examine the nature of focused proofs in the resulting linear logic setting. Second, we provide a single focusing proof system for intuitionistic logic and show that these other intuitionistic proof systems can be accounted for by assigning bias to atomic formulas and by inserting certain markers that halt focusing on formulas. Using either approach, we are able to account for proof search mechanisms that allow for forward-chaining (program-directed search), backward-chaining (goal- directed search), and combinations of these two. The keys to developing this kind of proof system for intuitionistic logic involves using Andreoli's completeness result for focusing proofs and Girard's notion of polarity used in his LC and LU proof systems.

• cut-free proofs


• systems can


• intuitionistic logic


• sequents changes


• andreoli's completeness theorem


• compact focusing calculus


• original proof

Sujets

• Philippus Baldaeus
• École polytechnique
• Saurin
• Hofstra University
• Intuitionistic logic

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 24
• Langue: English

Extrait

Onfocusingandpolaritiesinlinearlogicandintuitionisticlogic

ChuckLiangDaleMiller
HHofesmtrpastUeanidv,erNsiYtyINRIA&PLalIaXis/eEacuo,leFrPaonlcyetechnique
Draft:December15,2006

Abstract
Thereareanumberofcut-freesequentcalculusproofsystemsknownthatarecompleteforfirst-order
intuitionisticlogic.Proofsinthesedifferentsystemscanvaryagreatdealfromoneanother.Weare
interestedinprovidingaflexibleandunifyingframeworkthatcancollecttogetherimportantaspectsof
manyoftheseproofsystems.First,wesuggestthatonewaytounifytheseproofsystemsistofirst
translateintuitionisticlogicformulasintolinearlogicformulas,thenassignabias(positiveornegative)
toatomicformulas,andthenexaminethenatureoffocusedproofsintheresultinglinearlogicsetting.
Second,weprovideasinglefocusingproofsystemforintuitionisticlogicandshowthattheseother
intuitionisticproofsystemscanbeaccountedforbyassigningbiastoatomicformulasandbyinserting
certainmarkersthathaltfocusingonformulas.Usingeitherapproach,weareabletoaccountforproof
searchmechanismsthatallowforforward-chaining(program-directedsearch),backward-chaining(goal-
directedsearch),andcombinationsofthesetwo.Thekeystodevelopingthiskindofproofsystemfor
intuitionisticlogicinvolvesusingAndreoli’scompletenessresultforfocusingproofsandGirard’snotion
ofpolarityusedinhisLCandLUproofsystems.

1

Contents
1Introduction3
2FocusedproofsinLinearlogic6
2.1Synchronousandasynchronousproofsearch............................6
2.2Assignmentofbias..........................................8
2.3Themeaningofbias.........................................8
3TranslatingLJProofs10
4TranslatingLJQandLJT17
4.1LJQ’..................................................17
4.2LJT’..................................................22
5MixedPolaritiesand
λ
RCC25
5.1
λ
RCC.................................................25
5.2EnhancedForward-Chaining.....................................26
5.3TowardsaStronglyFocusedSystemwithMixedPolarities....................27
6UnifiedFocusingforIntuitionisticLogic28
6.1OptimizingAsynchronousDecomposition.............................28
6.2PermeableAtomsandTheirPolarity................................30
6.3CompletingtheTranslation.....................................32
6.4LJF
0
..................................................33
6.5LJF..................................................38
6.6TheNeutralFragment........................................39
6.7DecoratingIntuitionisticConjunction................................41
7CutElimination43
7.1AdmissibilityofCuts.........................................44
7.2SimultaneousEliminationofCuts..................................48
8EmbeddingIntuitionisticSystemswithinLJF53
8.1EmbeddingLJTinLJF.......................................54
8.2EmbeddingLJ............................................55
9EmbeddingClassicalLogicinIntuitionisticLogic57
9.1LKF..................................................58
9.2CorrectnessofLKF..........................................62
9.3DerivingLKFfromLinearLogic..................................64
10Futurework65
10.1Cut-EliminationforLKF......................................65
10.2Multi-SuccedentIntuitionisticLogic................................65
10.3FocusedLU..............................................65
10.4ExtensiontoSecondOrderQuantifiers...............................66
11Conclusion66
2

1Introduction
Wewishtorefineourunderstandingofthestructureofproofsinintuitionisticlogic.Inparticular,wewillbe
concernedwithhowtostructurethenon-determinismthatarisesinthesearchforcut-freeproofs.Indoing
so,wehopetoprovideatheoreticalfoundationforunderstandingproofsearchmechanismsbasedonforward-
chaining(program-directedsearch),backward-chaining(goal-directedsearch),andtheircombinations.Such
afoundationshouldfindapplicationinthebuildingoflogicprogrammingandautomateddeductionsystems,
andinthestudyofvariousterm-reductionsystems.
Inlogicprogramming,computationismodeledbytheprocessofsearchingfora
cut-free
prooffrom
the“bottom-up”:asattemptstoprovesequentsgiverisetoattemptstoproveadditionalsequents,the
structureofsequentschanges.Thelogicprogrammeristhenabletousethisdynamicsofchangestoencode
computation.Theroleofcutandthecut-eliminationtheoremisrelegatedtoprovidingmeanstoreason
aboutcomputation.Thus,ourinteresthereindevelopingnormalformsforcut-freeproofs.
AprincipletoolforanalyzingproofsearchisAndreoli’scompletenesstheoremfor
focused
proofs[And92].
Sincethatresultholdsforlinearlogic,weshalldevelopanumberoftranslationsofintuitionisticlogic
intolinearlogic.Girard’soriginaltranslation[Gir87]ofintuitionisticlogicintolinearlogicwasbasedon
mappingalloccurrencesoftheintuitionisticimplication
B
⊃
C
totheformula!
B
−◦
C
.Usingsucha
mapping,itispossibletofindtightcorrespondencebetweenintuitionisticproofsandlinearlogicproofs
preservesthedynamicsofcut-elimination.Ifoneisinterestedincapturingonlycut-freeproofsfor,say,
first-orderlogics,thenitispossibletopredictwhethersubformulasoftheendsequentappearontheleftor
theright-handsideofsequentsintheproofjustbyobservingtheiroccurrencesinendsequent.(Suchan
invariantisnotgenerallytruewhenhigher-orderquantificationispresent[MNPS91,Section5].)Insuch
settings,intuitionisticformulascanbemappedintwodifferentwaysdependingonwhetherornottheyoccur
ontheleftorrightofsequents.Forexample,HodasandMiller[HM94]usedtwotranslationssuchthat
[
B
⊃
C
]
+
=![
B
]
−
−◦
[
C
]
+
and[
B
⊃
C
]
−
=[
B
]
+
−◦
[
C
]
−
.
Noticethatsuchamappingtranslatestheinitialsequent
B
⊃
C
−→
B
⊃
C
to[
B
]
+
−◦
[
C
]
−
−→
![
B
]
−
−◦
[
C
]
+
,
whichisprovable(butnotinitial)ifweassume,inductively,that[
C
]
−
−→
[
C
]
+
and[
B
]
−
−→
[
B
]
+
are
provable.Suchtranslationsbasedonapairofmutuallyrecursivetranslationsiscalledhere
asymmetrical
translations
:mosttranslationsthatmapintuitionisticlogicintolinearlogicconsideredinthispaperare
asymmetric.
Thetranslationsthatwedescribeareallbasedonassigninganswerstothefollowingquestions.
•
Wheretoinsertexponentials(!or?)?Forexample,theonlydifferencebetweenthetwotranslations
displayedaboveforimplicationisthatonecontainsa!thattheotherdoesnot.
•
Doesaconnectivegetmappedtoamultiplicativeoradditiveconnective?Forexample,thetranslations
usedin[HM94]resolvesthatchoiceforconjunctionas
[
B
∧
C
]
+
=[
B
]
−
⊗
[
C
]
+
and[
B
∧
C
]
−
=[
B
]
+
&[
C
]
−
.
Giventheprescenceof!inthetranslationsofintuitionisticlogicandthefactthatthatexponential
canchangeanadditivetoamultiplicative,thischoiceisoccasionallynotsimplybinary.
•
Whatisthepropertreatmentofatoms?Oftenatom
A
ismapped
A
orto!
A
.A
bias
foratomsmust
oftenbeassignedsothatfocusingproofscanbeproperlydefined.
Eventually,wepresentanewfocusedproofsystemforintuitionisticlogic.Thissystemwillsupportthe
mixingofpolaritiesduringproofsearch.Thatis,itwillsupportbothforwardandbackwardchaining.There
mightbevariouswaystomotivateandvalidateourdesign:forexample,coherentspacesemanticsisused
bysometomotivaterelatedproofsystemssuchasLC[Gir91].Ultimately,thesuccessofoursearchforan
intuitionisticfocusingsystemwillresultfromabetterunderstandingofthenotionofpolarity:specifically
howpolarityasdefinedinLCandLU[Gir93]relatetotheoperationalbehavioroffocusedproofs.The

3

designofoursystemswillbemotivatedentirelyprooftheoretically.Thatis,thereasonsforourchoicesin
designwillbeoperational:theactualprocessofsearchingforproofswilloftenbeconsidered.Ourapproach
hastheadvantageofbeingessentiallyelementaryandselfcontained.
TherearecloseconnectionsbetweenourworkandthoseofDanos,JoinetandSchellinx[DJS95,DJS97].
Manyconceptswhichtheyinitiallyexplored,suchas
inductivedecorations,
areusedthroughoutouranalysis.
Whereourworkdivergesfromtheirs,however,isintheadoptationofAndreoli’sfocusingcalculusasourmain
instrumentofconstruction(deconstruction?).Theworkof[DJS97]wasbasedonanin-depthanalysisofcut
eliminationinclassicallogic.Their
LK
pη
systemessentiallyreformulatesfocusingnotasasequentcalculus
butasaprotocolforconstructingproofs.Itsconnectionstopolarizationandfocusingwerefurtherexplored
andextendedbyLaurent,QuatrinianddeFalco[LQdF05]using
polarizedproofnets.
Itislikelythatthese
alternativeformalismscanbeadjustedtointuitionisticlogicandreplaceAndreoli’ssequentcalculusasthe
meanstoaccomplishourgoals.WefindAndreoli’sapproachsuitablebecauseourtargetsarealsosequent
calculi,whichcanbeeasilyimplemented.Moreover,Andreoli’ssystemdefinesfocusingfor
full
linearlogi