 



\documentstyle[
   portrait,%% from LM
  slidesonly,%  Try notes or notesonly instead.
  fancybox,
  %notes,%      Use instead of slidesonly to typeset the notes.
  %notesonly,%  Use instead of slidesonly to typeset notes and slides.
  %semcolor,%   Try me if using PSTricks.
  %semrot,%     Try me if using Rokicki's dvips.
  semhelv,%    Try me if using a PostScript printer.
  %article,%    Try me.
  %portrait,%   Try me.
  sem-a4,%     Try me if using A4 paper.
  semlayer%     This must be included, but you need the semcolor option to
  ]{seminar}                                  % actually see the overlays.



\renewcommand{\sliderightmargin}{-.0in}  %%% was -.75in
\renewcommand{\slideleftmargin}{-.0in}  %%% was -.75in
%\oddsidemargin -4in
%\evensidemargin -7in


\newpagestyle{MH}%
 {\hskip .15in{\tiny{Namur 2004}}\hfil  \tiny{Dynamic QL} \thepage\hskip .15in}{} 
\pagestyle{MH}



%\input{diagram.tex}
\input{xypic.sty}
\xyoption{all}
\slidesmag{5}%%% was 5
\articlemag{1}


\rotateheaderstrue          % Try this out if using rotation macros.



