arXiv:2511.10188 · Logic Journal of IGPL

Quantum modal logic

Kenji Tokuo

Published Nov 12, 2024• 3 citations

Abstract

Abstract A modal logic based on quantum logic is formalized in its simplest possible form. Specifically, a relational semantics and a sequent calculus are provided, and the soundness and the completeness theorems connecting both notions are demonstrated. This framework is intended to serve as a basis for formalizing various modal logics over quantum logic, such as quantum alethic logic, quantum temporal logic, quantum epistemic logic, and quantum dynamic logic.

DOI: 10.1093/jigpal/jzae123

Related papers

LQP: The Dynamic Logic of Quantum Information

Alexandru Baltag, Sonja Smets

The main contribution of this paper is the introduction of a dynamic logic formalism for reasoning about information flow in composite quantum systems. This builds on our previous work on a complete quantum dynamic logic for single systems. Here we extend that work to a sound (but not necessarily complete) logic for composite systems, which brings together ideas from the quantum logic tradition with concepts from (dynamic) modal logic and from quantum computation. This Logic of Quantum Programs (LQP) is capable of expressing important features of quantum measurements and unitary evolutions of multi-partite states, as well as giving logical characterisations to various forms of entanglement (for example, the Bell states, the GHZ states etc.). We present a finitary syntax, a relational semantics and a sound proof system for this logic. As applications, we use our system to give formal correctness proofs for the Teleportation protocol and for a standard Quantum Secret Sharing protocol; a whole range of other quantum circuits and programs, including other well-known protocols (for example, superdense coding, entanglement swapping, logic-gate teleportation etc.), can be similarly verified using our logic.

arXiv:2110.01361Oct 4, 20211 citation

Birkhoff style proof systems for hybrid-dynamic quantum logic

Daniel Găină

We explore a simple approach to quantum logic based on hybrid and dynamic modal logic, where the set of states is given by some Hilbert space. In this setting, a notion of quantum clause is proposed in a similar way the notion of Horn clause is advanced in first-order logic, that is, to give logical properties for use in logic programming and formal specification. We propose proof rules for reasoning about quantum clauses and we investigate soundness and compactness properties that correspond to this proof calculus. Then we prove a Birkhoff completeness result for the fragment of hybrid-dynamic quantum logic determined by quantum clauses.

arXiv:2406.13360Jun 19, 20240 citations

The Logic of Quantum Programs

Alexandru Baltag, Sonja Smets

We present a logical calculus for reasoning about information flow in quantum programs. In particular we introduce a dynamic logic that is capable of dealing with quantum measurements, unitary evolutions and entanglements in compound quantum systems. We give a syntax and a relational semantics in which we abstract away from phases and probabilities. We present a sound proof system for this logic, and we show how to characterize by logical means various forms of entanglement (e.g. the Bell states) and various linear operators. As an example we sketch an analysis of the teleportation protocol.

arXiv:2109.06792Sep 14, 202141 citations

Strict implication in quantum modal logic

Kenji Tokuo

Abstract Quantum logic has no canonical implication connective, and polynomial candidates differ in the inferential principles they satisfy. We study a relational strict implication in quantum modal logic and interpret it through the modal accessibility relation. On reflexive modal frames, a formula formed with this connective is valid exactly when its antecedent semantically entails its consequent. The connective therefore internalizes semantic consequence. The forcing condition links modal accessibility to non-orthogonality. Consequently, any formula whose principal connective is this strict implication has the same truth value throughout each component determined by non-orthogonality. The truth set of each such formula therefore belongs to the Boolean algebra of unions of these components. We also establish further semantic laws and analyze quantum disjunction, contraposition, and nested implications.

Logic Journal of IGPLSep 4, 20260 citations

A LOGIC-ALGEBRAIC FRAMEWORK FOR CONTEXTUALITY AND MODALITY IN QUANTUM SYSTEMS

Héctor Freytes

In this work we develop a modal structure for the simultaneous treatment of \nactual and possible properties of quantum systems. A logical system based on \northomodular lattices enriched with a modal operator is given, obtaining algebraic \ncompleteness and completeness with respect to a Kripke-style semantic. \nWe show that, in spite of the fact that, the language is enriched with the addition \nof a modal operator, contextuality remains a central feature of quantum \nsystems.

Mar 5, 20140 citations

Foundations of logic programming in hybrid-dynamic quantum logic

Daniel Găină

The main contribution of the present paper is the introduction of a simple yet expressive hybrid-dynamic logic for describing quantum programs. This version of quantum logic can express quantum measurements and unitary evolutions of states in a natural way based on concepts advanced in (hybrid and dynamic) modal logics. We then study Horn clauses in the hybrid-dynamic quantum logic proposed, and develop a series of results that lead to an initial semantics theorem for sets of clauses that are satisfiable. This shows that a significant fragment of hybrid-dynamic quantum logic has good computational properties, and can serve as a basis for defining executable languages for specifying quantum programs. We set the foundations of logic programming in this fragment by proving a variant of Herbrand's theorem, which reduces the semantic entailment of a logic-programming query by a program to the search of a suitable substitution.

arXiv:2406.02085Jun 4, 20240 citations