\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{quantum logic}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{physics}{}\paragraph*{{Physics}}\label{physics}

[[!include physicscontents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{History}{History and Critique}\dotfill \pageref*{History} \linebreak
\noindent\hyperlink{approaches}{Approaches}\dotfill \pageref*{approaches} \linebreak
\noindent\hyperlink{birkhoffvon_neumann_quantum_logic}{Birkhoff-von Neumann quantum logic}\dotfill \pageref*{birkhoffvon_neumann_quantum_logic} \linebreak
\noindent\hyperlink{logic_of_quantales}{Logic of Quantales}\dotfill \pageref*{logic_of_quantales} \linebreak
\noindent\hyperlink{linear_logic}{Linear logic}\dotfill \pageref*{linear_logic} \linebreak
\noindent\hyperlink{bohr_toposes}{Bohr toposes}\dotfill \pageref*{bohr_toposes} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{literature}{Literature}\dotfill \pageref*{literature} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

Broadly speaking, \emph{quantum logic} is meant to be a kind of [[formal logic]] that is to traditional formal logic as [[quantum mechanics]] is to [[classical mechanics]]: a formal framework which is supposed to be able to \emph{express} the statements whose [[semantics]] is the totality of all what is verifiable by [[measurement]] in a [[quantum system]] ([[quantum measurement]]).

In its traditional and default meaning due to (\hyperlink{BirkhoffvonNeumann36}{Birkhoff-vonNeumann 1936}) ``quantum logic'' refers specifically to the [[orthocomplemented lattice]] of closed linear subspaces of a [[Hilbert space]] [[space of quantum states|of quantum states]]. Later it was proposed (\hyperlink{Yetter90}{Yetter 90}, \hyperlink{Pratt92}{Pratt 92}, \hyperlink{AbramskyDuncan05}{Abramsky-Duncan 05}, \hyperlink{Girard11}{Girard 11}) that a better way to think of the BvN quantum lattices is as the [[propositions]] in [[linear logic]] (\hyperlink{Girard}{Girard 87}), the [[categorical logic]] of [[symmetric monoidal categories]].

There is also the proposal (\hyperlink{HeunenLandsmanSpitters07}{Heunen-Landsman-Spitters 07}) that quantum logic should be understood as being the [[internal logic]] of [[Bohr toposes]].

In [[quantum computing]] the quantum analog of classical [[logic gates]] are called \emph{[[quantum logic gates]]}.

\hypertarget{History}{}\subsection*{{History and Critique}}\label{History}

Typically in the literature the term ``quantum logic'' is taken to refer very specifically to the first proposal for such a formalization that was given by (\hyperlink{BirkhoffvonNeumann36}{Birkhoff-von Neumann 1936}). In this proposal given a [[quantum mechanical system]] with a [[Hilbert space]] [[space of states|of states]], the logical [[propositions]] about the system are taken to correspond to (the [[projections]] to) [[closed subspaces]], with [[implication]] given by inclusion of such subspaces. Hence Birkhoff-von Neumann quantum logic is given by the [[lattice]] of closed linear subspaces of Hilbert spaces (regarded as an [[Hilbert lattice]]).

This formalization is often understood as being the default meaning of ``quantum logic''. But the proposal has later been much criticised, for its lack of key properties that one would demand of a [[formal logic]].

For instance in (\hyperlink{Abramsky09}{Abramsky 09}) it is called a ``non-logic''

\begin{quote}%
The term quantum logic is usually understood in connection with the 1936 Birkhoff-von Neumann proposal to consider the (closed) linear subspaces of a Hilbert space ordered by inclusion as the formal expression of the logical distinction between quantum and classical physics. While in classical logic we have deduction, the linear subspaces of a Hilbert space form a non-distributive lattice and hence there is no obvious notion of implication or deduction. Quantum logic was therefore always seen as logically very weak, or even as a non-logic. In addition, it has never given a satisfactory account of compound systems and entanglement.


\end{quote}
Here by ``no [[deduction]]'' is meant ``no [[deduction theorem]]''.

And for example in (\hyperlink{HeunenLandsmanSpitters07}{Heunen-Landsman-Spitters 07, p. 4}) it says the following.

\begin{quote}%
Attractive and revolutionary as this spatial quantum ``logic'' may appear it faces severe problems. The main logical drawbacks are:

\begin{enumerate}%
\item Due to its lack of distributivity, quantum `logic' is difficult to interpret as a logical structure.
\item In particular, despite various proposals no satisfactory implication operator has been found (so that there is no deductive system in quantum logic).
\item Quantum `logic' is a propositional language; no satisfactory generalization to predicate logic has been found.

\end{enumerate}
Quantum logic is also problematic from a physical perspective. Since (by various theorems and wide agreement) quantum probabilities do not admit an ignorance interpretation, $[0, 1]$-valued truth values attributed to propositions by pure states via the Born rule cannot be regarded as sharp (i.e. \{0, 1\}-valued) truth values muddled by human ignorance. This implies that, if $X = [a \in \Delta]$ represents a quantum-mechanical proposition, it is wrong to say that either $x$ or its negation holds, but we just do not know which of these alternatives applies. However, in quantum logic one has the law of the excluded middle in the form $x \vee x^\perp = 1$ for all $x$. Thus the formalism of quantum logic does not match the probabilistic structure of quantum theory responsible for its empirical content.


\end{quote}
But notice that one may argue that the first three points here are squarely resolved by thinking of BvN-quantum logic as embedded into [[linear logic]], we come back to this in a moment. Concerning the last point one might argue that the propositions in BvN-quantum logic concern the [[quantum measurement]]-outcomes (only), for which, at least in some [[interpretation of quantum mechanics|interpretations]], it does make sense to speak of a definite result.

In (\hyperlink{Girard11}{Girard 11, page xii}) it says:

\begin{quote}%
Among the magisterial mistakes of logic, one will first mention quantum logic, whose ridiculousness can only be ascribed to a feeling of superiority of the language -- and ideas, even bad, as soon as they take a written form -- over the physical world. Quantum logic is indeed a sort of punishment inflicted on nature, guilty of not yielding to the prejudices of logicians\ldots{} just like Xerxes had the Hellespont -- which had destroyed a boat bridge -- whipped.


\end{quote}
For more and more objective criticism see (\hyperlink{Girard11}{Girard 11, section 17}).

Girard had introduced the class of [[formal logic]] systems called \emph{[[linear logic]]} and it has been argued that [[linear logic]] and more generally \emph{[[linear type theory]]} does faithfully capture the essence of [[quantum mechanics]] (\hyperlink{Yetter90}{Yetter 90}. \hyperlink{Pratt92}{Pratt 92}, \hyperlink{AbramskyDuncan05}{Abramsky-Duncan 05}, \hyperlink{Duncan06}{Duncan 06}), see (\hyperlink{BaezStay09}{Baez-Stay 09}) for an introductory exposition). This is due to the fact that the [[categorical semantics]] of linear logic is in [[symmetric monoidal categories]] such as those used in the description of [[finite quantum mechanics in terms of dagger-compact categories]]. In particular the [[category]] of (finite dimensional) [[Hilbert spaces]] whose [[subobjects]]/[[propositions]] form the Birkhoff-von Neumann style quantum logic does interpret [[linear logic]].

This is stated explicitly for instance in (\hyperlink{Pratt92}{Pratt 92, p.4}):

\begin{quote}%
These objections are overcome in the extension of quantum logic to linear logic as a dynamic quantum logic.


\end{quote}
Notice that the [[subobjects]] in a category of (finite dimensional) [[Hilbert spaces]], and hence the [[propositions]] in the [[categorical logic]] of Hilbert spaces, are the (closed) linear subspaces. Therefore Birkhoff-von Neumann quantum logic is indeed subsumed as a fragment of linear logic. This (obvious) fact was highlighted in (\hyperlink{Crown75}{Crown 75}) and then later with more of [[categorical logic]] in place and emphasizing [[dagger-category|dagger]]-structures in (\hyperlink{Heunen08}{Heunen 08}, \hyperlink{Harding08}{Harding 08} \hyperlink{HeunenJacobs09}{Heunen-Jacobs 09}, \hyperlink{CoeckeHeunenKissinger13}{Coecke-Heunen-Kissinger 13}). Also (\hyperlink{CCGP09}{CCGP 09, section 9.3}):

\begin{quote}%
both orthologic (or weakenings thereof) and linear logic share the failure of lattice distributivity. In particular, the fragment of linear logic that includes just negation and the additive connectives is nothing but a version of the paraconsistent quantum logic PQL.


\end{quote}
That seems to make much of the above-listed criticism appear in a different light. For instance there is also a natural notion of [[dependent linear type theory]] and that does yield a well-behaved kind of [[predicate logic]] with [[quantifiers]] for linear logic.

\hypertarget{approaches}{}\subsection*{{Approaches}}\label{approaches}

\hypertarget{birkhoffvon_neumann_quantum_logic}{}\subsubsection*{{Birkhoff-von Neumann quantum logic}}\label{birkhoffvon_neumann_quantum_logic}

It is based on the setting the [[Hilbert lattice]] (of closed suspaces of a Hilbert space) to represent the set of propositions of quantum system.

\ldots{}

[[conjunction]] is given by intersection of two linear subspaces

[[disjunction]] however is given by forming the [[linear space]] of two linear subspaces. Hence [[quantum states]] in the conjunction $A \vee B$ may be [[linear combinations]] of states in $A$ and $B$. This is an incarnation of [[superposition principle]] of [[quantum mechanics]].

as a result, the BvN disjunction does not [[distributivity|distribute]] over conjunction, and hence the BvN lattice is not a [[distributive lattice]].

[[negation]] is given by forming [[orthogonal complement]]

[[Hilbert lattice]]

\hypertarget{logic_of_quantales}{}\subsubsection*{{Logic of Quantales}}\label{logic_of_quantales}

On top of the above [[lattice]] of lineat subspaces, take into account that it carries naturally a [[tensor product]]. That makes it a \emph{[[quantale]]}.

\hypertarget{linear_logic}{}\subsubsection*{{Linear logic}}\label{linear_logic}

More generally, if we do not just consider the monoidal [[poset]] (quantale) but more generally [[symmetric monoidal categories]] then this is \emph{[[linear logic]]}, \emph{[[linear type theory]]}

(\ldots{})

\emph{[[quantum computing]]}.

(\ldots{})

The linearity of the logic, hence the absence of a [[diagonal]] in its [[categorical semantics]], corresponds to the [[no-cloning theorem]] of [[quantum physics]]

\hypertarget{bohr_toposes}{}\subsubsection*{{Bohr toposes}}\label{bohr_toposes}

See at \emph{[[Bohr topos]]} for more.

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[effect algebra]]


