Authors: Davide Fazio and Raffaele Mascella

\quad

Our talk concerns an order-theoretical and algebraic investigation of some partially ordered algebraic structures arising in the logico-algebraic approach to Quantum Mechanics (QM), namely paraorthomodular lattices (PLs). Such algebras find a prominent example in the boundedly complete pseudo-Kleene Olson-de 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 logico-algebraic rendering of complementarity phenomena between observables, as they can be regarded as “pastings” of their maximal Boolean “contexts”/sub-algebras (blocks). This means that the order of an OML determines, and it is determined by, the order on its Boolean sub-algebras.

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 lattice-theoretical 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 super-paraorthomodular lattices (SPLs), i.e. pseudo-Kleene lattices satisfying a generalized version of the orthomodular law [1]. We will outline their salient order-theoretical and algebraic properties by providing several characterization results like e.g. a Dedekind-type (forbidden configuration) theorem, and a theory of commutativity (for modular SPLs). It will turn out that the spectral pseudo-Kleene lattice \(\mathbf{L}(\mathcal{H})\) of effects over a separable HS \(\mathcal{H}\) is indeed super-paraorthomodular. 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 super-praorthomodular lattice is isomorphic to a pseudo-Kleene lattice of partial propositions in the algebraic reduct of a PPRM.

Bibliography

1. D. Fazio, and R. Mascella, On Contextuality and Unsharp Quantum Logic,submitted, arXiv:2311.06109.

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 multi-player 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 single-round 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

1. V. Goranko Logics for Strategic Reasoning of Socially Interacting Rational Agents: An Overview and Perspectives. Logics, vol. 1(1), 2023. Online publication: https://www.mdpi.com/2813-0405/1/1/3.
2. Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi. Reasoning about strategies. In Proc. of {FSTTCS} 2010, volume 8 of LIPIcs, pages 133–144.

Authors: Alessandro Aldini and Ludovico Fusco

Since its official patenting in the 1980s, the Radio-Frequency 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 RFID-based 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 low-level, trace-based model suitable for representing RFID systems implementing tree protocols for tag collision arbitration [3]. Our model features a component-oriented, event-based 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 tree-based anti-collision protocols for RFID tags: hyper-reachability, hyper-adaptivity, and generalized non-interference. 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

1. Clarkson, M.R., Schneider, F.B.,Hyperproperties,Journal of Computer Security,vol. XVIII (2010), no. VI, pp. 1157–1210.
2. Coenen, N., Finkbeiner, B., Hahn, C., Hofmann, J.,The Hierarchy of Hyperlogics,LICS ‘19: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science(Vancouver, Canada),article no. 39,2019,pp. 1–13.
3. Popovski, P.,Tree-Based Anti-Collision Protocols for RFID Tags,RFID Systems: Research Trends and Challenges(Miodrag Bolic, David Simplot-Ryl, and Ivan Stojmenovic, editors),Wiley,2010,pp. 203–229.

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 Martin-Lö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 Curry-Howard 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

1. Frank Pfenning and Rowan Davies,A judgmental reconstruction of modal logic,Mathematical Structures in Computer Science,vol. 11 (2001), no. 4, pp. 511–540.
2. Per Martin-Löf,Philosophical aspects of intuitionistic type theory. Lecture notes,Per Martin-Löf: Transcriptions archive,{https://pml.flu.cas.cz/uploads/PML-LeidenLectures93.pdf},1993.

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 turn-based two-players games. In this talk we present the result from our recent paper making explicit the relationship between winning strategies for Lorenzen-style 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

1. Acclavio, M., Catta, D.,Lorenzen-Style Strategies as Proof-Search Strategies,European Conference on Multi-Agent Systems,Cham: Springer Nature Switzerland,(2023).
2. Lorenzen, P.,Logik und Agon,Atti Del XII Congresso Internazionale di Filosofia,vol. 4 (1958), pp. 187–194.
3. Lorenzen, P., Lorenz, K.,Dialogische Logik,Wissenschaftliche Buchgesellschaft [Abt. Verlag],(1978)