August 2016 - Categories - categories.org.au

Free access to Logica Universalis and Studies in Universal Logic
by Universal Logic 29 Aug '16

29 Aug '16

For a limited period of time there is free access to all the issues of Logica Universalis http://link.springer.com/journal/volumesAndIssues/11787 in particular to the latest Issue Volume 10, Issue 2-3, June 2016 Special Issue: The Vatican Square http://link.springer.com/journal/11787/10/2/page/1 And to the following volumes of the book series Studies in Universal Logic: The Road to Universal Logic Festschrift for 50th Birthday of Jean-Yves B??ziau Volume I Editors: Arnold Koslow, Arthur Buchsbaum http://link.springer.com/book/10.1007%2F978-3-319-10193-4 The Road to Universal Logic Festschrift for the 50th Birthday of Jean-Yves B??ziau Volume II Editors: Arnold Koslow, Arthur Buchsbaum http://link.springer.com/book/10.1007%2F978-3-319-15368-1 The Life and Work of Leon Henkin Essays on His Contributions Editors: Mar??a Manzano, Ildik?? Sain, Enrique Alonso http://link.springer.com/book/10.1007%2F978-3-319-09719-0 Around and Beyond the Square of Opposition Editors: Jean-Yves B??ziau, Dale Jacquette http://link.springer.com/book/10.1007/978-3-0348-0379-3 Visual Reasoning with Diagrams Editors: Amirouche Moktefi, Sun-Joo Shin http://link.springer.com/book/10.1007/978-3-0348-0600-8 Kripke???s Worlds An Introduction to Modal Logics via Tableaux Authors: Olivier Gasquet, Andreas Herzig, Bilal Said, Fran??ois Schwarzentruber http://link.springer.com/book/10.1007%2F978-3-7643-8504-0 Institution-independent Model Theory Authors: Razvan Diaconescu http://link.springer.com/book/10.1007/978-3-7643-8708-2 Logica Universalis Towards a General Theory of Logic Editors: Jean-Yves Beziau http://link.springer.com/book/10.1007%2Fb137041 Towards a General Theory of Classifications Authors: Daniel Parrochia, Pierre Neuville http://link.springer.com/book/10.1007%2F978-3-0348-0609-1 Modern Logic 1850-1950, East and West Editors: Francine F. Abeles, Mark E. Fuller http://link.springer.com/book/10.1007/978-3-319-24756-4 Completeness Theory for Propositional Logics Authors: Witold A. Pogorzelski, Piotr Wojtylak http://link.springer.com/book/10.1007%2F978-3-7643-8518-7 Towards an Arithmetical Logic The Arithmetical Foundations of Logic http://link.springer.com/book/10.1007/978-3-319-22087-1 And also: New Directions in Paraconsistent Logic 5th WCP, Kolkata, India, February 2014 Editors: Jean-Yves Beziau, Mihir Chakraborty, Soma Dutta http://link.springer.com/book/10.1007/978-81-322-2719-9 Enjoy! >-------------------------------------------------------------------------> Jean-Yves Beziau Editor-in-Chief Logica Universalis http://link.springer.com/journal/11787 Studies in Universal Logic http://www.springer.com/series/7391 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Re: Examples of certain monotone operators
by Mamuka Jibladze 26 Aug '16

26 Aug '16