\item [[quantum probability]]


\item [[interpretation of quantum mechanics]]


\item [[order-theoretic structure in quantum mechanics]]

\begin{itemize}%
\item [[Kochen-Specker theorem]]


\item [[Alfsen-Shultz theorem]]


\item [[Harding-Döring-Hamhalter theorem]]



\end{itemize}

\item [[Fell's theorem]]


\item [[Gleason's theorem]]


\item [[Wigner theorem]]


\item [[Bell's theorem]]


\item [[Bub-Clifton theorem]]


\item [[Kadison-Singer problem]]


\item [[collapse of the wave function]]


\item [[qbit]]


\item [[quantum circuit]]


\item [[linear logic]],


\item [[quantum mechanics]]

\begin{itemize}%
\item [[quantum computing]]


\item [[beable]]



\end{itemize}

\item [[computable physics]]


\item [[quantale]],


\item [[Bohr topos]]



\end{itemize}
\hypertarget{literature}{}\subsection*{{Literature}}\label{literature}

General introductions and surveys include

\begin{itemize}%
\item Wikipedia, \emph{\href{http://en.wikipedia.org/wiki/Quantum_logic}{Quantum logic}}


\item Stanford encyclopaedia of philosophy, \emph{\href{http://plato.stanford.edu/entries/qt-quantlog}{Quantum logic and probability theory}}


\item Kurt Engesser, Dov M. Gabbay, Daniel Lehmann (eds.) \emph{Handbook of Quantum Logic and Quantum Structures: Quantum Logic}, 2009 North Holland


\item I. Pitowsky, \emph{Quantum probability --- quantum logic}, Springer Lecture Notes in Physics \textbf{321}


\item P. Pt\'a{}k and S. Pulmannov\'a{}, \emph{Orthomodular structures as quantum logics}, ser. Fundamental theories of physics. Kluwer Academic Publishers, 1991.



\end{itemize}
A bibliography of hundreds of works up to 1992 is

\begin{itemize}%
\item Mladen Pavii, \emph{Bibliography on quantum logics and related structures}, \href{http://www.irb.hr/users/mpavicic/papers-ps-pdf/quantum-logic/1992-int-j-theor-phys-1.pdf}{pdf}.

\end{itemize}
The original article on quantum logic is

\begin{itemize}%
\item [[Garrett Birkhoff]], [[John von Neumann]], \emph{The logic of quantum mechanics}, Annals of Mathematics, 37: 823-843 (1936)

\end{itemize}
Further discussion of this includes

\begin{itemize}%
\item A. Gleason, \emph{Measures on the closed subspaces of a Hilbert space}, Journal of Mathematics and Mechanics \textbf{6}: 885-893 (1957)


\item Samuel S. Holland Jr., \emph{Orthomodularity in infinite dimensions; a theorem of M. Sol\`e{}r}, Bull. Amer. Math. Soc. (N.S.) \textbf{32} (1995) 205-234, \href{http://arxiv.org/abs/math/9504224}{arXiv:math.RA/9504224}



\end{itemize}
Discussion of [[categorical logic]] in [[symmetric monoidal categories]] and hence of [[linear logic]] as quantum logic is in

\begin{itemize}%
\item G.D. Crown, \emph{On some orthomodular posets of vector bundles}. Journ. of Natural Sci. and Math., 15(1-2):11--25, 1975.

\end{itemize}
\begin{itemize}%
\item [[Jean-Yves Girard]], \emph{Linear logic}, Theoretical Computer Science 50:1, 1987. (\href{http://iml.univ-mrs.fr/~girard/linear.pdf}{pdf})

\end{itemize}
(\hyperlink{Girard}{Girard 87} introduces [[linear logic]] nad suggests a possible relation to [[quantum physics]], but remains undecided on thatM on p. 7 it says: ``One of the wild hopes that this suggests is the possibility of a direct connection with quantum mechanics\ldots{} but let's not dream too much!'')

\begin{itemize}%
\item [[David Yetter]], \emph{Quantales and (noncommutative) linear logic}, Journal of Symbolic Logic 55 (1990), 41-64.

\end{itemize}
(\hyperlink{Yetter90}{Yetter 90}) observes the the relation of linear logic to [[quantales]], which have otherwise been proposed as providing a quantum logic.)

\begin{itemize}%
\item [[Vaughan Pratt]], \emph{Linear logic for generalized quantum mechanics}, in Proc. of \emph{Workshop on Physics and Computation (PhysComp'92)} (\href{http://boole.stanford.edu/pub/ql.pdf}{pdf}, \href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.137.7817}{web})

\end{itemize}
(\hyperlink{Pratt92}{Pratt 92} is maybe the first to say fully that linear logic is a good kind of quantum logic.=

\begin{itemize}%
\item [[Samson Abramsky]], [[Ross Duncan]], \emph{A Categorical Quantum Logic} (\href{http://arxiv.org/abs/quant-ph/0512114}{arXiv:quant-ph/0512114})

\end{itemize}
\begin{itemize}%
\item [[Ross Duncan]], \emph{Types for quantum mechanics}, 2006 (\href{http://homepages.ulb.ac.be/~rduncan/papers/rduncan-thesis.pdf}{pdf}, \href{http://www.cs.ox.ac.uk/people/ross.duncan/talks/2005/pps-22-05-2005.pdf}{slides})

\end{itemize}
(This highlights more [[linear type theory]] and its use in quantum theory.)

\begin{itemize}%
\item [[Chris Heunen]], \emph{Quantifiers for quantum logic} (\href{http://arxiv.org/abs/0811.1457}{arXiv:0811.1457})

\end{itemize}
\begin{itemize}%
\item [[John Harding]], \emph{A link between quantum logic and categorical quantum mechanics}, Int J Theor Phys (2009) 48: 769--802


\item [[Chris Heunen]], [[Bart Jacobs]], \emph{Quantum Logic in Dagger Kernel Categories}, Order, July 2010, Volume 27, Issue 2, pp 177-212, (\href{http://arxiv.org/abs/0902.2355}{arXiv:0902.2355})



\end{itemize}
\begin{itemize}%
\item Gianpiero Cattaneo, Maria Luisa Dalla Chiara, Roberto Giuntini and Francesco Paoli, section 9 of \emph{Quantum Logic and Nonclassical Logics}, p. 127 in Kurt Engesser, Dov M. Gabbay, Daniel Lehmann (eds.) \emph{Handbook of Quantum Logic and Quantum Structures: Quantum Logic}, 2009 North Holland


\item [[Samson Abramsky]], \emph{Temperley-Lieb Algebra: From Knot Theory to Logic and Computation via Quantum Mechanics}, In Goong Chen, Louis Kauffman, and Sam Lomonaco (eds.), \emph{Mathematics of Quantum Computing and Technology}, pages 415--458. Taylor and Francis, 2007. (\href{http://arxiv.org/abs/0910.2737}{arXiv:0910.2737})


\item [[Jean-Yves Girard]], \emph{[[Lectures on Logic]]}, European Mathematical Society 2011



\end{itemize}
\begin{itemize}%
\item Ugo Dal Lago, Claudia Faggian, \emph{On Multiplicative Linear Logic, Modality and Quantum Circuits} (\href{http://arxiv.org/abs/1210.0613}{arXiv:1210.0613})

\end{itemize}
\begin{itemize}%
\item [[Bob Coecke]], [[Chris Heunen]], [[Aleks Kissinger]], \emph{Compositional Quantum Logic} (\href{http://arxiv.org/abs/1302.4900}{arXiv:1302.4900})

\end{itemize}
That therefore in particular [[categories of cobordisms]] (the domains of [[FQFT|functorial quantum field theory]]) interpret quantum logic qua [[linear logic]] has been highlighted in

\begin{itemize}%
\item [[Sergey Slavnov]], \emph{From proof-nets to bordisms: the geometric meaning of multiplicative connectives}, Mathematical Structures in Computer Science / Volume 15 / Issue 06 / December 2005, pp 1151 - 1178

\end{itemize}
\begin{itemize}%
\item [[John Baez]], [[Mike Stay]], \emph{Physics, topology, logic and computation: a rosetta stone}, (\href{http://arxiv.org/abs/0903.0340}{arxiv/0903.0340}); in ``New Structures for Physics'', ed. Bob Coecke, Lecture Notes in Physics \textbf{813}, Springer, Berlin, 2011, pp. 95-174

\end{itemize}
Discussion of [[Fock space]]-type free [[quantum field theory]] in [[linear logic]] is in

\begin{itemize}%
\item [[Marcelo Fiore]], \emph{Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic} (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.109.2328}{web})

\end{itemize}
The proposal that the [[internal logic]] of [[Bohr toposes]] is a good notion of quantum logic is made in

\begin{itemize}%
\item [[Chris Heunen]], [[Klaas Landsman]], [[Bas Spitters]], \emph{A topos for algebraic quantum theory}, Comm. Math. Phys. 291:63--110, 2009, free access \href{http://dx.doi.org/10.1007/s00220-009-0865-6}{doi}, \href{http://arxiv.org/abs/0709.4364}{arXiv:0709.4364}

\end{itemize}
\begin{itemize}%
\item [[Steve Vickers]], slides from Midland Grad. School 2010, quantum topos theory, \href{http://www.cs.bham.ac.uk/~sjv/teaching/MGS2010}{web}, most relevant part IV: \href{http://www.cs.bham.ac.uk/~sjv/teaching/MGS2010/slides4.pdf}{pdf}

\end{itemize}
See also

\begin{itemize}%
\item [[Yuri Manin]], \emph{A course in mathematical logic}, Springer


\item .. ,    , 1966, 162 .


\item A. Sudbery, \emph{Quantum mechanics and the particles of nature}, An outline for mathematicians, Camb. Univ. Press 1986


\item Stanford Encyclopedia of Philosophy, \href{http://plato.stanford.edu/entries/qt-nvd}{qm: von Neumann vs. Dirac},



\end{itemize}
[[!redirects quantum logics]]



\end{document}