[PDF] Binary positivity in the language of locales

View - Download Binary positivity in the language of locales

Previous PDF

Next PDF

Binary positivityin the language of locales

Francesco CirauloDepartment of Mathematics

University of Padua

4 thWorkshop on Formal Topology

June 15-20 2012, Ljubljana

Francesco Ciraulo(Padua)Binary positivityin the language of locales4 WFTop- Ljubljana, June 15-20 20121 / 29

About this talk

1987

G. Sambin & P .Ma rtin-Lof

formal topology= predicative version of a locale = \locale with base" today

G. Sambin

POSITIVE topology= formal topology +

a BINARY POSITIVITY PREDICATE What does a binary positivitypredicate correspond to in the languages of locales? a fo rmaltop ology

IS TO a

lo cale AS a

POSITIVE t opology

IS TO a

lo cale

Answer:

a suitable system of overt, weakly closedsublocales

Francesco Ciraulo(Padua)Binary positivityin the language of locales4 WFTop- Ljubljana, June 15-20 20122 / 29

Locales with bases

A base for a localeLis a subsetS Ls.t. x=Wfa2Sjaxg (for everyxinL)

PutaCUdef:()aWU

(fora2SandUS) so thatfa2SjaCUg=WU (formal opensubset ) (any element ofL)

Formal topologycorresponding toL (S;C)

Formal topology

axiomatization of ( S;C) Overt lo cale = fo rmaltop ology+ una ryp ositivitypredicate = (S;C;Pos)Pos(a)()\9L(a) = 1"

Francesco Ciraulo(Padua)Binary positivityin the language of locales4 WFTop- Ljubljana, June 15-20 20123 / 29

Positive topologies (

locales z}|{ formal topologies+bina ryp ositivity) localez}|{

S;C;n)binary positivity

nSPow(S) anUa2U+anUU VanV+anUanfb2SjbnUg+ aWUz}|{ aCUa nV(9u2U)(unV)(compatibility) fa2SjanUg \formal closed"subset FormalClosed(n)def=fformal closed subsets w:r:t:ng

Francesco Ciraulo(Padua)Binary positivityin the language of locales4 WFTop- Ljubljana, June 15-20 20124 / 29

Two notions of closure

Intuitionistically,

TW O dierent w aysof dening closure for a subspaceYof a topological space:

int(Y)= the complem entof the in teriorof the complement of Xcl(Y)= the set of adherent p ointsof Xcl(Y) int(Y)and so Y=int(Y)= )Y=cl(Y)

but NOT the other way round(counterexample: discrete topology).

Francesco Ciraulo(Padua)Binary positivityin the language of locales4 WFTop- Ljubljana, June 15-20 20125 / 29

Example: positivities on a topological space

(X;) topological space Sbase Forxa point,xdef=fa2Sjx2ag= basic open neighbourhoods ofx.

U7! fx2XjxUg

fa2SjaGDg [DSambin

0s notation for inhabited intersection

More generally:For every subsetYX, the relation

anYUdef()(9y2Y)(a2yU) is apositivityand

FormalClosed(nY)=fclosed sets in the subspace topology on Yg.Francesco Ciraulo(Padua)Binary positivityin the language of locales4 WFTop- Ljubljana, June 15-20 20126 / 29

On the lattice of positivities

Llocale

SbasePosty(L)def= all positivities onL(w.r.t.S).Posty(L) is ordered by INCLUSION: n

1n2def()(8a2S;8US)(an1U)an2U)Posty(L) is a SUPLATTICE with:aW

iniU() 9i(aniU)

SoPosty(L) has:

MINIMUManminU()falsum

MAXIMUManmaxU()anUfor some positivityn(a more explicit characterization below)

Francesco Ciraulo(Padua)Binary positivityin the language of locales4 WFTop- Ljubljana, June 15-20 20127 / 29

Splitting subsets & suplattice morphisms

(completely-prime up-sets & sup-preserving maps)

Z LissplittingifxWY x2ZYGZ, that is, (WY)2Z()YGZ