> Note that (9) is the only place where monotonicity is used. > I wonder whether it could be actually deduced from the rest. As I mentioned in a subsequent message, this is actually not the only place where I had to use monotonicity. Now I realized that monotonicity cannot be deduced from f(fp -> p) without additional assumptions. Consider fp = (p or not p); then f(fp -> p) = (not p or not not p), so that f(fp -> p) holds iff the topos is de Morgan, whereas f is monotone iff the topos is Boolean (since f0 = 1). >> >> Dear all, >> >> I have come accross a certain kind of operators, and I wonder if they >> have a name or have been encountered before. >> >> We work internally in a topos with a subobject classifier ??. For the >> purposes of this discussion, call a monotone map f : ?? ??? ?? *good* if >> >> (*) ??? p : ??, f (f p ??? p) >> >> is valid in the topos. >> >> Some examples of good maps are: >> >> 1. The identity map. >> 2. The double negation map. >> 3. For any q ??? ??, the j-operator p ??? (q ??? p). >> >> Is the condition (*) known? Can you think of other examples of good >> maps (perhaps in specific toposes)? >> >> I have so far just one connection: in provability logic condition (*) >> appears (without the universal quantifier) as the antecedent of L??b's >> theorem, which sttates that ??? (??? p ??? p) ??? ??? p. >> >> With kind regards, >> >> Andrej [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Re: Examples of certain monotone operators: errata
by Mamuka Jibladze 26 Aug '16

26 Aug '16

