Namur 2004 Dynamic QL 1

Dynamic Quantum Logic

Sonja Smets

Center for Logic and Philosophy of Science

Vrije Universiteit Brussel

Part I: Standard Quantum Logic

Very Brief Introduction to the subject:

• Who, When

• Why, Motivation and Aims

• Starting a Logical Calculus

• Logical versus testable properties

• Logic?

• Problems: Implication, Weak modularity.

Namur 2004 Dynamic QL 2

Part II: Dynamic Quantum Logic

Joint work with Alexandru Baltag (Comlab, Oxford)

• Standard Quantum Logic Revisited (solving the problems)

• Dynamic Quantum Logic : Frames, Algebras, Completeness

Part I: Who and When?

Quantum Logic = a domain of research, it originated with: J. von Neumann : “Grundlagen der Quantenmechanik” ’32 G. Birkhoff and J. von Neumann : “The Logic of Quantum Mechanics” ’36 Quantum Logic didn’t had a lot of impact till the 50’s with the work of G. Mackey and the 60-70’s with Jauch, Piron, Varadarajan, Suppes, Finkelstein, Foulis, Randall, etc. Now: Quantum logic knows a revival due to the attraction of “quantum computation and q-information theory” (80’s- : Benioff, Feynman, Deutsch, etc.): e.g. one can use Q-logic as a proof-verification tool for Q-computation.

Part I: Why?, Motivation and Aims

G. Birkhoff and J. von Neumann ’36: Original AIM: “... to discover the logical structure one may hope to find in physical theories which, like quantum mechanics, do not conform to classical logic”.

“Based on admittedly heuristic arguments, one can reasonably expect to find a calculus of propositions which ... resembles the usual calculus of propositions with respect to [classical operators] and, or and not”

In the beginning QL started with an axiomatics based on the Hilbert space structure H

Starting a Logical Calculus

Given a quantum physical system:

• states := one-dimensional linear subspaces of H, call Σ the set of all states

• “Logical” Properties := sets of states P ⊆ Σ (set theoretical union)

• Orthogonality relation:

s ⊥ t iff ∀x ∈ s ∀y ∈ t < x | y >= 0

• Testable properties := biorthogonally closed sets of states, i.e. sets P ⊆ Σ s.t. P =∼∼ P, where

∼ P = {t ∈ Σ | s ⊥ t ∀s ∈ P }.

Intermezzo: Hilbert spaces

Underlying every Hilbert space H: A vector space over a

field D such as for example the complex numbers: ⟨V, +, −, ., \underline{0}⟩ (i.e. a structure with a sum and an associative scalar product which distributes over the sum).

This space is equipped with an inner product: < . | . >: V × V ↦ D s.t. the following conditions hold for

any x, y, z ∈ V and any a ∈ D:

(i) < x | x > ≥ 0; (ii) < x | x > = 0 iff x = \underline{0}; (iii) < y | ax > = a < y | x >; (iv) < x | y + z > = < x | y > + < x | z >;

(v) < x | y > = < y | x >∗, with ∗ the complex conjugate;

This space is metrically complete, indeed, the inner product allows us to define a norm || . || which induces a metric d on the space V :

The norm || x || of a vector is the number (< x | x >)1/2. Two vectors x, y are orthogonal iff

< x | y >= 0. The metric is d(x, y) :=|| x − y ||.

Metrically complete means that every Cauchy sequence of vectors in V converges to a vector of V .

Ref’s: Dalla Chiara et al, Berberian.

Logical versus testable properties

The logical properties are expressions about the system and correspond to unions of linear subspaces, not all of them can be “experimentally evaluated”. The testable properties can be “experimentally evaluated” and correspond to closed linear subspaces. It’s not so that for every arbitrary set of states {s_{i}}_{i} and corresponding logical property P, there exists a unique testable property such that this testable property is true if and only if the system is realized in one of the states of

{s_{i}}.