for everyfxg [Y L. Let us putSplit(L)def=fsplitting subsets ofLg.Facts: 1 Split(L);Sis a suplattice;2there exists an isomorphism of suplattices

Split(L)=SupLat(L;

Z7![x7! f jx2Zg]

1(fg) ['

where =Pow(fg) is the frame of truth values.Examples: points,Pos.

Francesco Ciraulo(Padua)Binary positivityin the language of locales4 WFTop- Ljubljana, June 15-20 20128 / 29

FormalClosed(n),!Split(L)=SupLat(L;

)Thanks tocompatibility...FormalClosed(n),!Split(L)

U7! "U=fx2 L juxfor someu2Ug

fa2SjanUg 7!f x2 L j(9a2S)(axandanU)gis a sub-suplatticeofSplit(L)(w.r.t. union)

FormalClosed(n),!SupLat(L;

fa2SjanUg 7![x7! f j(9a2S)(axandanU)g]is a sub-suplatticeofSupLat(L;

)Francesco Ciraulo(Padua)Binary positivityin the language of locales4 WFTop- Ljubljana, June 15-20 20129 / 29

Positivities AS sub-suplattices ofSplit(L)

A base-independent description of positivities

LlocaleFor each baseSofL, the following denes a BIJECTION between

Posty(L) w.r.t.Sandfsub-suplattices ofSplit(L)g

n7! f"UjU2FormalClosed(n)g anFUdef()(9Z2F)(a2Z\SU) [F

Note:FormalClosed(nF) =fZ\SjZ2Fg=FCorollaries

ForS1;S2bases ofL:Posty(L)w.r.t.S1=Posty(L)w.r.t.S2.For everynone has:n=nFormalClosed(n), that is,

anU()a2ZUfor someZ2FormalClosed(n)Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201210 / 29

Thegreatest p ositivitynmaxin terms ofsplitting subsets

In the previous isomorphism

Posty(L)=fsub-suplattices ofSplit(L)g

n maxcorresponds toSplit (L) so anmaxU()9Z2Split(L)a2Z\SU and FormalClosed(nmax) =fZ\SjZ2Split(L)g=Split(L)Constructively... IfL= (S;C) isinductively generated, thennmaxis generated bycoinduction.

(Martin-Lof & Sambin -Generating Positivity by Coinduction)Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201211 / 29

Formal closed subsets AS ...

Bunge & Funk,Constructive Theory of the Lower Power Locale,MSCS6 (1996)

Points of the lower powerlocale

=overt,w eaklyclosed sublo calesof L =suplattice morphismsL ! =Pow(fg) =splitting subsetsof L n2Posty(L)FormalClosed(n) =FormalClosed(nmax) See also Spitters,Locatedness and overt sublocales,APAL162 (2010) and Vickers,Constructive points of powerlocales,Math.Proc.CambridgePhilos.Soc.122 (1997)

Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201212 / 29

Weakly closed sublocales

See Vickers,Sublocales in Formal Topology,JSL72 (2007) and Johnstone'sElephantfor the more general notion ofbrewise closed.

A weakly closedsublocale of (S;C) is onegenerated as follo ws1for eacha2Sx a (possibly empty) setI(a) of PROPOSITIONS;2fora2SandP2I(a) impose the EXTRA conditionaCfx2SjPg.

CLASSICALLY: this is just a closedsublocale.

Warning

In the spatial case,cl(Y) need not be weakly closed!Weakly closed sublocales are closed under binary joins. (Johnstone)

IffYXjcl(Y) =Ygis closed under binary unions, then LLPO. (Bridges)

Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201213 / 29

Overt, weakly closed sublocales

(S;C0),!(S;C) is weakly closedANDovert IFF there existsP2SupLat(L; )=Split(L) s.t. C

0can be generated by imposing the EXTRA axiomsaC0fx2SjP(a) = 1g, or equivalentlyaC0fag \P, for alla2S.

Pis the unary positivity predicateof (S;C0).Fact:

point of (S;C0) = point of (S;C) s.t. all its basic neighbourhoods are inPFrancesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201214 / 29

Formal closed subsets AS overt weakly-closed sublocales

Given (S;C;n) positive topology

andU=fx2SjxnUg(formal closed subset)"Usplitting subsetx7! f jx2("U)gsuplattice morphismL ! overt, weakly closedsublo cale generated by imposingaCfag \U with UNARY positivity given by ( )nU.

This is the smallest sublocale for which

( )nUis a unary positivity predicate. Its pointsare the points of (S;C) which are \contained" inU.

Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201215 / 29

Positivities AS ...

A fo rmalclos edsubset of L= (S;C) is......fa2SjanUgfor someUSand somen2Posty(L) ...fa2SjanmaxUgfor someUS ...S\Zfor someZ2Split(L) ...S\'1(1) for some'2SupLat(L; ...fa2SjPos(a)gfor some (S;C0;Pos),!(S;C)|{z} overt and weakly closedAp ositivityon a lo caleLis......a suplattice of 8 :splitting subsets ofL suplattice morphisms fromLto overt;weakly closed sublocales ofLand n max=Split(L)=SupLat(L; )=fovert, weakly closed sublocales ofLg

Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201216 / 29

Morphisms between positive topologies

A morphismf: (L

1z}|{ S

1;C1;n1)!(L

2z}|{ S

2;C2;n2) isa morphismf:L1! L2oflocales

(with fthe corresponding morphism of frames in the opposite direction)such that: a f(b) an1U =)bn2y2S2j 9u2U:u f(y)|{z} f(y)2"Ug for alla2US1andb2S2.?!?

Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201217 / 29

Positive topology= ( L;), with

La localeand

,!SupLat(L;

Given (L1;1), (L2;2) andf:L1! L2inLoc

TFAE1fis a morphism of positive topologies;2the mapU7!S2\( f)1("U) maps formal closed of (L2;2) to formal closed of (L1;1);3( f)1maps elements ofSplit(L1) corresponding to 1 to elements ofSplit(L2) corresponding to 2;4(8'21)(' f22), that is, 1 f2. ' L1]21[ ' L1 f L2]22

Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201218 / 29

The categoryPTopof Positive TopologiesObjects(L;F)(L;)Llocale+binary positivityF,!Split(L),!SupLat(L;

)Morphismsf:L1! L2of locales s.t.( f)1[F1]F2 1

f2Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201219 / 29

EmbeddingLocintoPTop

PTop (L1;1);(L2;2)=ff2Loc(L1;L2)j1 f2gLoc(L;L0)=PTop(L;);(L0;max)for every ,!SupLat(L; )SupLat(L0;

By identifyingLwith

L; maxz}|{

SupLat(L;

), we get:Loc,!PTop.

Fact:Locis a re

ectivesubcategory ofPTop.

Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201220 / 29

Pointsof a positive topologies

Def: a pointof (S;C;n) is...

...a point of (S;C) which \belongs" toFormalClosed(n) i.e. a point whose set of basic neighbourhoods belongs toFormalClosed(n).

Points(L;)=Points(L)\=Frame(L;

)\=f'2j'preserves nite meetsg =PTop1;(L;)where1= terminal object ofPTop= terminal locale + max

Idea: a positivity isa way for selecting points.

Sambin & Trentinaglia,On the meaning of positivity relations...,J.UCS11 (2005)

Note that:Points(L;max) =PointsL;SupLat(L;

)=Points(L).

Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201221 / 29

One formal closed subset, three positive topologies

Let (S;C;n) be a positive topology.

For anyH2FormalClosed(n) one can construct:1an overt, weakly closed sublocale (S;CH) by adding the extra axiom schemaaCfag \H (Hacts as the unary positivity predicate)2another positivitynHdened by:anHUdef()anH\U (j.w.w. G. Sambin and M. Maietti)

And one can show that:

Pt(S;CH) =Pt(S;CH;nH) =f2Pt(S;C)j1(>)\SHg

=Pt(S;C;nH)this is PREDICATIVE (even whenCis not generated)

Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201222 / 29

Two adjunctions betweenTopandPTop1Extending the usual adjunction betweenTopandLoc:

Top Loc PTop

X7! X7!( X;n max)Pt(L) [L [(L;)2A new adjunction:

Top PTop

X7!( X;n

X)Pt(L;) [(L;)

Recall thatanXU()(9x2X)(a2xU) wherex= basic neighbourhoods ofx.CLASSICALLY: nX=nmaxand soPt(

X;nX) =Pt(

X;nmax)=Pt(

X).

Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201223 / 29

Two notions of sobriety

points = Pt(

X) =Pt(

X;nmax)

\strong" points = Pt( X;nX) 2Pt( X) is \strong" if for alla2, there existsx2Xs.t.a2x. soberX=Pt(

X;nmax)

weak soberX=Pt(

X;nX)IfXisT2, thenXis weakly sober.

On the contrary, if \T2)sober" were true, then LPO would hold. Fourman & Scott,Sheaves and Logic, inApplications of sheaves,LNM753 (1979) Aczel & Fox,Separation properties in constructive topology,OLG48 (2005)

Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201224 / 29

Spatiality for positive topologies

A positive topology (L;n) is (bi-)spatialif

(L;n) =

Pt(L;n);nPt(L;n)

that requires TWO things:1L= Pt(L;n) (stronger than usual spatiality)2n=nPt(L;n)(\reducibility")1 By unfolding denitions:1xyIFF82Pt(L)\(x)(y)2anUIFF92Pt(L;n)a21(>)\SU i.e. coincides with its sub-suplattice spanned byPt(L)\.1

Rinaldi, Sambin and Schuster have a joint work in progress about reducibility in Ring Theory.Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201225 / 29

Positivity relations on suplattices

The notion of abinary positivity predicatemakes sense also for the category

SupLatof suplattices and sup-preserving maps.

basic topology= suplatticeL+ positivity ,!SupLat(L; See C. & Sambin,A constructive Galois connection between closure and interior,JSL, to appear and my talk in Kanazawa 2010. As before, every suplatticeLcan be identied with the basic topology (L;max).

Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201226 / 29

Positivity on topoi (?)

Future work (?)

By adopting the view of TOPOI as generalized spaces...

Llocale Etopos

Set '2SupLat(L; ) functor fromEtoSetthat preserves colimits Aim:to obtain a PREDICATIVE account of some Topos Theory (e.g. ofclosedsubtopoi).

Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201227 / 29

References

1P. Aczel and C. Fox,Separation properties in constructive topology, inFrom sets and types

to topology and analysis,Oxford Logic Guides48 (2005), pp. 176-192.2M. Bunge and J. Funk,Constructive Theory of the Lower Power Locale,Mathematical

Structures in Computer Science6 (1996), pp. 69-83.3F. Ciraulo and G. Sambin,A constructive Galois connection between closure and interior,

Journal of Symbolic Logic, to appear (arXiv:1101.5896v2).4M. P. Fourman and D. S. Scott,Sheaves and Logic, inApplications of sheaves,Lecture

Notes in Mathematics753 (1979), pp. 302-401.5P. T. Johnstone,Sketches of an elephant: a topos theory compendium,Oxford Logic

Guides43-44 (2002).6P. Martin-Lof and G. Sambin,Generating Positivity by Coinduction, in Sambin's book.7G. Sambin and G. Trentinaglia,On the meaning of positivity relations for regular formal

spaces,Journal of Universal Computer Science11 (2005), pp. 2056-2062.8B. Spitters,Locatedness and overt sublocales,Annals of Pure and Applied Logic162

(2010), pp. 36-54.9S. Vickers,Constructive points of powerlocales,Mathematical Proceedings of the

Cambridge Philosophical Society122 (1997), pp. 207-222.10S. Vickers,Sublocales in Formal Topology,Journal of Symbolic Logic72 (2007), pp.

463-482.

Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201228 / 29

Najlepsa hvala! Thank you very much!

Francesco Ciraulo(Padua)Binary positivityin the language of locales4WFT op- Ljubljana, June 15-20 201229 / 29

quotesdbs_dbs14.pdfusesText_20

[PDF] languages in automata theory

[PDF] languages in discrete mathematics

[PDF] languages in south korea

[PDF] langue and parole ignou

[PDF] langue and parole in linguistics with examples

[PDF] langue and parole meaning in hindi

[PDF] langue and parole pdf

[PDF] langue and parole short notes

[PDF] langue des gitan d'espagne 4 lettres

[PDF] langue des signes québécoise (lsq)

[PDF] langue des signes québécoise alphabet

[PDF] langue des signes québécoise dictionnaire

[PDF] langue des signes québécoise gatineau

[PDF] langue elfique traduire

[PDF] langue en pays zoulou