There are some problems with my previous post, sorry > (1) q -> fp = f(q -> p) ; in particular, f is inflationary. > This has been pointed out by Ingo Blechschmidt Actually inflationarity does not follow from this directly, (1) only gives q -> fq = f1 To show f1 = 1 use f(fp -> p) with p = 1 > (7) q -> fp = q -> f(q & p): > by (1) both are equal to f(q -> p) = f(q -> (q & p)) > > > (8) fq & fp -> f(q & p): > in (7), take fq & fp in place of q, > then the lhs of (7) becomes true lhs indeed becomes true but the rhs is not yet what we want, it is (fq & fp) -> f(fq & fp & p) = f(fq & p). To finalize, f(fq & p) -> f(q & p) has to be proved, and here it seems I cannot get away without another use of monotonicity: from fq & p -> f(q & p) it gives f(fq & p) -> ff(q & p) and then one can use (6). As for fq & p -> f(q & p), it is obtained from (7) as explained in the last remark of my previous post. Mamuka [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Re: Examples of certain monotone operators
by Mamuka Jibladze 26 Aug '16

26 Aug '16

> Date: Mon, 15 Aug 2016 17:05:50 -0300 > From: Andrej Bauer <andrej.bauer(a)andrej.com> > To: categories list <categories(a)mta.ca> > Subject: categories: Examples of certain monotone operators Here is (I hope) a proof that such map is a (sub-open) nucleus. (1) q -> fp = f(q -> p) ; in particular, f is inflationary. This has been pointed out by Ingo Blechschmidt (2) (fp -> p) -> p = fp: reasoning "inside Omega" this is almost trivial - if fp -> p is p, then f(fp -> p) is fp (3) (fp -> p) -> fp = (fp -> p) -> p: (fp -> p) -> fp = [(fp -> p) -> fp] & [(fp -> p) -> (fp -> p)] = (fp -> p) -> [fp & (fp -> p)] = (fp -> p) -> [fp & p] = (fp -> p) -> p (this only required inflationarity of f, at the last step) (4) (fp -> p) -> fp = f((fp -> p) -> p): this is a particular case of (1) (with fp -> p in place of q) (5) (fp -> p) -> p = f((fp -> p) -> p): this follows from (3) and (4) (6) fp = ffp: this follows from (2) and (5) (7) q -> fp = q -> f(q & p): by (1) both are equal to f(q -> p) = f(q -> (q & p)) (8) fq & fp -> f(q & p): in (7), take fq & fp in place of q, then the lhs of (7) becomes true (9) f(q & p) -> fq & fp: monotonicity So f is inflationary, idempotent (6) and multiplicative (8-9). Note that (9) is the only place where monotonicity is used. I wonder whether it could be actually deduced from the rest. I think I have seen in a paper by Anders Kock that any idempotent prenucleus on Omega is a nucleus; and it follows easily (without monotonicity) that q & fp = fq & fp - just apply q & _ to both sides of (7). Glad I'm back, Mamuka > > Dear all, > > I have come accross a certain kind of operators, and I wonder if they > have a name or have been encountered before. > > We work internally in a topos with a subobject classifier ??. For the > purposes of this discussion, call a monotone map f : ?? ??? ?? *good* if > > (*) ??? p : ??, f (f p ??? p) > > is valid in the topos. > > Some examples of good maps are: > > 1. The identity map. > 2. The double negation map. > 3. For any q ??? ??, the j-operator p ??? (q ??? p). > > Is the condition (*) known? Can you think of other examples of good > maps (perhaps in specific toposes)? > > I have so far just one connection: in provability logic condition (*) > appears (without the universal quantifier) as the antecedent of L??b's > theorem, which sttates that ??? (??? p ??? p) ??? ??? p. > > With kind regards, > > Andrej [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Re: Examples of certain monotone operators
by Tadeusz Litak 22 Aug '16

22 Aug '16

As a PS to my last email: I've been thinking more about the last point, i.e., whether []([]A -> A) indeed captures an inhabitation law shared by both comonadic and most monadic operators. It is not really the case. For normal comonadic ones, it trivially holds, as I discussed before. But I realized that monadic examples already mentioned by Andrej are rather special. Without going into the full generality of monads on aribitrary categories, it's enough to have a look at the building blocks of nuclei on a frame. Harold Simmons denotes these as u_a(x) := a \vee x v_a(x) := a -> x w_a(x) := (x -> a) -> a As Andrej noticed in his third example, v_a(v_a(x) -> x) = \top for any a. w_a generalizes double negation, so with a = \bot it turns into Andrej's second example. But for other a, it is not in general not true that w_a(w_a(x) -> x) = \top. Just consider the three-element Heyting algebra, call the middle element * and note that w_*(w_*(\bot) -> \bot) = * And u_a(u_a(x) -> x) = \top can be also refuted in the three-element Heyting algebra. So if one wants f to be monadic, one cannot generalize Andrej's examples too much. On 18/08/16 14:07, Tadeusz Litak wrote: > Dear Andrej, > > as you mentioned modal logic, here are three modal cents. > > All the examples you mention are not only monotone, but also are what modal logicians would call "normal boxes" or > "dual operators", i.e., the satisfy the law > > f (A -> B) -> f A -> f B > > and the "necessitation" or "G??del" rule > A/ f A > > Is it actually, intended that these laws should hold? > > (Actually, all your examples also satisfy the inflationary law A -> f A, which is commonly thought to be more > typical of "diamonds" or "operators", which led some researchers to, e.g., reconstruct such beasts in terms of > combinations of boxes an diamonds. But from my point of view, as long as you satisfy the normality laws, you're a > perfectly good box). > > At any rate, when one is talking about normal boxes, your law []([]A -> A) holds in all extensions of the modal logic > T: the modal logic of reflexive relations, axiomatized by []A -> A, i.e., a "deboxed" variant of your formula. This is > obviously thanks to that "necessitation" or "G??del" rule. > > Your axiom even has what modal logicians call a "local" FO counterpart, i.e., a first-order formula \phi(x), which is > satisfied by a given point in a Kripke structure iff the original modal formula holds at that point under all > valuations. This formula is "all successors are reflexive", i.e., > > \forall y. (x R y -> y R y) > > (I'm omitting here correspondence for intuitionistic modal logics, but can do it in another mail if you care. It isn't > much more complicated than that) > > This means that your axiom holds in many typical modal logics, esp. S4 a.k.a. the "comonadic" logic or the logic of > Kuratowski's interior operator or the logic of all (finite) preorders or the logic of partial orders. Extensions of > S4, in turn, include the Grzegorczyk logic of all finite partial orders/finite trees or S5, the logic of all (finite) > equivalence relations. > > On the other hand, the L??b axiom is a wrong route to go in your case. Adding your axiom to the L??b logic would > trivialize the box into the "verum" operator: []A would be true for every A. In the provability setting, one sometimes > adds (following Solovay) []A -> A to the L??b system, but even then one is not closing under necessitation. > > What is more curious, though, is that all your examples are monadic in nature, whereas the T axiom and its extensions > have "comonadic" character. I've never realized that an axiom like yours can provide a common ground for both; nice! > > HTH, best, > t. > > > > On 15/08/16 22:05, Andrej Bauer wrote: >> Dear all, >> >> I have come accross a certain kind of operators, and I wonder if they >> have a name or have been encountered before. >> >> We work internally in a topos with a subobject classifier ??. For the >> purposes of this discussion, call a monotone map f : ?? ??? ?? *good* if >> >> (*) ??? p : ??, f (f p ??? p) >> >> is valid in the topos. >> >> Some examples of good maps are: >> >> 1. The identity map. >> 2. The double negation map. >> 3. For any q ??? ??, the j-operator p ??? (q ??? p). >> >> Is the condition (*) known? Can you think of other examples of good >> maps (perhaps in specific toposes)? >> >> I have so far just one connection: in provability logic condition (*) >> appears (without the universal quantifier) as the antecedent of L??b's >> theorem, which sttates that ??? (??? p ??? p) ??? ??? p. >> >> With kind regards, >> >> Andrej >> >> >> [For admin and other information see: http://www.mta.ca/~cat-dist/ ] > [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Examples of certain monotone operators
by Andrej Bauer 18 Aug '16

18 Aug '16

Dear all, I have come accross a certain kind of operators, and I wonder if they have a name or have been encountered before. We work internally in a topos with a subobject classifier Ω. For the purposes of this discussion, call a monotone map f : Ω → Ω *good* if (*) ∀ p : Ω, f (f p ⇒ p) is valid in the topos. Some examples of good maps are: 1. The identity map. 2. The double negation map. 3. For any q ∈ Ω, the j-operator p ↦ (q ⇒ p). Is the condition (*) known? Can you think of other examples of good maps (perhaps in specific toposes)? I have so far just one connection: in provability logic condition (*) appears (without the universal quantifier) as the antecedent of Löb's theorem, which sttates that □ (□ p ⇒ p) ⇒ □ p. With kind regards, Andrej [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

4 3

CSR 2017: Preliminary Call for Papers
by Edward A. Hirsch 18 Aug '16

18 Aug '16

Preliminary Call for Papers The 12th International Computer Science Symposium in Russia, CSR-2017 Kazan, Russia June 8-12, 2017 http://logic.pdmi.ras.ru/csr2017/ --------------------------------- CSR is an annual conference that intends to reflect the broad scope of international cooperation in computer science. The topics covered vary from year to year, but in general try to cover as much of the contemporary computer science as possible. They include, but are not limited to: algorithms and data structures combinatorial optimization constraint solving computational complexity cryptography combinatorics in computer science formal languages and automata algorithms for concurrent and distributed systems, networks applications of logic to computer science, e.g. proof theory, model checking and verification formal and algorithmic aspects of bio-informatics current challenges such as quantum computing --------------------------------- Important dates Deadline for submissions: December 15, 2016 (23:59 anywhere on Earth). Notification of acceptance: February 15, 2017. Conference dates: June 8-12, 2017. --------------------------------- Distinguished opening lecture and invited lectures TBA --------------------------------- Submission and publication Authors are invited to submit papers presenting original research in the conference topics, in electronic form (pdf format) via EasyChair. Submissions must be unpublished, not under review for publication elsewhere, and provide sufficient information to judge their merits. Submissions must be in English, and not exceed 12 pages, including the title page, in Springer's LNCS LaTeX style (instructions available here). Additional material, to be read at the discretion of reviewers and PC members, may be provided in a clearly marked appendix or by reference to a manuscript on a web site. Accepted papers will be published in an LNCS volume by Springer. Instructions for formatting camera-ready versions will be communicated to the authors of accepted papers. For an accepted paper to be included in the proceedings, one of the authors must commit to presenting the paper at the conference. --------------------------------- Yandex Awards for the best paper and for the best student paper will be given by the PC. --------------------------------- Organizers and sponsors CSR is organized by Kazan Federal university (Volga region), with the support of (tentative list): The Russia Foundation for Basic Research, http://www.rfbr.ru/rffi/eng/info Kazan Federal University, http://kpfu.ru/eng Yandex, https://www.yandex.com/ --------------------------------- Organizing committee (tentative) The organizing committee can be reached at the following address: CSR2017.Kazan(a)gmail.com Farid Ablayev (KFU), chair Aida Gainutdinova (KFU) Anton Marchenko (KFU) Daniil Musatov (MIPT) Alexander Vasiliev (KFU) Valeria Volkova (KFU) Mansur Ziatdinov (KFU) Marsel Sitdikov (KFU) --------------------------------- Program Committee Farid Ablayev (Kazan, RU) Ittai Abraham (Jerusalem, IL) Isolde Adler (Leeds, UK) Fr??d??rique Bassino (Paris Nord, FR) V??ronique Bruy??re (Mons, BE) Maike Buchin (Bochum, DE) Hubie Chen (San Sebastian, ES) Anuj Dawar (Cambridge, UK) St??phanie Delaune (Cachan, FR) Anna Frid (Marseille, FR) Elena Grigorescu (Purdue, US) Krishna S (Mumbai, IN) K.N. Kumar (Chennai, IN) Fr??d??ric Magniez (Paris, FR) Meena Mahajan (Chennai, IN) Grigory Marshalko (Moscow, RU) Catuscia Palamidessi (Saclay, FR) Victor Selivanov (Novosibirsk, RU) Kavitha Telikepalli (Mumbai, IN) Thomas Thierauf (Aalen, DE) Szymon Torunczyk (Warsaw, PL) H??l??ne Touzet (Lille, FR) Mikhail Volkov (Ekaterinburg, RU) Dorothea Wagner (Karlsruhe, DE) Pascal Weil (Bordeaux, FR), chair --------------------------------- Steering Committee for the CSR series Edward A. Hirsch (St.Petersburg, RU) Juhani Karhum??ki (Turku, FI) Ernst W. Mayr (Munich, DE) Alexander Razborov (Chicago, US and Moscow, RU) Mikhail Volkov (Ekaterinburg, RU) --------------------------------- Previous CSR conferences CSR 2016 took place in St.Petersburg, Russia The list of previous CSR webpages can be found at http://logic.pdmi.ras.ru/~csr/ UNSUBSCRIPTION: If you do not wish to receive any news regarding CSR conferences, please reply to this mail and we will remove you from the mailing list. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

New paper "Sketches for arithmetic universes"
by Steve Vickers 05 Aug '16

05 Aug '16

Some of you may have heard talks about my paper "Sketches for arithmetic universes", or even seen preliminary drafts of it. I now have a version which I intend to submit shortly, and have put it on my website at http://www.cs.bham.ac.uk/~sjv/AUSk.pdf I've also sent it to arXiv. The paper is intended to help deal with a problem with geometric logic, namely that it has infinities in its formalism (specifically: infinitary disjunctions) that are extrinsic to the logic itself and supplied by choosing a base topos. In practice, many of the infinities needed are countable and are not sensitive to change of base as long as the base has a natural numbers object. The aim of this work is to make those infinities intrinsic to the logic by adding type-theoretic ingredients (specifically, list objects, hence in particular nnos) that enable infinite disjunctions to be replaced by existential quantification. Categorically this amounts to replacing Grothendieck toposes (over base with nno) by arithmetic universes (no base needed) - that is to say, by pretoposes with parametrized list objects. Already, Milly Maietti has studied some type-theoretic issues for these. The paper describes "contexts", finite gadgets analogous to sketches that play the role of geometric theories, and their classifying AUs, replacing classifying toposes as generalized spaces. Maps and 2-cells for contexts are also finite gadgets. The 2-category of contexts embeds fully and faithfully in the 2-category of AUs, strict AU-functors, and natural transformations. Steve [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0