• example: Take an arbitrary set of states {s, ∼ s} and the corresponding logical property P: “the system is either in state s or in state ∼ s”. For classical systems this property is testable and always true, but not for quantum systems A quantum system can be in a superposition of a state s and a state ∼ s, which means that it is neither in s, nor in ∼ s but has to be located in s⊔ ∼ s :=∼∼ (s∪ ∼ s).

Logic?

The structure of the properties of a classical physical system, corresponds exactly to the structure of the powerset of the state space and hence forms a boolean algebra. Quantum logic deals with the structure of the testable properties (L) of a quantum physical system, which does not correspond to the structure of the powerset of the state space. Due to the appearance of superpositions we have to replace classical disjunctions (which distribute over conjunctions) in our logic by quantum joins which do not distribute over conjuctions. Distributivity has to be replaced by “weak modularity”!

∀P, Q ∈ L and P ⊆ Q then

Q = P ⊔ (Q∩ ∼ P)

Orthocomplemented weak modular lattice = orthomodular lattice.

Namur 2004 Dynamic QL 9

J.M Jauch and C. Piron in ’60 - ’70: Aim: “to inquire on a more fundamental level about the origin of the superposition principle and thus to justify the use of Hilbert space without appeal at the outset of the notion of probability.” Shift in focus from the 50’s on: Quantum logicians were looking for the abstract conditions to describe the property structure of a physical system, without a priori starting from the Hilbert space structure.

The Implication in distributive logic

• Distributivity of conjunctions and disjunctions

• No implication problem:

• We introduce an implication operation by means of : “the implicative condition”:

P ∩ R ⊆ Q iff R ⊆ P → Q

The implicative condition characterizes implicative lattices (classical and intuitionistic logic) since we have:

Skolem’s theorem:

“Any lattice with a binary connective satisfying the implicative condition, is necessarily distributive.”

Namur 2004 Dynamic QL 11

Also important, this implication satisfies the strengthened law of entailment:

P ⊆ Q iff P → Q = Σ

The law of exportation:

(P ∩ R ⊆ Q ⇒ R ⊆ P → Q),

as part of the implicative condition, is equivalent to the so-called “deduction theorem” in the following form (with a given logical theory T and formula’s P, Q):

T ∪ {P } ⊢ Q ⇒ T ⊢ P → Q (∗)

Let us quote J.M. Dunn and G.H. Hardegree (2001):

“... the deduction theorem in its form (∗) is central to the classical and intuitionistic systems, particularly to the intuitionistic system wherein all the pure implicational theorems may be deduced from (∗) and its converse (modus ponens). Accordingly [the implicative condition] is central to the algebraic treatment of the intuitionistic system. ...”

Namur 2004 Dynamic QL 12

The implicative condition can not be encountered in the case of quantum logic since it implies distributivity.

Implication in quantum logic

• Non-distributive

• Joins (no classical disjunctions)

• Implication problem: The implicative condition fails (it implies distributivity). For example: there is no material implication which satisfies the str. law of entailment: in MO2:

P ⊈ Q while ∼ P ⊔ Q = Σ

Quantum logicians have focused on implications which satisfy the str. law of entailment:

Five ways to define an “internal” operator which satisfies the Strengthened Law of Entailment [Kalmbach]

We focus only on the Sasaki Hook Operation:

P →^{s} Q =∼ P ⊔ (Q ∩ P)

But P →^{s} Q cannot be called a good “Implication” (in the non-boolean orthomodular case):

Why ? What Fails ?

• contraposition: P →^{s} Q =∼ Q →^{s}∼ P

• transitivity: (P →^{s} Q) ∩ (Q →^{s} R) ⊆ (P →^{s} R)

• weakening: (Q →^{s} R) ⊆ ((P ∩ Q) →^{s} R)

• deduction theorem: (P ∩ R ⊆ Q ⇒ R ⊆ P →^{s} Q)