\newcommand{\sref}[1]{SLIDE \ref{#1}}
%\newcommand{\heading}[1]{\begin{center}\large\bf
%#1\end{center}}


\newcommand{\heading}[1]{%
  \begin{center}
    \large\bf
    \doublebox{#1}%
  \end{center}
  \vspace{1ex minus 1ex}}

\newcommand{ \proP}{{\mathbf P}}

\newcommand{ \QQ}{{\mathbf Q}}
\newcommand{ \Mod}{{\mathbf{ SMod}}}

%\pagestyle{empty}
\centerslidesfalse

\newenvironment{mybox}      {\begin{Sbox}\begin{minipage}{0.9\textwidth}}      {\end{minipage}\end{Sbox}      \shadowbox{\TheSbox}} \newenvironment{mybox2}      {\begin{Sbox}\begin{minipage}{0.42\textwidth}}      {\end{minipage}\end{Sbox}      \fbox{\TheSbox}} \newenvironment{mybox3}      {\begin{Sbox}\begin{minipage}{0.55\textwidth}}      {\end{minipage}\end{Sbox}      \fbox{\TheSbox}} \newenvironment{myboxdef}      {\begin{Sbox}\begin{minipage}{0.9\textwidth}}      {\end{minipage}\end{Sbox}\ovalbox{\TheSbox}} \newenvironment{myboxaxm}      {\begin{Sbox}\begin{minipage}{0.9\textwidth}}      {\end{minipage}\end{Sbox}   \setlength{\fboxsep}{.05cm}\Ovalbox{\setlength{\fboxsep}{.4cm}\Ovalbox{\TheSbox}}} \newenvironment{myboxap}      {\begin{Sbox}\begin{minipage}{0.9\textwidth}}      {\end{minipage}\end{Sbox}   \setlength{\fboxsep}{.0cm}\Ovalbox{\setlength{\fboxsep}{.4cm}\Ovalbox{\TheSbox}}} \newenvironment{myboxqd}      {\begin{Sbox}\begin{minipage}{1\textwidth}}      {\end{minipage}\end{Sbox}\Ovalbox{\TheSbox}} \newenvironment{myboxqd2}      {\begin{Sbox}\begin{minipage}{0.45\textwidth}} {\end{minipage}\end{Sbox}\ovalbox{\TheSbox}} \newenvironment{myboxqd3}      {\begin{Sbox}\begin{minipage}{0.33\textwidth}} {\end{minipage}\end{Sbox}\ovalbox{\TheSbox}} 


  \newcommand{\bq}{\begin{quote}} \newcommand{\eq}{\end{quote}} \newcommand{\lood}{^\perp} \newcommand{\en}{\&} \newcommand{\of}{\vee} \newcommand{\meet}{\wedge} \newcommand{\M}{\mid\mid} \newtheorem{Th}{Theorem}   \newtheorem{ax}{Axiom}   \newtheorem{lm}{Lemma}  \newtheorem{df}{Definition}     \newtheorem{pr}{Proposition}  \newtheorem{cl}{Corollary}   \newtheorem{re}{Remark}     \newtheorem{as}{Assumption}   \newtheorem{wg}{Wild Guess} \newtheorem{ex}{Example} \newcommand{\bth}{\begin{Th}\hspace{-5pt}{\bf .} \ }  \newcommand{\Eth}{\end{Th}} \newcommand{\bax}{\begin{ax}\hspace{-5pt}{\bf .} \ }  \newcommand{\eax}{\end{ax}} \newcommand{\blm}{\begin{lm}\hspace{-5pt}{\bf .} \ } \newcommand{\elm}{\end{lm}} \newcommand{\bdf}{\begin{df}\hspace{-5pt}{\bf .} \ }    \newcommand{\edf}{\end{df}}  \newcommand{\bpr}{\begin{pr}\hspace{-5pt}{\bf .} \ }  \newcommand{\epr}{\end{pr}} \newcommand{\bcl}{\begin{cl}\hspace{-5pt}{\bf .} \ }  \newcommand{\ecl}{\end{cl}} \newcommand{\bre}{\begin{re}\hspace{-5pt}{\bf .} \ } \newcommand{\ere}{\end{re}} \newcommand{\bas}{\begin{as}\hspace{-5pt}{\bf .} \ } \newcommand{\eas}{\end{as}} \newcommand{\bwg}{\begin{wg}\hspace{-5pt}{\bf .} \ } \newcommand{\ewg}{\end{wg}} \newcommand{\bex}{\begin{ex}\hspace{-5pt}{\bf .} \ }   \newcommand{\eex}{\end{ex}} \newcommand{\bpf}{\noindent {\bf Proof:} } \newcommand{\epf}{$\bullet$\par\vspace{1.8mm}\noindent} \newcommand{\bit}{\begin{itemize}} \newcommand{\eit}{\end{itemize}\par\noindent} \newcommand{\beq}{\begin{equation}}  \newcommand{\eeq}{\end{equation}\par\noindent} \newcommand{\beqa}{\begin{eqnarray*}} \newcommand{\eeqa}{\end{eqnarray*}\par\noindent} \newcommand{\beqn}{\begin{eqnarray}}   \newcommand{\eeqn}{\end{eqnarray}\par\noindent}
\newcommand{\diraco}{\mid 0 \rangle}
\newcommand{\dirac}{\mid 1 \rangle}
\newcommand{\Odiraco}{\overline{\mid 0 \rangle}}
\newcommand{\Odirac}{\overline{\mid 1 \rangle}} \newcommand{\langep}{\stackrel{\textstyle \xi}{\textstyle \downarrow}} \newcommand{\langepijl}{\stackrel{\textstyle \mid}{\textstyle \langep}}
\newcommand{\sasaki}{\stackrel{S}{\to}}   

\begin{document}
\usepackage{diagrams.sty}

%\maketitle          % This won't show up when \onlynotestoo is in effect.
\begin{slide}[7in,10in]  
\heading{Dynamic Quantum Logic}
\center{Sonja Smets}
\center{Center for Logic and Philosophy of Science}
\center{Vrije Universiteit Brussel}
\bigskip
\flushleft
{\bf Part I: Standard Quantum Logic}
\medskip\par
Very Brief Introduction to the subject:
\medskip\par
$\bullet$ Who, When\\
$\bullet$ Why, Motivation and Aims\\
$\bullet$ Starting a Logical Calculus\\
$\bullet$ Logical versus testable properties\\
$\bullet$ Logic?\\
$\bullet$ Problems: Implication, Weak modularity.
\newpage
{\bf Part II: Dynamic Quantum Logic}
\medskip\par
Joint work with Alexandru Baltag (Comlab, Oxford)

$\bullet$ Standard Quantum Logic Revisited (solving the problems)\\
$\bullet$ Dynamic Quantum Logic : Frames, Algebras, Completeness

\end{slide}



\begin{slide}[7.3in,10.1in]  
\heading{Part I:  Who and When?}
\medskip\par
{\bf 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

{\bf 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.

\end{slide}

\begin{slide}[7.3in,10.1in]  
\heading{Part I: Why?, Motivation and Aims}
\medskip\par
{\bf G. Birkhoff and J. von Neumann '36:}
{\bf 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".
\medskip\par
``Based on admittedly heuristic arguments, one can reasonably expect to find a calculus of
propositions which ... {\it resembles the usual calculus}
of propositions with respect to [classical operators] {\it and, or} and {\it not}" 

\medskip\par
\bf{In the beginning QL started with an axiomatics based on the Hilbert space structure ${\cal H}$}




\end{slide}

\begin{slide}[7.3in,10.1in]  
\heading{Starting a Logical Calculus}

Given a quantum physical system:

$\bullet$ {\bf states} := one-dimensional linear subspaces of ${\cal H}$, call $\Sigma$ the set of all states \\
$\bullet$ {\bf ``Logical" Properties} := sets of states $P \subseteq \Sigma$ (set theoretical union)\\
$\bullet$ {\bf Orthogonality relation:}
$$ s \perp t \, \, {\rm iff} \, \, \forall x \in s \, \forall y \in t \, \, <x \mid y > = 0$$
$\bullet$ {\bf Testable properties}  := biorthogonally closed sets of states, i.e. sets $P \subseteq \Sigma$ s.t. $P = \sim \sim P$, where $\sim P = \{ t \in \Sigma \mid s \perp t \, \, \forall s \in P\}$.


\end{slide}

\begin{slide}[7.3in,10.1in]  
\heading{Intermezzo: Hilbert spaces}

Underlying every Hilbert space ${\cal H}$:
{\small
A {\bf vector space over a field $D$} such as for example the complex numbers: $\langle V, +, -, ., \underline{0}\rangle$ (i.e. a structure with a sum and an associative scalar product which distributes over the sum).  

This space is {\bf equipped with an inner product}: $<. \mid . >: V \times V \mapsto D$ s.t. the following conditions hold for any $x,y,z \in V$ and any $a \in D$:

{\tiny
(i) $<x \mid x> \, \, \geq 0$; \\
(ii) $<x \mid x > \, = 0$ iff $x = \underline{0}$;\\
(iii) $<y \mid a x> \, = \, a < y  \mid x>$;\\
(iv) $<x \mid y + z>  \, = \,  <x \mid y> + <x \mid z>$;\\
(v) $<x \mid y> \, =Ê\, <y \mid x>^*$, with $*$ the complex conjugate;}

This space is {\bf metrically complete}, indeed, the inner product allows us to define a norm $\mid \mid . \mid \mid$ which induces a metric $d$ on the space $V$:

{\tiny
The norm $\mid \mid x \mid \mid$ of a vector is the number $(< x \mid x>)^{1/2}$. Two vectors $x, y$ are orthogonal iff $<x \mid y> = 0$.

The metric is $d(x, y) := \mid \mid x -Êy \mid \mid$.

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

Ref's: Dalla Chiara et al, Berberian.}

\end{slide}


\begin{slide}[7.3in,10.1in]  
\heading{Logical versus testable properties}

The {\bf logical properties} are expressions {\it about} the system and correspond to unions of linear subspaces, not all of them can be ``experimentally evaluated".

The {\bf 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\}$.

$\bullet$ {\bf example:} Take an arbitrary set of states $\{s,\sim s\}$ and the corresponding logical property $P$: ``the system is either in state $s$ or in state $\sim s$".    {\it For classical systems this property is testable and always true, but not for quantum systems}  

{\it A quantum system can be in a superposition} of a state $s$ and a state $\sim s$, which means that it is neither in $s$, nor in $\sim s$ but has to be located in $s \sqcup \sim s := \sim \sim (s \cup \sim s)$.

\end{slide}

\begin{slide}[7.3in,10.1in]  
\heading{Logic?}

The structure of the properties of {\bf 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 {\bf the testable properties} (${\cal 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 {\bf superpositions} we have to replace classical disjunctions (which distribute over conjunctions) in our logic by {\bf quantum joins} which do not distribute over conjuctions.   

Distributivity has to be replaced by ``weak modularity"!

$\forall P,Q \in {\cal L}$ and $P \subseteq Q$ then
$$ Q = P \sqcup (Q \cap \sim P)$$

Orthocomplemented weak modular lattice = orthomodular lattice.


\end{slide}



\begin{slide}[7.3in,10.1in]  
{\bf J.M Jauch and C. Piron in '60 - '70:}

{\bf Aim:} ``to inquire on a more fundamental level about the origin of the superposition principle and
thus {\it to justify the use of Hilbert space} without appeal at the outset of the notion of probability."

{\rm 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}.



\end{slide}


\begin{slide}[7in,10in]  
\heading{The Implication in distributive logic}

$\bullet$ Distributivity of conjunctions and disjunctions\\
$\bullet$ No implication problem:\\
$\bullet$ We introduce an implication operation by means of :\\
\centerline{``the implicative condition":}
\smallskip\par\noindent
\centerline{$P \cap R \subseteq Q$ iff $R \subseteq P \rightarrow Q$}
\smallskip\par\noindent The implicative condition characterizes implicative lattices (classical and intuitionistic logic) since we have:
\par\noindent
\centerline{Skolem's theorem:}
\begin{quote} ``Any lattice with a binary connective satisfying the implicative condition, is necessarily
distributive."
\end{quote}
\newpage Also important, this implication satisfies the strengthened law of entailment:
\smallskip\par\noindent
\centerline{$P \subseteq Q$ iff $P \rightarrow Q = \Sigma$}
\smallskip\par\noindent The law of exportation:\\
 $(P \cap R \subseteq Q \Rightarrow R \subseteq P \rightarrow 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$):
\smallskip\par\noindent
\centerline{$T \cup \{P\} \vdash Q \Rightarrow T \vdash P \rightarrow Q \ \ \ (\ast)$}
\smallskip\par\noindent Let us quote J.M. Dunn and G.H. Hardegree (2001):
\begin{quote} ``... the deduction theorem in its form ($\ast$) is central to the classical and intuitionistic
systems, particularly to the intuitionistic system wherein all the pure implicational theorems may be deduced from
($\ast$) and its converse (modus ponens). Accordingly [the implicative condition] is central to the algebraic
treatment of the intuitionistic system. ..."
\end{quote}
\newpage
\smallskip\par\noindent The implicative condition can not be encountered in the case of quantum logic since it
implies distributivity. 
\end{slide}

\begin{slide}[7in,10in]  
\heading{Implication in quantum logic}

\par\noindent
$\bullet$ Non-distributive\\
$\bullet$ Joins (no classical disjunctions)\\
$\bullet$ 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 \not \subseteq Q$ while  
$\sim P \sqcup Q= \Sigma$\\
\par\noindent Quantum logicians have focused on  implications which satisfy the str. law of entailment:
\smallskip\par\noindent Five ways to \\ define an ``internal" operator  \\ which satisfies the \\ Strengthened Law
of Entailment [Kalmbach] \\ \\ We focus only on the Sasaki Hook Operation: \\
$P\stackrel{s}{\rightarrow} Q = \sim P \sqcup (Q \cap P)$
\newpage But $P \stackrel{s}{\rightarrow} Q$ cannot be called a good ``Implication" (in the non-boolean
orthomodular case):
\\ \\ Why ? What Fails ? 
\\
$\bullet$ contraposition: $P \stackrel{s}{\rightarrow} Q =  \sim Q
\stackrel{s}{\rightarrow} \sim P$\\
$\bullet$ transitivity: $(P \stackrel{s}{\rightarrow} Q) \cap (Q
\stackrel{s}{\rightarrow} R) \subseteq (P \stackrel{s}{\rightarrow} R)$\\
$\bullet$ weakening: $(Q \stackrel{s}{\rightarrow}ÊR) \subseteq (( P \cap Q) 
\stackrel{s}{\rightarrow} R)$\\ 
$\bullet$ deduction theorem: $(P \cap R \subseteq Q \Rightarrow R \subseteq P \stackrel{s}{\rightarrow} Q)$
\\ \\ Ref. Hardegree 75,79; Herman Marsden Piziak 75; Malinowski 90; Blok et al 84
\par\noindent Is there a way out? YES! 
\par\noindent {\bf Idea} = Let us place the Sasaki Hook in its context, i.e. we take {\bf 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 {\bf the old orthodox moral} (adopted by many writers
including Birkhoff) should be questioned:
\begin{quote}``Quantum Logic can have no decent implication
since distribution fails"
\end{quote}
\end{slide}

\begin{slide}[7in,10in]  
\heading{Weak Modularity}
 {\bf In Physics:} The {\bf distributive identity} is a logical consequence of the
compatibility of observables (Birkhoff $\&$ von Neumannn)  \\
And the {\bf Weak modular identity} is a logical consequence of the
incompatibility of observables (so: the even in principle NOT-simultaneous
measurability).
 
$\forall P,Q \in {\cal L}$ and $P \subseteq Q$ then
$$ Q = P \sqcup (Q \cap \sim P)$$
 
{\bf Birkhoff $\&$ von Neumann's (modified) question}: ``what simple and plausible physical motivation is there for Weak Modularity?"  We look for an answer!

{\bf 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. 

{\bf 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.

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.

{\bf In Part II, we introduce WM as a frame condition!} This can be done in a dynamic quantum logic.


\end{slide}

\begin{slide}[7in,10in]  
\heading{Part II: Quantum Logic Revisited}
\centerline{{\it joint work with A. Baltag}}

{\bf QUANTUM LOGIC =} the negation-free part of test-only Quantum Dynamic Logic.  The {\bf syntax} consists of a
 set of {\it propositional formulas}, defined by:
$$\varphi ::= \bot \mid p \mid \varphi \wedge \varphi \mid [\varphi?] \varphi$$

{\it Orthocomplement} is defined  $\sim \varphi := [\varphi?]\bot$.\\

\medskip
{\bf Interpretation}:
\begin{itemize}
\item The {\it interpretation of a formula} $\varphi$ is a ``testable property"
$|\varphi|$, i.e. a closed linear subspace in a Hilbert space. 
\item The {\it interpretation of a test} $\varphi?$ is given by {\it
projective measurements} (projectors in a Hilbert Space).
\item The formula $[\varphi ?] \psi$ expresses the weakest precondition
$[\varphi?] \psi$ ensuring that (postcondition) $\psi$ will be
satisfied after executing $\varphi ?$ . This is nothing but the
so-called ``Sasaki hook".
\end{itemize}




\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}[7.3in,10.1in]  
\heading{Quantum Dynamic Logic} 

Our full logic has two sides: 
{\it propositions} $\varphi$ and {\it quantum
programs} $\pi$.

{\small
\beqa
\begin{array}{llllllll}
\varphi ::= & \bot & \mid p & \mid c & \mid \varphi \wedge \varphi & \mid \neg \varphi & \mid [\pi] \varphi & \\
\pi ::=  &\varphi? & \mid U & \mid \pi_{\varphi} & \mid \pi ; \pi & \mid \pi \cup \pi & \mid \pi^{*} & \mid \pi^{\dagger}
\end{array}
\eeqa}
The propositional logic 
has a classical negation $\neg$. In
addition to propositional variables $p$, we are given a set of {\it
propositional constants} $c\in {\cal C}$, denoting the
elements of a basis (of the underlying Hilbert space): so these
constants will represent mutually orthogonal states. The
weakest precondition formulas $[\pi]\psi$ are generalized here to
``quantum programs" $\pi$. Besides tests $\varphi?$, the
programs will include {\it unitary evolutions} $U\in {\cal
U}$, a  program  $\pi_{\varphi}$ (which is a program $\pi$ that affects only those states satisfying $\varphi$ and is the identity on the states orthogonal to $\varphi$); and regular
operations with programs (choice $\pi\cup \pi'$, sequential composition 
$\pi ; \pi'$,  and
iteration $\pi^*$), as well as an {\it adjoint} operation $\pi^{\dagger}$.

\end{slide}

\begin{slide}[7.3in,10.1in]  
\heading{Completeness}

The propositional logic (part) is Boolean: all the non-classical features
are pushed into the {\it 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).

\medskip

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

\bth
Our axiom system for the star-free fragment (i.e. without $\pi^*$) of this logic
is sound and {\bf complete} with respect to Hilbert spaces of
infinite dimension.
\Eth

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. 

\end{slide}



\begin{slide}[7.3in,10.1in]  
\heading{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.

\bigskip
\bigskip


\begin{enumerate}
\item Quantum Frames
\item Concrete Quantum Frames (based on Hilbert spaces)
\item Quantum Dynamic Algebras
\item Representation theorems
\end{enumerate}


\end{slide}





%%%%Quantum Logic (OML):
%%%%$$
%%%%\xymatrix@1{  & *++[oo][F-:<3pt>]{``test-only"\, Q.\, Frame}  \ar[d]
%%%%\\
%%%%& *++[oo][F-:<3pt>]{``test-only"\, Q.\, Dynamic\, Algebra}  }
%%%%$$
\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{slide}[7in,10in]  
\heading{Quantum Frames}

\noindent{\bf Definition:}
$(\Sigma, \{\stackrel{P?}{\to} \}_{P \in {\cal L} }, \{
\stackrel{U}{\to} \}_{U \in {\cal U} })$ , where
\begin{itemize}
\item $\Sigma$ is a set of ``states",  ${\cal L} \subseteq {\cal P}(\Sigma)$
is a collection of ``testable properties", ${\cal U}$ is
a collection of ``actions" (``unitary evolutions") 
\item $\{ \stackrel{U}{\to} \}_{U \in {\cal U} }$ is  a family of
binary relations $\stackrel{U}{\to} \subseteq \Sigma \times \Sigma$,
indexed by actions $U \in {\cal U}$  
\item $\{\stackrel{P?}{\to} \}_{P \in {\cal L} }$ 
is a family of binary relations  $\stackrel{P?}{\to} \subseteq \Sigma
\times \Sigma$,
indexed by properties $P \in {\cal L}$,
\quad
\end{itemize}
subject to some conditions (to be given later). 

To formulate these conditions, we need some
{\bf Definitions:}
\\
{\bf Measurement and orthogonality relations.} \\
\begin{tabular}{lll}
$s \stackrel{?}{\to} t$ & iff & $ s \stackrel{P?}{\to} t
\mbox{ for some } P \in {\cal L}$ \\
$s \perp t$ & iff & $ s\not\stackrel{?}{\to} t$
\end{tabular}




\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{slide}[7in,10in]  
\heading{Quantum Programs:}

{\bf Define:} The set of {\bf Quantum Programs} is the least family of 
binary relations ${\cal Q} \subseteq
{\cal P}(\Sigma \times \Sigma)$ which contains :
\\
(1) all tests $\{ \stackrel{P?}{\to}\}_{P \in {\cal L}}$ \\
(2) all actions $\{\stackrel{U}{\to} \}_{U
\in {\cal U}}$ and 
all converse actions $\stackrel{U^{-1}}{\to} \,\, := \,\, \stackrel{U}{\leftarrow}$ \\
and is closed under: \\
(3) {\it sequential composition} $\pi ; \pi'$, defined by
$$s \stackrel{\pi; \pi'}{\to} t \, \, \mbox{ iff } \, \,
s\stackrel{\pi}{\to}w\stackrel{\pi'}{\to} t \mbox{ for some } w\in\Sigma$$
(4) {\it choice} (=infinitary union) $\bigcup_i
\pi_i$, defined by
$$s \stackrel{\pi\cup \pi'}{\to} t \, \, \mbox{ iff } \, \,
\mbox{ either } s\stackrel{\pi}{\to}t \mbox{ or } 
\mbox{ either } s\stackrel{\pi'}{\to}t$$


\bigskip\par\noindent
{\bf Define:} {\bf Quantum maps} are the quantum programs obtained
form (1) and (2) using only sequential composition (3).  
(Note that quantum maps are partial functions.)
\end{slide}





\begin{slide}[7in,10in]  
\heading{Frame Axioms}


We list our conditions for quantum frames.


\medskip\par\noindent
0. {\bf Arbitrary Conjunctions}: If ${\cal L'}\subseteq {\cal L}$ then
$\bigcap {\cal L'}\in {\cal L}$. 


\bigskip\par\noindent
1. {\bf Partial Functionality.} 
{\it The outcome of a test is unique}:
\\ if $s \stackrel{P?}{\to} t $ and $s \stackrel{P?}{\to} v$ then $t = v$ 
\bigskip\par\noindent
2. {\bf Trivial Tests.} $\stackrel{\emptyset?}{\to} = \emptyset \mbox{ and } 
\stackrel{\Sigma?}{\to} = \{(s,s) \mid s \in \Sigma \}$ 
\bigskip\par\noindent
3. {\bf Adequacy.} {\it Testing a true property does not change the state}:\\
if $s \in P$ then $s \stackrel{P?}{\to} s$ 
\bigskip\par\noindent
4. {\bf Repeatability.} {\it Any property holds after it has been successfully tested}:\\
if $s \stackrel{P?}{\to}t$ then $t \in P$ \\
$$\xymatrix {*++[oo][F-:<3pt>]{s} \ar[r]^{P?} & *++[oo][F-:<3pt>]{t: P}  }
$$

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{slide}[7in,10in]  
\heading{Axioms continued}

\medskip\par\noindent
5. {\bf Compatibility Axiom}.\\
$P? ; Q? = Q? ; P?$ implies
$P?;Q? =(P \cap Q)?$ 
\bigskip\par\noindent

6. {\bf Proper Superposition Axiom.}
{\it Every two states can be properly superposed into a new state}:\\
$\forall s,t \in \Sigma: \exists w \in \Sigma$ s.t. $s \stackrel{?}{\to} w \stackrel{?}{\to} t$ \\



$$
\xymatrix{ & *++[oo][F-:<3pt>]{s}\\
& *++[oo][F-:<3pt>]{w }\ar @{..>}[u]^{?}
\\
& *++[oo][F-:<3pt>]{t} \ar @{..>}[u]^{?}  }
$$





\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{slide}[7in,10in]  
\heading{7. Self-Adjointness Axiom}


 If $s \stackrel{P?}{\to} w \stackrel{?}{\to} t$ then there exists some element $v
\in \Sigma$ s.t. $t \stackrel{P?}{\to} v \stackrel{?}{\to} s$. \\ \\
$$
\xymatrix{ *++[oo][F-:<3pt>]{s } \ar[r]^{P?} & *++[oo][F-:<3pt>]{w } \ar[d]^{?}\\
*++[oo][F-:<3pt>]{v } \ar@{..>} [u]^{?} & *++[oo][F-:<3pt>]{t} \ar@{..>} [l]_{P?} }
$$

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{slide}[7in,10in]  
\heading{Action Axioms} 


\medskip\par\noindent
8. {\bf Reversibility and Totality}.
{\it Actions are total bijective functions}:
$$\forall t \in \Sigma: \quad \exists ! s: s \stackrel{U}{\to} t $$
$$\forall s \in \Sigma: \quad \exists ! t: s \stackrel{U}{\to} t $$
%$s \stackrel{a^{\dagger}}{\to} t = t \stackrel{a}{\to} s$ \\ 

%$$\xymatrix {*++[oo][F-:<3pt>]{s:} \ar@{..>}@/^/ [rr]^{U} \ar @/_/[rr]^{U} &&  *++[oo][F-:<3pt>]{t: \varphi}  } $$ \\
%$$\xymatrix {*++[oo][F-:<3pt>]{s: \varphi} \ar @/^/ @(l,d)[]_{U ; U^{-1}} } $$ \\
%$$\xymatrix {*++[oo][F-:<3pt>]{s: \varphi} \ar @/^/ @(l,d)[]_{U^{-1} ; U} }
%$$


\medskip\par\noindent
9. {\bf Orthogonality Preservation}. {\it Actions preserve (non-)orthogonality:}\\
Let $s,t,s',t' \in \Sigma$ be s.t. $s \stackrel{U}{\to} s'$ and $ t \stackrel{U}{\to} t'$. \\
Then: $s \to t$ iff $s' \to t'$.
%{\tiny In other words: $s \to t$ iff $U(s) \to U(t)$, scalar product preservation: $<s \mid t> \not = 0$ iff $<U(s) \mid U(t)> \not = 0$}
\\ 
$$
\xymatrix{   *++[oo][F-:<3pt>]{s } \ar @{}[dr]|{<=>} \ar @{..>}[d]_{?} \ar[r]^{U} & *++[oo][F-:<3pt>]{s' } \ar @{..>}[d]^{?}\\
*++[oo][F-:<3pt>]{t } \ar[r]^{U} & *++[oo][F-:<3pt>]{t'} }
$$



\end{slide}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{slide}[7in,10in]  
\heading{Axioms continued}

\bigskip\par\noindent
10. {\bf Ample Unitary Group Axiom:} \\
For all states $s,t \in \Sigma$ there exists some action $U \in {\cal
U}$ such that: 
$$s \stackrel{U}{\to}
t$$
and
$$w \stackrel{U}{\to}w \, \, \, \, \mbox{ for all states } w \perp s,t$$

$$
\xymatrix{ *++[oo][F-:<3pt>]{w } \ar @/^/ @(l,d)[]_{U} \ar @/^/[r]|{+} \ar @/^/ [dr]|{\times} & *++[oo][F-:<3pt>]{s}\ar @{..>}[d]^{U} \\
& *++[oo][F-:<3pt>]{t} }
%\\
%& *++[oo][F-:<3pt>]{t} \ar @{..>}[u]  }
$$

\bigskip\par\noindent
11. {\bf Dimensionality}: \\
There exist an infinite set of states in $\Sigma$ such that each $s_i \not \to s_j$ for $i \not = j$.





\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{slide}[7in,10in]  
\heading{The Adjoint of a Program}

{\bf Define}  {\bf Adjoints}: $\dagger : {\cal Q} \to {\cal Q}$ by
induction:

\begin{enumerate}
\item $(P?)^{\dagger} \, = \, P?$ 
\item $U^\dagger \, = \, U^{-1}$, where $U^{-1}$ is the inverse function
(corresponding to the converse relation $ \stackrel{U}{\leftarrow}$)
\item $(U^{-1})^{\dagger} \, = \, U$ 
\item $(\pi;\sigma)^\dagger \, = \, \sigma^\dagger ; \pi^\dagger$ 
\item $(\bigcup_i \pi_i)^\dagger \, = \, \bigcup_i \pi_i^{\dagger}$
\end{enumerate}

Observe: $(\pi^\dagger)^\dagger = \pi$

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{slide}[7in,10in]  
\heading{Proposition:}

{\bf Adjointness for quantum programs} \\
Let $s,w,t \in \Sigma$:
If $s \stackrel{\pi}{\to} w \stackrel{?}{\to} t$ then there exists
some element $v \in \Sigma$ s.t. $t \stackrel{\pi^{\dagger}}{\to} v \stackrel{?}{\to} s$.
\\ \\ \\

$$
\xymatrix{ *++[oo][F-:<3pt>]{s } \ar[r]^{\pi} & *++[oo][F-:<3pt>]{w } \ar[d]^{?}\\
*++[oo][F-:<3pt>]{v } \ar@{..>} [u]^{?} & *++[oo][F-:<3pt>]{t} \ar@{..>} [l]_{\pi^{\dagger}} }
$$














\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{slide}[7in,10in]  
\heading{Orthocomplement, Precondition and Image}

For $P \subseteq \Sigma$ and
$\pi \subseteq \Sigma \times \Sigma$, let : 
$$\sim P := [P?] \bot$$
$$[\pi] P := \{ s \in \Sigma \mid \forall t ( s \stackrel{\pi}{\to} t
\Rightarrow t \in P)\}$$
(the {\it weakest precondition} ensuring $P$ after $\pi$) 
and 
$$\pi(P) := \sim [ \pi^{\dagger}] \sim P $$
\medskip

\bth \begin{itemize}
\item $\pi(P)$ is the image of $P$ under program $\pi$:
$$\pi(P) = \{t: s\stackrel{\pi}{\to} t \mbox{ for some } s\in P\}$$
\item {\bf Quantum Modus Ponens (=Weak Modularity)}:\\
 $P \cap [P?] Q \subseteq P \, \, \, $
\item {\bf Linearity of programs:}
$\overline{\pi(P)}
= \pi(\overline{P})$
\end{itemize}
\Eth
\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{slide}[7in,10in]  
\heading{Concrete Quantum Frames}

We can associate a QF to any Hilbert space ${\cal H}$, in a canonical manner:
$$(\Sigma, \{\stackrel{P?}{\to}\}_{P \in {\cal L}},
\{\stackrel{U}{\to}\}_{U \in {\cal U}})$$

\begin{itemize}
\item {\bf States $s\in \Sigma$:} one-dimensional subspaces of ${\cal H}$

\item{\bf Properties $P\in {\cal L}$:} sets $P\subseteq \Sigma$ of
states, such that $\bigcup P$ is a closed linear subspace of ${\cal H}$

\item{\bf Quantum Programs}: unions of linear maps.  Every linear operator
$F: {\cal H} \to {\cal H}$ induces a quantum 
map on states $\pi\subseteq \Sigma \times \Sigma$,
given by:
$$s\stackrel{\pi}{\to} t
\mbox{ iff } F(x)=y\not=0 \mbox{ for some } x\in s, y \in t$$
Quantum programs are arbitrary unions of such linear operators.

\item {\bf Quantum Tests $P?$:} the quantum maps induced
by the projectors $Proj_W$ on the closed subspace $W= \bigcup P$ associated to 
$P$.


\item{\bf Actions $U\in {\cal U}$}: the quantum maps induced by
unitary transformations of ${\cal H}$.

\end{itemize}


\end{slide}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}[7in,10in]
\heading{Representation Theorem}

\medskip

A {\it "concrete quantum frame"} is any subframe of the frame induced by 
a Hilbert space ${\cal H}$. 

\medskip

\bth
Every concrete QF is a QF.
\Eth
\medskip



\bth (Representation Theorem)
Every QF is isomorphic to a concrete QF.
\Eth

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{slide}[7in,10in]
\heading{Quantum Dynamic Algebras}
{\small Note: The algebraic semantics for PDL (cfr. Dynamic Frame) is
a {\bf dynamic algebra with tests and actions} (Pratt $\&$
 Kozen `79)}
\bigskip\par\noindent
A {\bf quantum dynamic algebra} is a structure:

$$(\, {\cal L}, 
{\cal Q}, {\cal U}, \bigwedge, \bigcup , ; , \dagger, 
? , [-]- \, )$$
consisting of: a set ${\cal L}$ of {\it "properties"}, a set
${\cal Q}$ of {\it "quantum programs"}, a set ${\cal U}\subseteq {\cal 
Q}$ of "actions"; and operations:\\
\begin{tabular}{ll}
$\bigwedge: {\mathcal P}({\cal L}){\to}{\cal L}$ &
$\bigcup: {\mathcal P}({\cal Q}){\to} {\cal Q}$ \\
$; \, : {\cal Q}\times {\cal Q}{\to} {\cal Q}$ & $?:{\cal L}{\to} {\cal
Q}$ \\
 $[ - ] -: {\cal Q}\times {\cal L}{\to } {\cal L}$ &
\end{tabular}\\
subject to a
number of conditions (to be given later).


\end{slide}


\begin{slide}[7in,10in]
\heading{Abbreviations}

$$\bot := \bigwedge {\cal L}$$
$$\sim:{\cal L}{\to} {\cal L},    \, \, \, \sim P := [P?]\bot$$
$$\top := \sim \bot$$
$$P\leq Q \mbox{ iff } P\wedge Q =P$$
$$P\perp Q \mbox{ iff } P \leq \sim Q$$
$$At({\cal L}) := \{P\in {\cal L}: \forall Q\in {\cal L}(\bot\not=Q \leq P \Rightarrow Q=P)\}$$
\end{slide}

\begin{slide}[7in,10in]
\heading{Axioms for QDA's}


\begin{itemize}
\item $({\cal L}, \bigwedge)$ is a complete lattice
\item $({\cal Q}, \bigcup, \top?)$ is a unital quantale having $\top?$ 
as its unit: $\top? ; \pi = \pi ; \top? = \pi$.
\item $\bot ? \leq \pi \, \,$  (i.e. $\bot_{\cal L} ? = \bot_{\cal Q}$)
\item $ \pi ; \bot ? = \bot? ; \pi = \bot ?$
\item ${\cal Q}$ is generated by ${\cal U}\cup \{P? : P \in {\cal L}\}$ using $;$ and $\bigcup$.
\item {\it Normality}: $[\pi] \top = \top$
\item {\it Distributivity}: $[\pi] ( \bigwedge_i P_i) = \bigwedge_i [\pi] P_i$
\item {\it Choice}: $[ \bigcup_i \pi_i] P = \bigwedge_i [\pi_i] P$
\item {\it Composition}: $[\pi ; \sigma]P = [\pi][\sigma] P$
\item {\it Partial Functionality for Tests}: \\
if $Q\in At({\cal L})$ then $P? (Q)\in
At({\cal L})\cup\{\bot\}$
\item {\it Repeatability}: $[P?]P = \top, $
\item Adequacy : $P \wedge Q \leq [Q?] P$ and $[\top?]P \leq P$
\item {\it Compatibility}:
If $P? ; Q? = Q? ; P?$ then $P? ; Q? = (P \cap Q) ?$
\item {\it Proper Superpositions}: \\
if $P, Q\not=\bot$ then there exist $R,
S\in {\cal L}$ such that $R?; S? (P)\wedge Q\not=\bot$.
\item {\it Adjointness Axiom}:  $P \leq [\pi ] \sim[ \pi^{\dagger}]\sim P$
\item {\it Adjoints} : 
$P?^{\dagger} = P? $, \\
$(\pi ; \sigma)^{\dagger} = \sigma^{\dagger}; \pi^{\dagger} , \, \, \, \, (\bigcup_i \pi_i)^{\dagger} = 
\bigcup_i( \pi_i^{\dagger})$ 
\item {\it Total Functionality for Actions}: if $Q\in At({\cal L})$ then $U (Q)\in
At({\cal L})$
\item {\it Reversibility of Actions}: $U; U^{\dagger} = U^{\dagger}; U = T?$
\item {\it Ample Unitary Group Axiom}: if $P, Q\not= \bot$ then there exists
some $U\in {\cal U}$ such that:
$$U(P) \wedge Q \not= \bot$$
$$U(R) \leq R \mbox{ for all } R\perp P, Q$$ 
\item {\it Dimensionality }: \\
$\exists P_i \in {\cal
L}$ s.t. $P_i\perp P_j$ for all $i\not=j$. 


\end{itemize}
\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{slide}[7in,10in]
\heading{Representation Theorems}

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


\noindent{\bf Consequences}:
The two Representation theorems imply:
\begin{itemize}
\item Every QDA is isomorphic to a "concrete" QDA, i.e. one based on a Hilbert 
space.
\item Completeness for our Quantum Dynamic logic.

\end{itemize}

\end{slide}

\begin{slide}[7in,10in]
\heading{Representation Theorems}

{\bf Main Point:}  
I presented a Quantum Dynamic Logic ($QDL$), designed as a {\it logical
calculus for quantum information flow}. This is a quantum
version of $PDL$, i.e. a logic equipped with dynamic
modalities to deal with {\it quantum measurements} (``tests"), and
{\it unitary evolutions}. 

\heading{Claims}


\noindent{\bf Claim 1:}
Standard {\bf Quantum Logic} is the negation-free ``test-only" fragment of
Quantum Dynamic Logic.
Sasaki hook is re-discovered as a standard {\it dynamic modality}: the {\it
weakest precondition}.

\medskip

\noindent{\bf Claim 2 :}
We have a {\bf Frame Condition} for Weak Modularity, giving a
natural ``operational" meaning to this axiom.


\medskip

\noindent{\bf Claim 3 :}
We have a {\it Completeness result for Hilbert spaces}.  Our proofs use the representation theorem of C. Piron added with the improvement of M.P. Sol\'er.

\newpage

Some REFS:

{\small 
$\bullet$ For compound systems: \\
A. Baltag and S. Smets ``The Logic of Quantum Programs", \\
{http://philsci-archive.pitt.edu/archive/00001799/}

$\bullet$ For single systems:Ê\\
A. Baltag and S. Smets ``The Logic of Quantum Actions" upcoming

$\bullet$ 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/


$\bullet$ Most recent book on QL: \\
M. Dalla Chiara, R. Giuntini and R. Greechie: {\it Reasoning in Quantum Theory}, Kluwer 2004

$\bullet$ Hilbert Spaces: \\
S.K. Berberian: {\it Introduction to Hilbert Space}, Chelsea Publishing Company, 1961
}

\end{slide}

\end{document}




















 