Contributed Talks 16
Chair: Gianluca Curzi
Talks in this session
14:00 
Davide Fazio, On Contextuality and unsharp quantum logic 
Authors: Davide Fazio and Raffaele Mascella \quad Our talk concerns an ordertheoretical and algebraic investigation of some partially ordered algebraic structures arising in the logicoalgebraic approach to Quantum Mechanics (QM), namely paraorthomodular lattices (PLs). Such algebras find a prominent example in the boundedly complete pseudoKleene Olsonde Groote spectral lattice of effects over a separable Hilbert space \(\mathcal{H}\). It is well known that the set \(\mathbf{P}(\mathcal{H})\) of projections over a separable Hilbert space (HS) \(\mathcal{H}\) can be regarded as quantum experimental propositions concerning Lüders measurements which form a complete orthomodular lattice (OML). OMLs provide a logicoalgebraic rendering of complementarity phenomena between observables, as they can be regarded as “pastings” of their maximal Boolean “contexts”/subalgebras (blocks). This means that the order of an OML determines, and it is determined by, the order on its Boolean subalgebras. Over the past years, it has been argued that the idealizing and simplifying assumption of considering only Lüders measurements leads to conflict with experimental possibilities and to theoretical inconsistencies. As a consequence, generalized measurable “unsharp” properties, whose formal counterpart is given by effects, have been introduced. In order to provide them with a logical structure which is amenable of latticetheoretical investigations, PLs, i.e. “unsharp” generalizations of OMLs, have been defined. In the first part of our talk we characterize the class of paraorthomodular lattices which are “pastings” of their Kleene (i.e. distributive) blocks. To this aim we introduce the variety of superparaorthomodular lattices (SPLs), i.e. pseudoKleene lattices satisfying a generalized version of the orthomodular law [1]. We will outline their salient ordertheoretical and algebraic properties by providing several characterization results like e.g. a Dedekindtype (forbidden configuration) theorem, and a theory of commutativity (for modular SPLs). It will turn out that the spectral pseudoKleene lattice \(\mathbf{L}(\mathcal{H})\) of effects over a separable HS \(\mathcal{H}\) is indeed superparaorthomodular. Moreover, SPLs’ theory captures important features of spectral lattices as, for example, orthocomplemented elements of an SPL \(\mathbf{A}\) always form an orthomodular poset. In the second part of the talk, taking advantage of well known J. Czelakowski’s results, we introduce paraconsistent partial referential matrices (PPRM) for the formal treatment of (partial) experimental quantum propositions taking truth values over the three element Kleene chain \(\mathbf{K}_{3}\), which are meaningful/defined for certain states of a physical system, and undefined otherwise. We will show that any superpraorthomodular lattice is isomorphic to a pseudoKleene lattice of partial propositions in the algebraic reduct of a PPRM. Bibliography


14:25 
Valentin Goranko, Local Basic Strategy Logic 
Basic Strategy Logic (BSL) introduced in [1] is a minimal system of strategy logic of the type studied in [2]. BSL builds on a fixed set of agents \(\mathsf{Agt}\) and on some (usually temporalized) language for expressing agents goals, such as LTL, that defines a set of goal formulae \(\Gamma\) which are evaluated on plays in concurrent game models. The language of BSL extends \(\Gamma\) with standard Boolean connectives and associates with each agent \(\mathsf{a} \in \mathsf{Agt}\) a strategy variable, denoted by \(\mathsf{x}_{\mathsf{a}}\). These variables range over strategies for the respective agents and can be quantified over within the formulae of BSL. Thus, BSL can be used for formalising the reasoning about strategic abilities of agents (players) and coalitions in concurrent multiplayer games. It is shown in [1] that BSL is sufficiently expressive to capture many naturally defined recently studied operators and logics for strategic abilities. In the present work I study its local version LBSL, which only involves in the language of \(\Gamma\) the Nexttime temporal operator, referring to the immediate outcomes states from playing singleround concurrent games at the states of the model. I explore and characterise the expressiveness of LBSL, study its validities, present an axiomatic system for them, and discuss the problems of its completeness and of the decidability of LBSL. Bibliography