Ref. Hardegree 75,79; Herman Marsden Piziak 75; Malinowski 90; Blok et al 84 Is there a way out? YES! Idea = Let us place the Sasaki Hook in its context, i.e. we take a dynamic turn. I will show that the Sasaki Hook is a “dynamic implication” which obviously doesn’t behave nice in a static approach. Ref. Coecke-Smets In some sense the old orthodox moral (adopted by many writers including Birkhoff) should be questioned:

“Quantum Logic can have no decent implication since distribution fails”

Weak Modularity

In Physics: The distributive identity is a logical consequence of the compatibility of observables (Birkhoff & von Neumannn) And the Weak modular identity is a logical consequence of the incompatibility of observables (so: the even in principle NOT-simultaneous measurability).

∀P, Q ∈ L and P ⊆ Q then

Q = P ⊔ (Q∩ ∼ P)

Birkhoff & von Neumann’s (modified) question: “what simple and plausible physical motivation is there for Weak Modularity?” We look for an answer! Standard quantum logic has a big problem: “Weak Modularity is not elementary” (Goldblatt, 1984). There is no way to express the WM property in a (ortho)frame as an elementary (first-order) condition. As a result, WM has not been presented as a frame condition. WM only appeared as an artificial restriction on the valuation (interpretation) in a model.

Namur 2004 Dynamic QL 16

WM should be a frame condition if we ever want to obtain a nice completeness result of quantum logic with respect to the Hilbert space structure. In Part II, we introduce WM as a frame condition! This can be done in a dynamic quantum logic.

Part II: Quantum Logic Revisited

joint work with A. Baltag

QUANTUM LOGIC = the negation-free part of test-only Quantum Dynamic Logic. The syntax consists of a set of propositional formulas, defined by:

φ ::= ⊥ | p | φ ∧ φ | [φ?]φ

Orthocomplement is defined ∼ φ := [φ?]⊥.

Interpretation:

• The interpretation of a formula φ is a “testable property” |φ|, i.e. a closed linear subspace in a Hilbert space.

• The interpretation of a test φ? is given by projective measurements (projectors in a Hilbert Space).

• The formula [φ?]ψ expresses the weakest precondition [φ?]ψ ensuring that (postcondition) ψ will be satisfied after executing φ? . This is nothing but the so-called “Sasaki hook”.

Quantum Dynamic Logic

Our full logic has two sides: propositions φ and quantum programs π.

\begin{matrix}φ ::= & ⊥ & | p & | c & | φ ∧ φ & | ¬φ & | [π]φ \\ π ::= & φ? & | U & | π_{φ} & | π; π & | π ∪ π & | π^{∗} & | π^{†} \end{matrix}

The propositional logic has a classical negation ¬. In addition to propositional variables p, we are given a set of propositional constants c ∈ C, denoting the elements of a basis (of the underlying Hilbert space): so these constants will represent mutually orthogonal states. The weakest precondition formulas [π]ψ are generalized here to “quantum programs” π. Besides tests φ?, the programs will include unitary evolutions U ∈ U, a program π_{φ} (which is a program π that affects only those states satisfying φ and is the identity on the states orthogonal to φ); and regular operations with programs (choice π ∪ π′, sequential composition π; π′, and iteration π^{∗}), as well as an adjoint operation π^{†}.

Completeness

The propositional logic (part) is Boolean: all the non-classical features are pushed into the quantum program expressions. This corresponds to our intuitions: quantum physics does not require a non-classical logic, but only a non-classical notion of physical (inter)action (in particular a non-classical notion of measurement).

In our upcoming paper we present an axiomatic proof system for QDL. The semantics of this logic can be given in terms of what we call quantum frames (QF). The algebra of this logic is (a Boolean version of) what we call a quantum dynamic algebra (QDA). The results we present about QF ’s and QDA’s have as a consequence:

Theorem 1 . Our axiom system for the star-free fragment (i.e. without π^{∗}) of this logic is sound and complete with respect to Hilbert spaces of infinite dimension.

The proof uses Soler’s theorem. As far as we know, this is the first such completeness result. All previous results were about completeness only with respect to some algebraic semantics.

