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

English
68 Pages
Read an excerpt
Gain access to the library to view online
Learn more

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


Subjects

Informations

Published by
Reads 24
Language English
Report a problem

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

systemessentiallyreformulatesfocusingnotasasequentcalculus
butasaprotocolforconstructingproofs.Itsconnectionstopolarizationandfocusingwerefurtherexplored
andextendedbyLaurent,QuatrinianddeFalco[LQdF05]using
polarizedproofnets.
Itislikelythatthese
alternativeformalismscanbeadjustedtointuitionisticlogicandreplaceAndreoli’ssequentcalculusasthe
meanstoaccomplishourgoals.WefindAndreoli’sapproachsuitablebecauseourtargetsarealsosequent
calculi,whichcanbeeasilyimplemented.Moreover,Andreoli’ssystemdefinesfocusingfor
full
linearlogic.
WedemonstratethatthismeansthatitisinfactendowedwiththepowerofLU,andisthereforeasuitable
choiceasahost-logicframework.Ourapproachtothissubjectiselementary.Weexaminethestructureof
cut-freeproofs,basingourconstructionsonwell-establishedcuteliminationtheoremsandthecorrectnessof
thelinearfocusingcalculus.Theendresultisacompactfocusingcalculusforfullintuitionisticlogic,with
whichwecanalsoderiveasimilarsystemforclassicallogic.Ourworkcanbeextendedtosecondorderlogic,
althoughthispaperismainlyconcernedwithfirst-orderintuitionisticlogic.
Thispaperhastwomajorgoals.First,weshowthatanumberofknownintuitionisticproofsystems
(LJT,LJQ,and
λ
RCC)canbederivedandprovedcorrectbyfirsttranslatingintuitionisticlogicformulas
intolinearlogicandshowingthatfocusedproofsofthetranslatedformulasareinone-to-onecorrespondence
toproofsintheoriginalsequentcalculus.Thus,theessentialcharacteroftheoriginalproofsystemis
capturedbythewayitistranslatedintolinearlogic.Thisapproachtoproofsystemsinintuitionisticlogic
hasaparallelwiththewaythatcontinuation-passingstyletranslationsareusedtomakeexpliciteither
call-by-nameorcall-by-valueevaluation[Plo76]:thestrategyisencodedinthetranslation.Intheproof
searchsetting,wehaveachoiceofdoinggoal-directedorprogram-directedproofsearchoracombinationof
both.Whichwaythisisdoneiscapturedhereviatranslationsintolinearlogic.
Thesecondmajorgoalistheintroductionofanewproofsystem,LJF,thatallowsustocapturefo-
cusedproofsearchinintuitionisticlogic.Weillustratethatotherproofsystemsforintuitionistilogiccan
beaccountedforbyinsertinglogicalexpressionsintointuitionisticformulasthatprematurelyhaltthede-
terministicaspectsofproofsearchinLJF.Finally,weusethenewsystemLJFtoderiveafocusedsequent
calculusforclassicallogicthatsupportsitsconstructivecharacteristics(inthesenseofLC).
Thestructureofcompletenessproofs
Astandardformatwillbeusedtoprovethesoundnessand
completenessofanumberofproofsystems.ItisillustratedwiththehelpofFigure1.Thefoundationof
theformatisatranslationfromintuitionisticlogictolinearlogiccalledthe“0/1”translation.Abijective
mapping(indicatedbyatwo-wayarrow)isestablishedbetweenarbitraryLJproofs(indicatedby
`
I
)and
focusedproofsinlinearlogicofthetranslatedimage(indicatedwith
`⇑
).Supposewethenwishtoproof
thesoundnessandcompletenessofsomeotherintuitionisticproofsystem,labeled
`
O
.Wedeviceanother
translation,labeled
l/r
,thatalsomaps
`
O
proofstofocusedproofsofitsimageinlinearlogic(
`⇑
withrespect
tothe
l/r
translation).Itwillthenbeshownthatproofsunderthe0/1translationcanbetransformedinto
proofsunderthenewtranslation.Asisusuallythecase,thesoundnessof
`
O
withrespecttoLJwillbe
trivial(indicatedbythearrowfrom
`
O
to
`
I
).Thiscompletesa“grandtour”thatestablishestheequivalence
amongfourdistinctnotionsofprovability.Consequently,
`
O
proofsareshowntobecompletewithrespect
tointuitionisticlogic.

4

1/0⇑`✻

❄✛`I

r/l✲⇑`✻

❄`O

Figure1:Completenessproofusinga“grandtour”throughlinearlogic

Acknowledgements:
WewishtothankAlexisSaurin,DavidBaelde,andKaustuvChaudhuriforhelpful
discussions.ThewritingofthispaperwasdonewhilethefirstauthorwasonsabbaticalleavefromHofstra
UniversitytoLIX/EcolePolytechnique.

5

2FocusedproofsinLinearlogic
WesummarizesomekeyconceptsandresultsfromAndreolipaperonfocusproofsforlinearlogic[And92].
A
literal
iseitheranatomicformulaorthelinearnegationofanatomicformula.Alinearlogicformula
isin
negationnormalform
ifitdoesnotcontainoccurrencesof
−◦
andifallnegationshaveatomicscope.If
K
isliteral,then
K

denotesitscomplement:inparticular,if
K
is
A

then
K

is
A
.
2.1Synchronousandasynchronousproofsearch
Connectivesinlinearlogiccanbeclassifiedaseither
asynchronous
or
synchronous
.Theasynchronous
connectivesare

,
.
,?,
>
,&,and

whilethesynchronousconnectivesaretheirdeMorgandual,namely,
1
,

,!,
0
,

,and

.Asynchronousconnectivesarethosewheretheright-introductionruleisalways
invertiblewhilethesynchronousconnectiveshaveright-introductionrulesthatarenotalwayinvertible.
Formally,aformulainnegationnormalformisofthreekinds:literal,asynchronous(meaningthatitstop-
levelconnectiveisanasynchronousconnective),andsynchronous(meaningthatitstop-levelconnectiveisa
synchronousconnective).
Inthe
focusingproofsystem
inFigure2,therearetwokindofsequents.InthesequentΨ:Δ

L
,the
“zones”ΨandΔaremultisetsand
L
isalist.Thissequentencodestheusualone-sidedsequent


,
Δ
,L
(here,weassumethenaturalcoercionoflistsintomultisets).Thissequentwillalsoalwayssatisfythe
invariantthatrequiresΔtocontainonlyliteralsandsynchronousformulas.InthesequentΨ:Δ

F
,Ψis
amultisetofformulasandΔisamultisetofliteralsandsynchronousformulas,while
F
isasingleformula.
Asynchronousphase
Ψ:Δ

L
Ψ:Δ

F,G,L
.
Ψ
,F


L
[

][][?]
Ψ:Δ
⇑⊥
,L
Ψ:Δ

F
.
G,L
Ψ:Δ

?
F,L
Ψ:Δ

F,L
Ψ:Δ

G,L
Ψ:Δ

B
[
y/x
]
,L
[
>
][&][

]
Ψ:Δ
⇑>
,L
Ψ:Δ

F
&
G,L
Ψ:Δ
⇑∀
x.B,L
Ψ:Δ
,F

L
[
R

]providedthatFisnotasynchronous
Ψ:Δ

F,L
Synchronousphase
Ψ:Δ
1

F
Ψ:Δ
2

G
Ψ:
∙⇑
F
[
1
][

][!]
Ψ:
∙⇓
1
Ψ:Δ
1
,
Δ
2

F

G
Ψ:
∙⇓
!
F
Ψ:Δ

F
1
Ψ:Δ

F
2
Ψ:Δ

B
[
t/x
]
[

l
][

r
][

]
Ψ:Δ

F
1

F
2
Ψ:Δ

F
1

F
2
Ψ:Δ
⇓∃
x.B
F⇑Δ:Ψ[
R

]providedthat
F
iseitherasynchronousoranegativeliteral
F⇓Δ:ΨIdentityandDeciderules
If
K
apositiveliteral:

[
I
1
]

[
I
2
]
Ψ:
K

K
Ψ
,K
:
∙⇓
K
Ψ:Δ

F
Ψ:Δ

F
If
F
isnotanegativeliteral:[
D
1
][
D
2
]
Ψ:Δ
,F
⇑∙
Ψ
,F

⇑∙
Figure2:ThefocusedproofsystemLLFforlinearlogic
Forconvenience,weshallrefertothefocusingproofsystemforlinearlogicas
LLF.
Intheoriginalpresentationofthisfocusingsystem[And92],atomsareconsidered“positive”andtheir

6

negations“negative.”ThiswasalsotheclssificationusedbyGirardforLC[Gir91].Itis,however,amore
generaltreatmenttoassignanarbitrary
polarity
or
bias
directlytoatoms(seefurtherdiscussionofthese
notionsattheendofthissection).Forintuitionisticlogicandtheintuitionisticrestrictionoflinearlogic
uponwhichmanycurrentsystemsarebased,assigningbiasdirectlytoatomsistheonlypossiblechoice.For
linearandclassicallogics,thisformulationisconsistentwiththeoriginalstyleofclassification.
ThusitistobeinterpretedthatLLFrequiresthattheatomsaredividedintotwosets:onefor
positive
atomsandtheotherfor
negative
atoms.Thispolarityofatomsisextendedinthenaturalwaytoliterals:
negatinganegativeatomyieldsapositiveliteralandnegatingapositiveatomyieldsanegativeliteral.
Itisimportanttoobservethatintheinitialrule,theliteralontherightmustbepositive.Thus,ifthe
literal
K
ispositive,thenΨ:
K


K
hasanimmediateproofusing[
I
1
],whilethesequentΨ:
K

K

can
onlybeprovedwithamoreinvolvedproof,namely
IΨ:
K


K
1
D1Ψ:
K

,K

⇑RΨ:
K

K

⇓RΨ:
K

K

I∙
:
c


c
1
D∙
:
c

,c

1
⇑R∙
:
c

c

⇓RI∙
:
b


b
1

:
c

c

⊗∙
:
c,b


b

c

D∙
:
b

c

,c,b

⇑∙
1
⇓RI∙
:
a


a
1

:
b

c

,c

b

b

bc

c
⊗∙
:
a

,b

c

,c

a

b

a

ab,b
−◦
c

c
D∙
:
a

,a

b

,b

c

,c
⇑∙
1
a,a
−◦
b,b
−◦
c

c
Figure3:Afocused,one-sidedsequentanditscorrespondingtwo-sidedform.
Thechoiceofpolarityforatomicformulashasaneffectontheshapeofafocusedproof.Considerproving
thelinearlogicformula
a
−◦
(
a
−◦
b
)
−◦
(
b
−◦
c
)
−◦
c
.Thisisprovableifandonlyifthetwo-sidedsequent
a,a
−◦
b,b
−◦
c

c
isprovable.Therearetwodifferentproofsofthissequentdependingontheorderin
whichthelinearimplicationsareintroduced.If
a
,
b
,and
c
arepositivethentheintroductionof
b
−◦
c
must
appearabovetheintroductionof
a
−◦
b
.Inparticular,Figure3containsthefocusedproofoftheone-sided
sequentandthecorrespondingproofoftheassociatedtwo-sidedsequent.If
a
,
b
,and
c
arenegativethen
thereisagainonefocusedproofanditcorrespondstoswitchingtheorderonintroducingtheseimplications.
TheproofsdisplayedinFigure3aresometimesreferredtoas“bottom-up”or“program-directed”:here,
onereasonsfromthe“(logic)program”,whichistheleft-handsideofthesequent,andattemptstomake
newlogicprograms(readingtheprooffromthebottom).Ontheotherhand,ifweswitchtheorderofthe
−◦
introduction,theresultingproofsaresometimesreferredtoas“top-down”or“goal-directed”:here,one
triestoprovethegoalimmediatelyandtoproducenewsub-goalsthatareattemptednext.Itwasobserved
in[Mil96]thatalloflinearlogiccouldbeseenasgoal-directedsearchifallatomicformulaswereassigneda
negativepolarity.
Changestothepolaritiesassignedtoatomsdoesnotaffectprovabilityofalinearlogicformula:instead
itaffectsthestructureoffocusedproofs.Thestructuringofcut-freeproofsisanunderlyingconcernofthis
paper.

7

2.2Assignmentofbias
Theterm“polarities”isusedintwodifferentbutrelatedways.Forthesakeofdiscussion,weshalluseforthe
momenttwotermstodistinguishthesetwosense.IntheworkonLU,Girardusedanotionofpolaritywith
thethreevaluesnegative,neutral,andpositive:thesewereusedtoindicatewhetherornotaformulacan
moveinandoutofdifferentzoneswithinsequents.Weshallsometimesrefertothisasthe“permeability”
ofaformulaandidentifynegativewith
rightpermeability
,positivewith
leftpermeability
,andneutralwith
non-permeability
.InSection6,wetakeourfirstexplicitlookatpermeability.Ourimmediateinteresthere
andinthenextseveralsectionsconcernstheclassificationofatoms(and,hence,literals)aspositiveand
negative.Forthesakeofclarity,weshallrefertothisdivisionas“bias”here.
Theassignmentofbiastoatomicformulaswithinfocusedproofsearchaffectstheshapeofproofsbut
nottheexistenceofproofs.Itseemsthatbiasforatomsexistsbecauseoftheneedoffocusingtoclassify
allsubformulaoccurrencesasbeingeithersynchronousorasynchronous.Apositivebiasliteralistreated
synchronously:inthe

-phase,encounteringapositiveliteralrequirestheprooftobecompletedimmediately:
nounfocusingoftheproofsearchisallowed.Conversely,anegativebiasliteralistreatedasynchronously:in
the

-phase,encounteringanegativeliteralrequirestheprooftolosefocus,evenifthecomplementofthe
literalisavailableinthecontext.
Thereappearstobeatleastthreewaystoassignbiastoatoms.
1.The
atom-based
approachassignsapolaritytoallatomsinafixedandglobalfashion.Thisassignment
doesnotneedtobestableundersubstitution.Thisstyleassignmentisusedin[And92].
2.The
predicate-based
approachassignsapolarityfirsttopredicatesymbols:atomstheninherenttheir
polarityfromthepredicatethatistheirhead.Suchassignmentisstableunderfirst-ordersubstitution.
AsweshallseeinSection5,the
λ
RCCproofsystemof[JNS05]canbeseenasusingthisstyleof
assignment.
3.The
proof-occurrence-based
approachassignspolaritiestoatomsbasedontheirlocationwithinproofs.
Twodifferentoccurrencesofthesameatomindifferent(conjunctive)branchesofaprooftreecan,
apparently,begivendifferentpolarities.Forexample,attemptingaproofof
−→
A

(
A

G
)willlead
toattemptingproofsoftwodifferentsequent,onefor
−→
A
andonefor
A
−→
G
.Theresultingtwo
occurrencesof
A
donotneedtohavethesamebiassincetheycannotinteract(viatheinitialrule,for
example).Infact,onemightwellwishtotreatthebiasofthesetwooccurrencesdifferently:ifthe
attempttoprove
G
resultsinattemptstoprove
A
,itmightbevaluabletoexpectthat
A
ispresentin
thecontextinsteadofallowingproofsearchtoreprove
A
(seethediscussiononmemo-izationinlogic
programmingin[Mil86]).
Inthisnote,wefollowthe
atom-based
approach,whichsubsumesthepredicate-basedapproach.
2.3Themeaningofbias
Onecouldsaythatthe“meaning”ofbiasistosimplyreducenon-determinisminthesearchforproof.A
betteranswermightbeusedtojustifythepredicate-basedassignmentscheme:predicatesarenon-logical
constantscanbeseenashigher-order(eigen-)variablesinahigher-orderlogic.Assuch,predicatescan
besubstitutedby
λ
-abstractedformulas.Suchananalysiswouldnaturallybebasedonlookingatfocused
proofsforlogicsinvolinghigher-orderquantifiers,whichweleaveforfuturework(seeSection10).
Ifapredicatethatisassignedapositivebiasisinstantiatedwithasynchronous(abstracted)formula,then
itshouldbethecasethatafocusedproofismappedtoanalmostfocusedproof(andduallyforinstantiating
anegativepredicatewithanasynchronousformula).
Anotherwaytoprovidemeaningtoan“unknown”predicateisviadefinitions,inthesenseof[Gir92,
SH93,MM00].Inthatapproach,predicatesareinterpretedasfixedpointdefinitions:duringproofsearch,
anatomicformulacanbeunfoldedaccordingtoitsdefinition.Insuchasetting,ifagivenpredicate
isinstantiatedwithasynchronousformula,thatatomwouldbeassignedapositivepolarity(duallyfor
asynchronousformulasandnegativepolarities).

8

Muchofourdebateonhowtoassignbiastoatomsandwhatbiasmightmean(apartfromproofsearch)
canbeavoidedifwecan,infact,avoidatomsentirely.Thenotionofdefinitionsmentionedaboveallowsfor
oneapproachtoavoidingatoms:atomsaresimplyexpressionsthatdonotrefertothemselvesbuttotheir
meaning.Ifsuchunfoldingscanbeguaranteedtobenoetherian,thenoneneedsnoinstancesoftheinitial
rule.AmoreextremesituationmightbetheonetakeninLudicsbyGirard:thereformulasarereplaced
bystructureswithwhichoneinteractstoarbitrarydepth[Gir01].Thestructurescorrespondingtoformulas
arenotbuiltfromatomsatall.
Giventhisdiscussionaboutbiasabove,weadoptthefollowingusesoftheterm“polarity”inthisreport.
Inlinearlogic,thenotionof
asynchronous
and
synchronous
areusedfornon-atomicformulas.Thenotion
ofbiasisusedforatomicformulas.Weshalldescribeaformulaasbeingof
positivepolarity
ifitiseithera
non-atomicsynchronousformulaorapositivebiasatom.Weshalldescribeaformulaasbeingof
negative
polarity
ifitiseitheranon-atomicasynchronousformulaoranegativebiasatom.Inintuitionisticlogic,
thenotionofpositivepolaritywillbeequatedtoleftpermeability:weshallalsoassignallpositivebias
atomstothisclass.Negativepolaritywillbeidentifiedwithnon-permeableformulas,whichwillalways
includethenegativebiasatoms.Similarly,inclassicallogic,thenotionofpositivepolaritywillbeequated
toleftpermeability:weshallalsoassignallpositivebiasatomstothisclass.Negativepolaritywillbe
identifiedwithright-permeableformulasandtheseformulasalwaysincludethenegativebiasatoms.These
classificationsarefurtherexplainedinSection6.2.

9

01BBBAAAtrue
1
>
false
1
0
100
0
0

0
⊥⊥
PP
∨∧
QQ
!!(
PP
1

&!
QQ
)
1
!!
PP
0
&

!!
QQ
0
==((??((
PP
0
))


&??((
QQ
0
))

))

P

Q
!(!
P
0
−◦
Q
1
)=!(?(
P
0
)

.
Q
1
)!
P
1
−◦
!
Q
0
=(!
P
1

?
Q
0

)

¬
P
!(!
P
0
−◦
0)=!(0
.
?(
P
0
)

)!
P
1
−◦
0=(!
P
1
⊗>
)


xP

x
!
P
1

x
!
P
0
=(

x
?(
P
0
)

)


xP
!

xP
1

x
!
P
0
=(

x
?(
P
0
)

)

Table1:The0/1translationusedtoencodeLJproofsintolinearlogic.

3TranslatingLJProofs
Aprincipalaimofthispaperistoshowthatfocusinginlinearlogiccanbeusedtoderivesystemsinlogics
thatlinearlogicisdesignedtoembed.OurfirsttaskistoshowthatarbitraryLJproofscanbemirrored
asfocusedproofswiththeappropriatetranslationtolinearlogic.Focusingyieldsafinedegreeofcontrol
overproofsearch,
including
thefreedomtoloosedeterministicbehavior.Moresignificantly,however,our
translationwillbeusedasananchorforfuturetranslations.Itwillserveasakeylinktointuitionistic
provability,andallowcompletenesstheoremsforvariousintuitionisticsystemstobeprovedviaa“grand
tour”throughlinearlogic.
The“0
/
1”translationgiveninTable1isour
sourcetranslation
forintuitionisticlogic,definedonformulas
oftheforms
true
|
false
|
A
|
P

Q
|
P

Q
|
P

Q
|∃
xP
|∀
xP

P
where
A
representsatomicformulas.Fortheconvenienceofmovingbetweenone-andtwo-sidedsequents,
wedisplaythedualofmostoftheformulasinthe
B
0
column.Thetwo-sidedintuitionisticsequentΓ
`
I
G
istranslatedintothetwo-sidedlinearlogicsequent!Γ
0
`
LL
G
1
andtheone-sidedlinearlogicsequent
`
LL
?(Γ
0
)

,G
1
.Here,wefollowtheusualconventionofapplyingexponentials,negations,andtranslations
tosetsandmultisetofformulas:forexample,!Γ
0
=
{
!
D
0
|
D

Γ
}
.
ReadersfamiliarwithGirard’soriginaltranslation[Gir87]ortheHodas-Millertranslationin[HM94]may
beconcernedwiththeprolificuseoftheexponential!intheabovetranslation.Indeed,ifweareinterested
onlyinpreserving
provability,
thenmostoftheseexponentialareunnecessary.However,ourinterestlies
alsoinpreservingthestructureof
proofs,
notjustinthetraditionalpresentationoflinearlogicbutalsoin
thefocusingcalculusLLF.Usingtheterminologyof[DJS95]weseek
inductivedecorationstrategies
:
i.e.
,we
wishtodefineone-to-onemappingsbetweenfocusedproofsandunrestrictedLJproofs.
Weshallsoonconsiderothertranslationsofintuitionisticlogicintolinearlogicthatstrengthenthe0/1-
translationalongthefollowing,inter-relateditems.
1.Various!’scanbedropped:forexample,
P

Q
canbetranslatedusingthepatterns!
P
−◦
!
Q
,
P
−◦
!
Q
,
or
P
−◦
Q
.
2.Intheabovetranslation,thepolarityofatomsisirrelevant:intranslationswithfewerexponentials,
thepolarityofatomscanplayanimportantrole.
3.Theintuitionisticconjunctionismappedtotheadditiveconjunction&.Othertranslationscanusethe
multiplicativeconjunction

.The&providesonly“partofthestory”oftheintuitionisticconjunction.
The0/1-translationplaces!infrontofasynchronousconnectivesontheright-handsidefortwopurposes.
First,the!stopsallright-sideformulasfrombeingtreatedasynchronously:inparticular,noformulais
decomposeduntilselectedbya“decide”inferencerule.Inthisway,wecanmaparbitraryLJproofs,which
havenofocusingdiscipline,intofocusedproofs.Itshouldbeobserved,however,thatinsteadofusing!
B

01