14:50 
Ludovico Fusco, Modeling hyperproperties for RFID systems 
Authors: Alessandro Aldini and Ludovico Fusco Since its official patenting in the 1980s, the RadioFrequency Identification (RFID) technology has experienced relentless advancement due to its extreme versatility and usability in a wide range of contexts. Moreover, as an enabling technology for the IoT computing paradigm, RFID today underpins new tools for object identification/data acquisition in smart environments. Although there have been many contributions to the formal description and verification of RFIDbased systems and protocols, there has yet to be much progress toward an explicit modeling of information flow policies for RFID systems in terms of hyperproperties [1]. In this work, we initiate a taxonomy of hyperproperties for RFID systems, laying the foundation for a general framework for their formalization. To this end, we introduce a lowlevel, tracebased model suitable for representing RFID systems implementing tree protocols for tag collision arbitration [3]. Our model features a componentoriented, eventbased notion of state allowing us to express hyperproperties in terms of event satisfaction by component configurations. In this context, we introduce and discuss three classes of hyperproperties for the analysis of treebased anticollision protocols for RFID tags: hyperreachability, hyperadaptivity, and generalized noninterference. For each of them, we provide a classical definition in the style of [1] and a formalization in a suitable hyperlogic [2]. Finally, we propose some insights about decidability issues. Bibliography


15:15 
Ivo Pezlar, A logic of judgmental existence and its relation to truncation and proof irrelevance 
We introduce a simple natural deduction system for reasoning with judgments of the form “there exists a proof of \(\varphi\)” to explore the notion of judgmental existence, following MartinLöf’s methodology of distinguishing between judgments and propositions. In this system, the existential judgment denoted as \(\varphi\) exist (or with explicit proof expressions as \(e \therefore \varphi\)) can be internalized into a modal notion of propositional existence denoted as \(\textsf{E} \varphi\). This modality is closely related to truncation modality, a key tool for obtaining proof irrelevance. We provide a constructive meaning explanation for existential judgments and computational interpretation in the style of the CurryHoward isomorphism for the corresponding existence modality. The investigation of judgmental existence is directly motivated by [2] who informally considers a new judgment of the form \(\varphi\) exists as expressing the notion of “bare existence”. The logic of judgmental existence itself is inspired by [1] and their judgmental reconstruction of modal logic. Formally, our system shares the most resemblance with their possibility logic and lax logic, however, we also allow existence premises of the form \(\varphi\) exists for elimination rules, not only true premises of the form \(\varphi\) true. In its present form, our logic deals only with a fragment of propositional logic containing the existence modality \(\textsf{E}\) and implication \(\to\). We show that both logical connectives are locally sound and complete in this system. Furthermore, we show that the system satisfies the structural properties of exchange, weakening, and contraction and we prove substitution lemma, subject reduction, and the strong normalization property. We do not consider dependent types and proof irrelevance is assumed to be propositional, not judgmental. Bibliography


15:40 
Matteo Acclavio, Dialogical strategies as proofsearch strategies 
Authors: Matteo Acclavio and Davide Catta Dialogical logic, originated in the work of Lorenzen and his student Lorenz [2,3], is an approach to logic in which the validity of a certain formula is defined as the existence of a winning strategy for a particular kind of turnbased twoplayers games. In this talk we present the result from our recent paper making explicit the relationship between winning strategies for Lorenzenstyle dialogical games and sequent calculus derivations [1]. We focus on three different classes of dialogical logic games for the implicational fragment of intuitionistic logic, showing that winning strategies for such games naturally correspond to classes of derivations defined by uniformly restraining the rules of the sequent calculus. Bibliography