Overview

For simplicity, we present here only the semantical and algebraic structures associated with this logic, concentrating on its “purely quantum” core: no Boolean negations are actually needed.

1. Quantum Frames

2. Concrete Quantum Frames (based on Hilbert spaces)

3. Quantum Dynamic Algebras

4. Representation theorems

Quantum Frames

Definition: (Σ, {→^{P?}}_{P ∈L}, {→^{U}}_{U∈U}) , where

• Σ is a set of “states”, L ⊆ P(Σ) is a collection of “testable properties”, U is a collection of “actions” (“unitary evolutions”)

• {→^{U}}_{U∈U} is a family of binary relations →^{U}⊆ Σ × Σ, indexed by actions U ∈ U

• {→^{P?}}_{P ∈L} is a family of binary relations →^{P?}⊆ Σ × Σ, indexed by properties P ∈ L,

subject to some conditions (to be given later). To formulate these conditions, we need some Definitions: Measurement and orthogonality relations.

s →^{?} t iff s →^{P?} t for some P ∈ L
s ⊥ t iff s ↛^{?} t

Quantum Programs:

Define: The set of Quantum Programs is the least family of binary relations Q ⊆ P(Σ × Σ) which contains :

(1) all tests {→^{P?}}_{P ∈L}

(2) all actions {→^{U}}_{U∈U} and all converse actions

→^{U^{−1}} := ←^{U}

and is closed under:

(3) sequential composition π; π′, defined by

s →^{π;π′} t iff s →^{π} w →^{π′} t for some w ∈ Σ

(4) choice (=infinitary union) ⋃_{i} π_{i}, defined by

s →^{π∪π′} t iff either s →^{π} t or either s →^{π′} t

Define: Quantum maps are the quantum programs obtained form (1) and (2) using only sequential composition (3). (Note that quantum maps are partial functions.)

Namur 2004 Dynamic QL 23

Frame Axioms

We list our conditions for quantum frames.

0. Arbitrary Conjunctions: If L′ ⊆ L then ⋂ L′ ∈ L.

1. Partial Functionality. The outcome of a test is unique:

if s →^{P?} t and s →^{P?} v then t = v

2. Trivial Tests. →^{∅?}= ∅ and →^{Σ?}= {(s, s) | s ∈ Σ}

3. Adequacy. Testing a true property does not change the state:

if s ∈ P then s →^{P?} s

4. Repeatability. Any property holds after it has been successfully tested:

if s →^{P?} t then t ∈ P

[figure: s; P?; t : P]

Axioms continued

5. Compatibility Axiom.

P?; Q? = Q?; P? implies P?; Q? = (P ∩ Q)?

6. Proper Superposition Axiom. Every two states can be properly superposed into a new state:

∀s, t ∈ Σ : ∃w ∈ Σ s.t. s →^{?} w →^{?} t

[figure: s; w; ?; t; ?]

Namur 2004 Dynamic QL 25

7. Self-Adjointness Axiom

If s →^{P?} w →^{?} t then there exists some element v ∈ Σ

s.t. t →^{P?} v →^{?} s.

[figure: s; P?; w; ?; v; ?; t; P?]

Action Axioms

8. Reversibility and Totality. Actions are total bijective functions:

∀t ∈ Σ : ∃!s : s →^{U} t

∀s ∈ Σ : ∃!t : s →^{U} t

9. Orthogonality Preservation. Actions preserve (non-)orthogonality:

Let s, t, s′, t′ ∈ Σ be s.t. s →^{U} s′ and t →^{U} t′.

Then: s → t iff s′ → t′.

[figure: s; <=>; ?; U; s′; ?; t; U; t′]

Axioms continued

10. Ample Unitary Group Axiom: For all states s, t ∈ Σ there exists some action U ∈ U such that:

s →^{U} t

and

w →^{U} w for all states w ⊥ s, t

[figure: w; U; +; ×; s; U; t]

11. Dimensionality: There exist an infinite set of states in Σ such that each

s_{i} ↛ s_{j} for i ≠ j.

Namur 2004 Dynamic QL 28

The Adjoint of a Program

Define Adjoints: † : Q → Q by induction:

1. (P?)^{†} = P?

2. U^{†} = U^{−1}, where U^{−1} is the inverse function (corresponding to the converse relation ←^{U})

3. (U^{−1})^{†} = U

4. (π; σ)^{†} = σ^{†}; π^{†}

5. (⋃_{i} π_{i})^{†} = ⋃_{i} π_{i}^{†}

Observe: (π^{†})^{†} = π

Namur 2004 Dynamic QL 29

Proposition:

Adjointness for quantum programs Let s, w, t ∈ Σ: If s →^{π} w →^{?} t then there exists some element v ∈ Σ s.t. t →^{π^{†}} v →^{?} s.

[figure: s; π; w; ?; v; ?; t; π^{†}]

Orthocomplement, Precondition and Image

For P ⊆ Σ and π ⊆ Σ × Σ, let :

∼ P := [P?]⊥

[π]P := {s ∈ Σ | ∀t(s →^{π} t ⇒ t ∈ P)}

(the weakest precondition ensuring P after π) and

π(P) :=∼ [π^{†}] ∼ P

Theorem 2 .

• π(P) is the image of P under program π:

π(P) = {t : s →^{π} t for some s ∈ P }

• Quantum Modus Ponens (=Weak Modularity):

P ∩ [P?]Q ⊆ P

• Linearity of programs: \overline{π(P)} = π(\overline{P})

Concrete Quantum Frames

We can associate a QF to any Hilbert space H, in a canonical manner:

(Σ, {→^{P?}}_{P ∈L}, {→^{U}}_{U∈U})

• States s ∈ Σ: one-dimensional subspaces of H

• Properties P ∈ L: sets P ⊆ Σ of states, such that ⋃ P is a closed linear subspace of H

• Quantum Programs: unions of linear maps. Every linear operator F : H → H induces a quantum map on states π ⊆ Σ × Σ, given by:

s →^{π} t iffF (x) = y ≠ 0 for some x ∈ s, y ∈ t

Quantum programs are arbitrary unions of such linear operators.

• Quantum Tests P?: the quantum maps induced by the projectors P roj_{W} on the closed subspace W = ⋃ P associated to P.

• Actions U ∈ U: the quantum maps induced by unitary transformations of H.

Representation Theorem

A ”concrete quantum frame” is any subframe of the frame induced by a Hilbert space H.

Theorem 3 . Every concrete QF is a QF.

Theorem 4 . (Representation Theorem) Every QF is isomorphic to a concrete QF.

Quantum Dynamic Algebras

Note: The algebraic semantics for PDL (cfr. Dynamic Frame) is a dynamic algebra with tests and actions (Pratt & Kozen ‘79)

A quantum dynamic algebra is a structure:

( L, Q, U, ⋀, ⋃,; , †,?, [−]−)

consisting of: a set L of ”properties”, a set Q of ”quantum programs”, a set U ⊆ Q of ”actions”; and operations:

⋀ : P(L)→L  ⋃ : P(Q)→Q
; : Q × Q→Q  ? : L→Q

[−]− : Q × L→L

subject to a number of conditions (to be given later).

Namur 2004 Dynamic QL 34

Abbreviations

⊥ := ⋀ L ∼: L→L, ∼ P := [P?]⊥

⊤ :=∼ ⊥ P ≤ Q iffP ∧ Q = P P ⊥ Q iffP ≤∼ Q

At(L) := {P ∈ L : ∀Q ∈ L(⊥ ≠ Q ≤ P ⇒ Q = P)}

Namur 2004 Dynamic QL 35

Axioms for QDA’s

• (L, ⋀) is a complete lattice

• (Q, ⋃, ⊤?) is a unital quantale having ⊤? as its

unit: ⊤?; π = π; ⊤? = π.

• ⊥? ≤ π (i.e. ⊥_{L}? = ⊥_{Q})

• π; ⊥? = ⊥?; π = ⊥?

• Q is generated by U ∪ {P? : P ∈ L} using ; and ⋃.

• Normality: [π]⊤ = ⊤

• Distributivity: [π](⋀_{i} P_{i}) = ⋀_{i}[π]P_{i}

• Choice: [⋃_{i} π_{i}]P = ⋀_{i}[π_{i}]P

• Composition: [π; σ]P = [π][σ]P

• Partial Functionality for Tests:

if Q ∈ At(L) then P?(Q) ∈ At(L) ∪ {⊥}

• Repeatability: [P?]P = ⊤,

• Adequacy : P ∧ Q ≤ [Q?]P and [⊤?]P ≤ P

Namur 2004 Dynamic QL 36

• Compatibility: If P?; Q? = Q?; P? then

P?; Q? = (P ∩ Q)?

• Proper Superpositions:

if P, Q ≠ ⊥ then there exist R, S ∈ L such that

R?; S?(P) ∧ Q ≠ ⊥.

• Adjointness Axiom: P ≤ [π] ∼ [π^{†}] ∼ P

• Adjoints : P?^{†} = P?,

(π; σ)^{†} = σ^{†}; π^{†}, (⋃_{i} π_{i})^{†} = ⋃_{i}(π_{i}^{†})

• Total Functionality for Actions: if Q ∈ At(L) then

U(Q) ∈ At(L)

• Reversibility of Actions: U; U^{†} = U^{†}; U = T?

• Ample Unitary Group Axiom: if P, Q ≠ ⊥ then there exists some U ∈ U such that:

U(P) ∧ Q ≠ ⊥
U(R) ≤ R for allR ⊥ P, Q

• Dimensionality :

∃P_{i} ∈ L s.t. P_{i} ⊥ P_{j} for all i ≠ j.

Representation Theorems

Theorem 5 . (Second Representation Theorem) Every QF induces a QDA, in the obvious way. Conversely, every QDA is isomorphic to such a frame-induced QDA.

Consequences: The two Representation theorems imply:

• Every QDA is isomorphic to a ”concrete” QDA, i.e. one based on a Hilbert space.

• Completeness for our Quantum Dynamic logic.

Representation Theorems

Main Point: I presented a Quantum Dynamic Logic (QDL), designed as a logical calculus for quantum information flow. This is a quantum version of P DL, i.e. a logic equipped with dynamic modalities to deal with quantum measurements (“tests”), and unitary evolutions.

Claims

Claim 1: Standard Quantum Logic is the negation-free “test-only” fragment of Quantum Dynamic Logic. Sasaki hook is re-discovered as a standard dynamic modality: the weakest precondition.

Claim 2 : We have a Frame Condition for Weak Modularity, giving a natural “operational” meaning to this axiom.

Claim 3 : We have a Completeness result for Hilbert spaces. Our proofs use the representation theorem of C. Piron added with the improvement of M.P. Solér.

Some REFS:

• For compound systems: A. Baltag and S. Smets “The Logic of Quantum Programs”, http://philsci-archive.pitt.edu/archive/00001799/

• For single systems: A. Baltag and S. Smets “The Logic of Quantum Actions” upcoming

• About WM and the Sasaki hook: B. Coecke and S. Smets “The Sasaki Hook is not a [Static] Implicative Connective but Induces a Backward [in Time] Dynamic One that Assigns Causes”, quant-ph/0111076 S. Smets: “On Causation and a Counterfactual in Quantum Logic: The Sasaki Hook”, philsci-archive.pitt.edu/archive/00000619/

• Most recent book on QL: M. Dalla Chiara, R. Giuntini and R. Greechie: Reasoning in Quantum Theory, Kluwer 2004

• Hilbert Spaces: S.K. Berberian: Introduction to Hilbert Space, Chelsea Publishing Company, 1961