# Orthologic and Quantum Logic: Models and Computational Elements.

Abstract: Motivated by a growing need to understand the computational potential of quantum devices we suggest an approach to the relevant issues via quantum logic and its model theory. By isolating such notions as quantum parallelism and interference within a model-theoretic setting, quite divorced from their customary physical trappings, we seek to lay bare their logical underpinnings and possible computational ramifications.In the first part of the paper, a brief account of the relevant model theory is given, and some new results are derived. In the second part, we model the simplest classical gate, namely the N-gate, propose a quantization scheme (which translates between classical and quantum models, and from which emerges a logical interpretation of the notion of quantum parallelism), and apply it to the classical N-gate model. A class of physical instantiations of the resulting quantum N-gate model is also briefly discussed.

Categories and Subject Descriptors: F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic-modal logic, model theory

General Terms: Theory

Additional Key Words and Phrases: Hilbert spaces, quantum computing, quantum logic, quantum physics

1. Introduction

Orthologic is a weakening of classical logic that results when conjunction is not assumed to distribute over disjunction. (Material implication in orthologic then also necessarily runs against the classical grain and we shall not address this vexed question in the present paper.) This kind of logic--in which conjunction and negation retain their usual connotations--might have preceded ordinary classical logic if classical logicians had failed to notice that distributivity among conjunction and disjunction seems to hold, at least in their experience of the ordinary macroscopic world. This century (the twentieth at the time of writing) has afforded logicians (and others) some experience of the microscopic or quantum world, and "logic" there seems to refute the distributive law. Opinion is divided (and subdivided) over such issues as whether or not this discovery entails a need to revise "ordinary" logic; whether or not this so-called "quantum logic" is really logic or is merely an algebraic simulacrum of logic so that its disjunction, for example, is not the disjunction, etc. These debates beg deeper questions concerning the nature and reality of those entities that are presumed to provide the subject matter of quantum logic. Such issues are by no means settled, even in the domain of quantum theory proper.

Motivated by a growing need to understand the computational potential of quantum devices it is our intention in this paper to prepare an approach to some of these problems through the purely formal direction of orthologic and its model theory. There are of course no epistemological problems while we remain within the scope of pure model theory, and metaphysical catastrophes can be avoided, or at least postponed. At the same time, the purely logical aspects of such puzzlements as quantum superposition, interference and entanglement--notions that cause so much disquiet in the minds of classical thinkers--can be brought to the fore, and their logical features examined without recourse to instantiation in the particular subclass of models that constitutes the arena of quantum physics proper.

As remarked above, our major motivation for conducting this exercise was provided by the advent of "quantum" computers and "quantum" computation: indeed, it is precisely the notions of quantum superposition, etc., that lie at the heart of the current interest in the feasibility of quantum computing. Proponents of this idea hope to harness the massive and instantaneous parallelism inherent in quantum systems to computational ends.

By isolating these notions within a model-theoretic setting quite divorced from their customary complex physical trappings, we seek to lay bare their logical underpinnings and possible computational ramifications.

The paper is in two parts. In the first part, we discuss orthologic as a propositional system and develop its (known) model theory using a set of modal identities collected together in Section 2.2. A different (and apparently new) characterization of orthologic is obtained in Section 2.4 by slightly modifying a forcing method of J. L. Bell. This result is somewhat peripheral to the main concerns of this paper, but is included for the sake of completeness and because of its intended use in a sequel. In Section 2.5, we offer another proof of the modal translation theorem for orthologic, which will be our main tool in the second part. The first part ends with a brief discussion of quantum logic proper, which touches on issues of logical realism in the light of some recent work of C. J. Isham and J. Butterfield.

In the second part, we develop a model-theoretic approach to the notion of a computational element or (reversible) gate. In Section 3.1, we treat the simplest classical case of such a gate, namely the so-called N-gate, and then specify at the model-theoretic level how a minimal quantization should proceed (Section 3.2). The quantization process exploits the modal translation theorem and permits distinctions to be drawn between classical and quantum computational paradigms at the (modal) logic level. One of these distinctions entails the emergence of the phenomenon known as "quantum parallelism", which is discussed at some length in this setting. These ideas are then applied in Section 3.3 to the problem of quantizing the classical N-gate, and a class of physical instantiations of the resulting quantum N-gate model is briefly discussed.

2. Orthologic and Quantum Logic

2.1. ORTHOLOGIC AS A DEDUCTIVE SYSTEM. The presentation of (first-order) orthologic as a deductive system seems first to have been achieved by Goldblatt [1974]; see also Bell [1983]. The primitive symbols are:

(i) a denumerable collection [[Phi].sub.0] of propositional variables [a.sub.1], [a.sub.2], ...;

(ii) the connectives ~ ("negation") and ?? ("conjunction"); and

(iii) parentheses.

The set [Phi] of (well-formed) formulae is constructed from these in the usual way. Elements of [Phi] will be denoted by lowercase Greek characters [Alpha], [Beta], ...

Since there is no implication sign in [Phi] a formal deductive calculus is based on the notion of a (binary) sequent. This is an expression of the form

(2.1.1) [Alpha] ?? [Beta]

for [Alpha], [Beta] [element of] [Phi], the intended reading of which is that [Beta] may be inferred from [Alpha]. Certain sequents are designated as axioms, namely, for any formulas [Alpha], [Beta]:

(A1) [Alpha] ?? [Alpha]

(A2) [Alpha] ?? [Beta] ?? [Alpha]

(A3) [Alpha] ?? [Beta] ?? [Beta]

(A4) [Alpha] ?? ~~ [Alpha]

(A5) ~~ [Alpha] ?? [Alpha]

(A6) [Alpha] ?? ~ [Alpha] ?? [Beta]

and there are three rules of inference, namely:

(A7) if [Alpha] ?? [Beta] and [Beta] ?? [Gamma] then [Alpha] ?? [Gamma]

(A8) if [Alpha] ?? [Beta] and [Alpha] ?? [Gamma] then [Alpha] ?? [Beta] ?? [Gamma]

(A9) if [Alpha] ?? [Beta] then ~ [Beta] ?? ~ [Alpha]

A disjunctive connective may be introduced according to the definition

(2.1.2) [Alpha] ?? [Beta] [equivalent] ~((~[Alpha]) ?? (~[Beta]

and dual forms of (A2), (A3), (A6), and (A8) follow.

A string [s.sub.1]; [s.sub.2]; ...; [s.sub.n] of sequents is called a proof of its last member [s.sub.n] if each [s.sub.i] is either an axiom or follows from some preceding sequent through the use of one of the rules of inference.

If there exists a proof of a sequent [Alpha] ?? [Beta], we write

(2.1.3) [Alpha] [[assertion sign].sub.o] [Beta]

and say that [Beta] is deducible from a in orthologic.

If [Alpha] [[assertion sign].sub.o] [Beta] for any formula [Alpha], we say that [Beta] is a theorem of orthologic or an orthotheorem, and we write

(2.1.4) [[assertion sign].sub.o] [Beta]

(Note that this condition is equivalent to [Alpha] ?? ~[Alpha] [[assertion sign].sub.o] [Beta].)

We recall that there are completeness theorems for ordinary propositional logic (PC) and intuitionistic logic (IL) which assert connections between the analogous forms of deducibility in these logics and the behavior of morphisms, or valuations, of formulas into certain classes of lattices: Boolean algebras in the case of PC and Heyting algebras in the case of IL. There is an analogous characterization of orthologic, involving a class of lattices called ortholattices.

An ortholattice is a bounded lattice <L, ??, ??, [0.sub.L], [1.sub.L], '> where ()' is a unary operation called orthocomplementation satisfying:

complementarity: [inverted] Aa [element of] L, a ?? a' = [0.sub.L], a ?? a' = [1.sub.L]

unitarity: a" = a

antitonicity: a ?? b iff b' ?? a'

It is easily shown that any ortholattice satisfies De Morgan's laws, for example,

(2.1.5) a ?? b = (a' ?? b')'.

An ortholattice is said to be complete if arbitrary subsets have meets and joins: a complete ortholattice satisfies the complete generalizations of the De Morgan laws.

Examples of ortholattices include all Boolean algebras and lattices of closed subspaces of Hilbert spaces.

Given an ortholattice L, a function [v.sub.L].: [[Phi].sub.0] [right arrow] L determines a valuation upon [[Phi] via the recursive definitions:

(2.1.6) [v.sub.L] ([Alpha] ?? [Beta] = [v.sub.L] ([Alpha]) ?? [v.sub.L] ([Beta]

(2.1.7) [v.sub.L] (~[Alpha] = [v.sub.L] ([Alpha])'

The algebraic characterization theorem for orthologic may be stated as follows:

THEOREM 2.1.1 [GOLDBLATT 1974; BELL 1983].

[Gamma] [[assertion sign].sub.o] [Alpha] iff [v.sub.L] ([Gamma]) ?? [v.sub.L] ([Alpha]) for all ortholattices L and all valuations [v.sub.L].

COROLLARY 2.1.1. [[assertion sign].sub.o] [Alpha] iff [v.sub.L] ([Alpha]) = [1.sub.L] for all ortholattices L and all valuations [v.sub.L].

A pair A [equivalent] <L, [v.sub.L]> may be called an algebraic orthomodel (for orthologic), and a formula [Alpha] deemed valid in this model if [v.sub.L] ([Alpha]) = [1.sub.L]. Then the above corollary may be stated as:

(2.1.8) [[assertion sign].sub.o] [Alpha] iff [Alpha] is valid in every algebraic orthomodel.

The following corollary follows immediately, since Boolean algebras are ortholattices.

COROLLARY 2.1.2. If [[assertion sign].sub.o] [Alpha], then [Alpha] is a theorem of PC.

(The converse is clearly false.)

A canonical class of examples of ortholattices is obtained as follows: An orthogonality space F = <W, [perpendicular to]> comprises a set W and a binary relation [perpendicular to] [subset or equal to] W x W which is an orthogonality: namely, it is irreflexive and symmetric. For x [element of] W, Y [subset or equal to] W we write

(2.1.9) x [perpendicular to] Y iff x [perpendicular to] y [inverted] Ay [element of] Y

and define

(2.1.10) [Y.sup.[perpendicular to]] [equivalent] {x:x [perpendicular to] Y}

In Goldblatt's terminology [Goldblatt 1973], Y [subset or equal to] W is said to be regular if

(2.1.11) [Y.sup.[perpendicular to][perpendicular to]] = Y.

The class R(F) of regular subsets of W is a complete ortholattice under the partial order given by set inclusion, with the lattice meet given by set intersection and [perpendicular to] as orthocomplement. This class of examples is canonical in light of Goldblatt's fundamental theorem a la Stone for ortholattices:

THEOREM 2.1.2 [GOLDBLATT 1973; BELL 1983]. Any ortholattice L is (completely) isomorphic to a sublattice of R([F.sub.L]) for some orthogonality space [F.sub.L].

Since this theorem is the cornerstone of all the models we shall discuss, it is worth describing the construction. For a given ortholattice L, [F.sub.L] = <[W.sub.L], [perpendicular to]> where [W.sub.L] is the class of proper filters of L, and for x, y [element of] [W.sub.L],

x [perpendicular to] y iff [exists]a [element of] L such that a' [element of] x and a [element of] y.

(A proper filter of L is an upward closed subset of L, closed also under finite meets, which does not contain [0.sub.L.])

The map

(2.1.12) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where 2 denotes the two-element set (usually expressed as 2 = {0, 1}), given for a [element of] L, by

(2.1.13) [Phi] (a) = {x [element of] [W.sub.L]: a [element of] x}

embeds L into R([F.sub.L]).

(Goldblatt also characterizes the image of L under [Phi]: it coincides with the family of those regular subsets of [W.sub.L] that are clopen in the topology on [W.sub.L] that has as a subbase the sets [Phi](a), a [element of] L, and their complements.)

In case L is complete, [Phi] is onto.

Clearly, we may restrict to the class of complete ortholattices in the algebraic characterization theorem (Theorem 2.1.1).

Now a proper filter is like a "world" that "validates" each of its members: if the membership of a in x is construed as "a is true in world x" then everything that can be inferred from a should also "be true in world x", which is the case if x is a filter, and ?? is read as a form of implication. Under this reading each [Phi](a) (eq. (2.1.12)), being a set of worlds, could be interpreted as a proposition of a certain type, and indeed Goldblatt's Stonean theorem (Theorem 2.1.2), taken together with the characterization theorem (Theorem 2.1.1), yields a class of Kripkean models that also characterize orthologic.

The discussion of these will be facilitated by the introduction of some formal results that it will prove convenient to collect together in the next section.

2.2. SOME MODAL IDENTITIES. A proximity space <W, [approximately equals]> is a set W together with a binary relation [approximately equals] [subset of equal to] W x W, which is reflexive and symmetric. Clearly each proximity space <W, [approximately equals]> determines an orthogonality space <W, [perpendicular to]>, where x [perpendicular to] y iff x ?? y, and, conversely, each orthogonality space <W, [perpendicular to]> determines a proximity space <W, [approximately equals]> where x [approximately equals] y iff not x [perpendicular to] y.

Given a proximity space <W, [approximately equals]> we define for each E [subset or equal to] W:

(2.2.1) [diamond] E [equivalent] {w [element of] W: [exists]v [element of] E such that w [approximately equals] v},

and note that E [subset of equal to] [diamond]E. It will prove convenient to employ the notation

(2.2.2) [S.sub.v] [equivalent] [diamond]{v} = {w [elememt of] W: w [approximately equals] v}

(the "sphere" around v, in the terminology of D. Lewis). Then one may also write

(2.2.3) [diamond] E = [[union].sub.v[element of] E] [S.sub.v].

Dually, we write

(2.2.4) [] E [equivalent] [([diamond] [E.sup.c]).sup.c],

where the superscript c denotes set complementation relative to W.

PROPOSITION 2.2.1. For <W, [approxiamtely equals]>, a proximity space and E, F [subset of equal to] W:

(M1) [diamond](E [union] F) = [diamond] E [union] [diamond] F

(M2) For a family F of subsets of W: [diamond]([[intersection].sub.F [element of] F] F) [subset or equal to] [[intersection].sub.F [element of] F] ([diamond] F)

(M3) [diamond] E = [([E.sup.[perpendicular to]]).sup.c] [equivalent] [E.sup.[perpendicular to] c]

(M4) [] E = [E.sup.c [perpendicular to]] = {w [element of] W: [S.sub.w] [subset of equal to] E}

(M5) E [subset or equal to] [E.sup.[perpendicular to] [perpendicular to]]

(M6) E [subset or equal to] F implies [F.sup.[perpendicular to]] [subset or equal to] [E.sup.[perpendicular to]]

(M7) [E.sup.[perpendicular to] [perpendicular to] [perpendicular to]] = [E.sup.[perpendicular to]]

(M8) [] [diamond] [] E = [] E

(M9) [diamond] [] [diamond] E = [diamond] E

(M10) [(E [union] F).sup.[perpendicular to]] = [E.sup.[perpendicular to]] [intersection] [F.sup.[perpendicular to]]

(M11) [E.sup.[perpendicular to]] [union] [F.sup.[perpendicular to]] [subset or equal to] [(E [intersection] F).sup.[perpendicular to]].

PROOF. The proofs of these elementary identities may be safely left to the interested reader. For instance, to prove (M3) we note that w [is not an element of] [diamond] E implies w ?? x for all x [element of] E so that w [perpendicular to] E showing that [([diamond] E).sup.c] [subset or equal to] [E.sup.[perpendicular to]] from which it follows that [([E.sup.[perpendicular to]]).sup.c] [subset or equal to] [diamond] E. The converse inclusion is obvious.

The proof of (M4) now follows, since

(2.2.5) []E [equivalent] [([[diamond]E.sup.c]).sup.c]

= [([([E.sup.c]).sup.[perpendicular to] c]).sup.c]

= [E.sup.c[perpendicular to]]

= {w: w [perpendicular to] [E.sup.c]}

= {w: v [is not an element of] E implies v ?? w}

= {w: v [approximately equals] w implies v [element of] E}

= {w: [S.sub.w] [subset of equal to] E}.

From (M6) applied to (MS), we obtain [([E.sup.[perpendicular to] [perpendicular to]).sup.[perpendicular to]] [subset or equal to] [E.sup.[perpendicular to]]. But from (M5) we also have [E.sup.[perpendicular to]] [subset of equal to] [([E.sup.[perpendicular to]]).sup.[perpendicular to] [perpendicular to]], and (M7) follows.

(M8), (M9), and (M10) follow immediately from (M3), etc., and (M11) follows from (M3) and (M2). []

2.3. KRIPKE MODELS FOR ORTHOLOGIC. These models seem to have appeared first in Goldblatt [1974] and have been extensively elaborated upon by Dalla Chiara and others (cf. Dalla Chiara [1986]).

Given a proximity space P = {W, <approximately equals]>, we follow Dalla Chiara [1986] in defining a proposition of P (or just a proposition, if the context is clear) to be a subset X [subset or equal to] W satisfying:

if x has the property that for each y with y [approximately equals] x,

there exists a z [element of] X such that y [approximately equals] z, then x [element of] X,

or, equivalently, X is a proposition of P iff

(2.3.1) [S.sub.x] [subset or equal to] [diamond] X implies x [element of] X.

(The reverse implication is clear, since [diamond] X = [[union].sub.x [element of] X] [S.sub.x].)

Then we have the following:

LEMMA 2.3.1

(1) X is a proposition iifx = [] [diamond] X = [X.sup.[perpendicular to] [perpendicular to]].

(2) X is a proposition iff x [is not an element of] X implies [exists]y [approximately equals] x with y [perpendicular to] X.

(3) For any Y [subset of equal to] W, [Y.sup.[perpendicular to]] is a proposition.

(4) If C is a family of propositions, then [intersection] C is a proposition.

(5) If Y is a proposition, then X [subset or equal to] Y iff [diamond] X [subset or equal to] [diamond] Y.

PROOF

(1) From (M4), the condition labelled (2.3.1) implies [] [diamond] X [subset or equal to] X, the reverse inclusion having been noted above. The second equation follows from (M3) and (M4).

(2) This follows immediately from (2.3.1) which is equivalent to: x [is not an element of] X implies [S.sub.x] ?? [diamond] X = [X.sup.[perpendicular to] c].

(3) Immediate from (M7).

(4) x [is not an element of] [[intersection].sub.C [element of] C] C implies [exists] [C.sub.0] [element of] [C.sub.0] such that x [is not an element of] [C.sub.0]. Thus [S.sub.x] ?? [diamond] [C.sub.0], since [C.sub.0] is a proposition (cf. the proof of (2) above). So [S.sub.x] ?? [[intersection].sub.C [element of] C] ([diamond] C) from which it follows that [S.sub.x] ?? [diamond]([[intersection].sub.C [element of] C]) in view of (M2).

(5) Implication in one direction is immediate; the other follows from (M3), (M5), and (M6). []

Thus, the family of propositions of a proximity space is exactly the family R(<W, [perpendicular to]>) of regular sets of the associated orthogonality space and the existence of the complete ortholattice structure possessed by this family of subsets (already alluded to) may be read off from Lemma 2.3.1. (Note that W and ?? are also propositions.)

A Kripke orthomodel M = (W, [approximately equals], ??) is a proximity space P = <W, [approximately equals]> and a function (called a valuation) ?? : [Phi] [right arrow] R (< W, [perpendicular to]>) satisfying:

(2.3.2) ?? (~[Alpha]) = ?? [([Alpha]).sup.[perpendicular to]]

(2.3.3) ?? ([Alpha] ?? [Beta] = ?? ([Alpha]) [intersection] ?? ([Beta]).

We will say that a formula [Alpha] is:

true at the "world" w [element of] w, and write w | [[equivalent].sub.m] [Alpha], iff W [element of] ?? ([Alpha]);

true on a set E [subset or equal to] W, and write E | [[equivalent].sub.m] [Alpha] iff w | [[equivalent].sub.m] [Alpha] for all w [element of] E, that is iff E [subset or equal to] ?? ([Alpha]);

true in the Kripke orthomodel M if it is true at every world in M;

Kripke valid, and write | [equivalent] [Alpha] iff it is true in all Kripke orthomodels.

In the sequel, we shall abbreviate R (<W, [perpendicular to]>) to R(W), since the proximity and orthogonality relations will never be ambiguous.

THEOREM 2.3.1

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

PROOF. Suppose [[assertion sign].sub.o] [Alpha], and let M = <W, [approximately equals], ??> denote an arbitrary Kripke orthomodel. Then <R(W), ??> constitutes an algebraic orthomodel and Corollary 2.1.1 (cf. statement (2.1.8)) implies that ?? ([Alpha]) = W so that [Alpha] is true in the Kripke orthomodel M. But M was arbitrary, so [Alpha] is Kripke valid.

Conversely, suppose | [equivalent] [Alpha], and let A [equivalent] <L, [v.sub.L]> denote an arbitrary algebraic orthomodel. Then M [equivalent] <[W.sub.L], [[approximately equals].sub.L], [[Phi].sub.L] [degrees] [v.sub.L]> (where [W.sub.L], [[Phi].sub.L] and [[perpendicular to].sub.L] are the entities appearing in the discussion of Goldblatt's Stonean theorem (Theorem 2.1.2)) constitutes a Kripke orthomodel. Since [Alpha] is assumed Kripke valid it is true in M, so that [[Phi].sub.L] ([v.sub.L]([Alpha])) = [W.sub.L]. But then [v.sub.L] ([Alpha]) = [[Phi].sub.L] since [[Phi].sub.L] is injective. Thus, [Alpha] is true in the arbitrarily chosen algebraic orthomodel A, so [[assertion sign].sub.o] [Alpha] by (2.1.8). []

Having established that the Kripke valid formulas are exactly the theorems of orthologic, we will now examine the semantic content of Kripke validity in a little more detail.

PROPOSITION 2.3.1. For a Kripke orthomodel M = <W, [approximately equals] ??>, formulas [Alpha], [Beta], [Gamma] and E [subset of equal to] W:

(1) E | [[equivalent].sub.M] [Alpha] iff [diamond]E [subset or equal to] [diamond] ?? ([Alpha]) iff v [approximately equals]. w for some w [element of] E implies [exists]x [approximately equals] v such that x | [[equivalent].sub.M] [Alpha].

(2) E | [[equivalent].sub.M] ~ [Alpha] iff [diamond]E [subset or equal to] ?? [([Alpha]).sup.c] iff [diamond] ?? ([Alpha]) [subset or equal to] [diamond] [([diamond]E).sup.c] iff v [approximately equals] w for some w [element of] E implies not v | [[equivalent].sub.M] [Alpha].

(3) E | [[equivalent].sub.M] [Beta] ?? [Gamma] iff E | [[equivalent].sub.M] [Beta] and E | [[equivalent.sub.M] [Gamma].

PROOF

(1) This is immediate from Lemma 2.3.1 (5).

(2) E | [[equivalent].sub.M] ~ [Alpha] iff [diamond] E [subset or equal to] [diamond] ?? (~[Alpha]) = [diamond] ?? [([Alpha]).sup.[perpendicular to]] = ?? [([Alpha]).sup.[perpendicular to] [perpendicular to]c] = ?? [([Alpha]).sup.c] from (M3) and because ?? ([Alpha]) is a proposition. This last containment is equivalent to the containment ?? ([Alpha]) [subset or equal to] [([diamond]E).sup.c] which in turn is equivalent to [diamond] ?? ([Alpha]) [subset or equal to] [diamond][([diamond]E).sup.c] by Lemma 2.3.1 (5) since [([diamond]E).sup.c] = [E.sup.[perpendicular to]] is a proposition (Lemma 2.3.1 (3)).

(3) Clear. []

A question that now interposes itself (and that will occupy us for the remainder of this paper) concerns the semantics of disjunction. In a Kripke orthomodel we have, for formulas [Alpha] and [Beta], and E [subset or equal to] W as above:

(2.3.4) E | [[equivalent].sub.M] [Alpha] ?? [Beta] iff E | [[equivalent].sub.M] ~ (~[Alpha] ?? ~[Beta])

iff [diamond]E [subset or equal to] ?? [(~[Alpha] ?? ~[Beta]).sup.c] from Proposition 2.3.1 (2)

= [(?? [([Alpha]).sup.[perpendicular to]] [intersection] ?? [([Beta]).sup.[perpendicular to]]).sup.c]

= ?? [([Alpha]).sup.[perpendicular to]c] [union] ?? [([Beta]).sup.[perpendicular to]c]

= [diamond] ?? ([Alpha]) [union] [diamond] ?? ([Beta]),

and the problem immediately arises of expressing this condition in some form consistent with the semantics that has already been given in terms of the validity of propositions.

For instance, although [diamond] ?? ([Alpha]) [union] [diamond] ?? ([Beta]) = [diamond](?? ([Alpha]) [union] ?? ([Beta])), one could not conclude from [diamond]E [subset or equal to] [diamond](?? ([Alpha]) [union] ?? ([Beta])) (and Lemma 2.3.1 (5)) that E [subset or equal to] ?? ([Alpha]) [union] ?? ([Beta]) since ?? ([Alpha]) [union] ?? ([Beta]) need not be a proposition.

In the remainder of this paper, we will discuss two further models in which this semantic problem is circumvented in the sense that a coherent semantics may be extended to "orthodisjunction".

Before embarking upon the discussion of these models, let us note that the interpretation of [Alpha] ?? [Beta] in a Kripke orthomodel may be expressed by

(2.3.5) ?? ([Alpha] ?? [Beta]) = ?? (~(~[Alpha] ?? ~[Beta]))

= [(?? [([Alpha]).sup.[perpendicular to] [intersection] ?? [([Beta]).sup.[perpendicular to]]).sup.[perpendicular to]]

= (?? ([Alpha]) [union] ?? [([Beta])).sup.[perpendicular to] [perpendicular to]] by (M10)

[contains or equal to] ?? ([Alpha]) [union] ?? ([Beta]).

Thus, the interpretations of orthodisjuncts are, in a sense, double negations of ordinary disjuncts of propositions--these are not necessarily themselves ordinary disjuncts: there are generally more worlds in ?? ([Alpha] ?? [Beta]) than there are in ?? ([Alpha]) [union] ?? ([Beta]). That is, one could have w | [[equivalent].sub.M] [Alpha] ?? [Beta] while neither w | [[equivalent].sub.M] [Alpha] nor w | [[equivalent].sub.M] [Beta] holds. This circumstance embodies much of what seems anomalous to classical minds when confronted with "quantum" phenomena.

2.4. J. L. BELL'S LOGIC OF ATTRIBUTES. (From now on all ortholattices will be assumed complete.) Bell [1983; 1986] introduced a new and simple semantics for orthologic that produces a consistent semantics for orthodisjunction. The inspiration for it seems to have been the "Beth-Kripke-Joyal" semantics of classical and intuitionistic logic, in which formulas are forced over elements of a lattice (Boolean in the classical case, Heyting in the intuitionistic case). In Bell [1986], a very interesting physical interpretation is developed. Unfortunately, as the author points out in Bell [1986], there is an error in the proof of the characterization theorem (Theorem 2.4) given in Bell [1983] and the question of completeness of Bell's original system seems to remain open.

We shall employ the Kripke orthomodels of the last section first to motivate and then to prove a characterization theorem (vis-a-vis orthologic) for a similar but weaker version of the propositional fragment of Bell's logic.

Note first that, given a proximity space <W, [approximately equals]>, the family of subsets of the form [diamond] E, E [subset or equal to] W, constitutes a complete ortholattice, the join being ordinary set union, the orthocomplement ([diamond] E)* of an element [diamond] E being given by

(2.4.1) ([diamond] E)* = [diamond][([diamond]E).sup.c]

and the meet of two elements [diamond] E and [diamond] F being the largest set of the form [diamond]() contained within [diamond] E [intersection] [diamond] F. J. L. Bell calls this the lattice of "parts" (of (W, [approximately equals] [is greater than]) and we shall follow him in denoting it by Part W (cf. Bell [1986]) since the proximity relation will never be ambiguous.

PROPOSITION 2.4.1. Given a proximity space <W, [approximately equals]>:

(2.4.2) [diamond]: R(W) [right arrow] Part W

is an isomorphism of complete ortholattices. Its inverse is

(2.4.3) []: Part W [right arrow] R(W).

PROOF. For any E [subset or equal to] W

(2.4.4) [diamond]([E.sup.[perpendicular to]]) = [E.sup.[perpendicular to] [perpendicular to] c]

= [E.sup.[perpendicular to] cc [perpendicular to] c]

= [([diamond]E).sup.c [perpendicular to] c]

= [diamond] [([diamond]E).sup.c]

= ([diamond]E)* from Eq. (2.4.1).

For any family [E.sub.i] of elements of R(W):

(2.4.5) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Thus, [diamond] restricted to R(W) is a homomorphism of complete ortholattices.

Now note that if A is some element of Part W then [] A = [A.sup.c [perpendicular to]] by (M4) which is in R(W) by Lemma 2.3.1(3). Moreover, for E [element of] R(W), [] [diamond] E = [E.sup.[perpendicular to] [perpendicular to]] = E so on R(W)

(2.4.6) [][diamond] = [1.sub.R(W)]

and for A = [diamond]F [element of] Part W,

(2.4.7) [diamond][]A = [diamond][][diamond]F = [diamond]F by (M9) = A

so on Part W

[diamond][] = [1.sub.Part W]. []

Returning to the semantics derived for Kripke orthomodels (Proposition 2.3.1) we note that, in view of the last proposition, they are equivalent to assertions concerning valuations lying in the corresponding lattice of parts. Thus, if we were to introduce a "forcing" relation ([satisfies]) between elements of the lattice of parts, Part W, for a given Kripke orthomodel M = <W, [approximately equals], ??>, and formulas [Alpha] by means of the definition

(2.4.9) [diamond]E [satisfies] [Alpha] iff [diamond]E [subset or equal to] [diamond] ?? ([Alpha])

then, by Proposition 2.3.1,

E | [[equivalent].sub.M] [Alpha] would translate into [diamond]E [satisfies] ~[Alpha] (via Proposition 2.3.1(1)).

Then E | [[equivalent].sub.M] ~ [Alpha] would translate into [diamond]E ?? ~[Alpha] which, by Proposition 2.3.1(2) (and Eq. (2.4.1)) is equivalent to

[diamond] ?? ([Alpha]) [subset or equal to] [diamond][([diamond] E).sup.c] = ([diamond]E)*,

which in turn is equivalent to

[diamond]F [subset or equal to] [diamond] ?? ([Alpha]) implies [diamond]F [subset or equal to] ([diamond]E)*,

which, in terms of the forcing relation and the lattice structure of Part W, amounts to:

(2.4.10) [diamond]E [satisfies] ~[Alpha] iff [diamond]F ?? [Alpha] implies [diamond]F ?? ([diamond]E)*.

It is immediate from the definition (assertion (2.4.9)) and (M2) that

(2.4.11) [diamond]E [satisfies] [Beta] ?? [Gamma] iff [diamond]E [satisfies] [Beta] and [diamond]E [satisfies] [Gamma].

Thus, by means of the forcing relation, the Kripke semantics may be transported over to the ortholattice of parts, and, since all complete ortholattices are isomorphic to lattices of parts, we may divest ourselves of Kripkean trappings and write the forcing rules in terms of an arbitrary complete algebraic model.

Restarting, then, with a given (complete) algebraic orthomodel A [equivalent] <L, [v.sub.L]> we recursively define a forcing relation p [[satisfies].sub.A] [Alpha], for p [element of] L and [Alpha] a formula, as follows:

(F1) For atomic [Alpha]:

p [[satisfies].sub.A] [Alpha] iff p ?? [v.sub.L]([Alpha])

(F2) For a formula [Alpha]:

p [[satisfies].sub.A] ~ [Alpha] iff q [[satisfies].sub.A] [Alpha] implies q ?? p'

(F3) For formulas [Beta] and [Gamma]:

p [[satisfies].sub.A] [Beta] ?? [Gamma] iff p [[satifies].sub.A] [Beta] and p [[satisfies].sub.A] [Gamma]

The promised derived semantics for orthodisjunction is given as follows.

THEOREM 2.4.1

p [[satisfies].sub.A] [Alpha] ?? [Beta] iff [exists] q, r [element of] L with p ?? q ?? r such that q [[satisfies].sub.A] [Alpha] and r [[satisfies].sub.A] [Beta].

First we prove

LEMMA 2.4.1 (CF. BELL [1983, LEMMATA 2.0 AND 2.1])

(1) For any formula [Alpha], [0.sub.L] [[satisfies].sub.A] [Alpha].

(2) For a family [p.sub.i] [element of] L, if [p.sub.i] [[satisfies].sub.A] [Alpha] for all i then [??.sub.i] [p.sub.i] [[satisfies].sub.A] [Alpha].

PROOF

(1) An easy induction on the complexity of [Alpha].

(2) By induction on the complexity of [Alpha]. The statement is clearly true for atomic [Alpha].

Negations: Suppose [p.sub.i] [[satisfies].sub.A] ~[Alpha] for all i. Then q [[satisfies].sub.A] [Alpha] implies that, for all i, q ?? [p'.sub.i], which implies that q ?? [??.sub.i] [p'.sub.i] = ([??.sub.i] [p.sub.i])' so that [??.sub.i] [p.sub.i] [[satisfies].sub.A] ~[Alpha]. Conjunctions: Suppose [p.sub.i] [[satisfies].sub.A] [Beta] ?? [Gamma]. Then, for all i, [p.sub.i] [[satisfies].sub.A] [Beta] and [p.sub.i] [[satisfies].sub.A] [Gamma] so by the induction hypothesis, ?? [p.sub.i] [[satisfies].sub.A] [Beta] and ?? [p.sub.i] [[satisfies].sub.A] [Gamma], so ?? [p.sub.i] [[satisfies].sub.A] [Beta] ?? [Gamma]. []

PROOF OF THEOREM 2.4.1 (AFTER BELL [1983, LEMMA 2.2]). Suppose p [[satisfies].sub.A] [Alpha] ?? [Beta]: that is,

p [[satisfies].sub.A] ~(~[Alpha] ?? ~ [Beta]).

This is the case:

(2.4.12) iff q [[satisfies].sub.A] ~[Alpha] ?? ~ [Beta] implies q ?? p' iff q ?? p' implies not q [[satisfies].sub.A] ~ [Alpha] or not q [[satisfies].sub.A] ~ [Beta] iff q ?? p' implies [exists]r ?? q' such that r [[satisfies].sub.A] [Alpha] or r [[satisfies].sub.A] [Beta].

Let

(2.4.13) [p.sub.[Alpha] [equivalent] ?? {r: r [[satisfies].sub.A] [Alpha]}, [p.sub.[Beta]] [equivalent] ?? {r: r [[satisfies].sub.A] [Beta]} and s [equivalent] [p.sub.[Alpha]] ?? [p.sub.[Beta]].

Then [p.sub.[Alpha]] [[satisfies].sub.A], [Alpha] and [p.sub.[Beta]] [[satisfies].sub.A] [Beta] by Lemma 2.4.1(2), so:

(2.4.14) [exists][p.sub.[Alpha]], [p.sub.[Beta]] [element of] L with s [equivalent] [p.sub.[Alpha]] ?? [p.sub.[Beta]] such that [p.sub.[Alpha]] [??.sub.A] [Alpha] and [p.sub.[Beta]] [??.sub.A] [Beta].

Now suppose p ?? s. Then s' ?? p' so by assertion (2.4.12)

[exists]r ?? s" = s such that r [[satisfies].sub.A] [Alpha] or r [[satisfies].sub.A] [Beta]

contradicting the defining Eq. (2.4.13). Thus, p ?? s and assertion (2.4.14) gives

[exists][p.sub.[Alpha]], [p.sub.[Beta]] L with p ?? [p.sub.[Alpha]] ?? [p.sub.[Beta]] such that [p.sub.[Alpha]] [[satisfies].sub.A] [Alpha] and [p.sub.[Beta]] [[satisfies].sub.A] [Beta]

and this proves the left-to-right implication of the theorem.

To prove the converse, suppose [exists][p.sub.1], [p.sub.2] [element of] L with p ?? [p.sub.1] ?? [p.sub.2] such that [p.sub.1] [[satisfies].sub.A] [Alpha] and [p.sub.2] [[satisfies].sub.A] [Beta]. Let [p.sub.[Alpha]] [equivalent] ?? {r: r [[satisfies].sub.A] [Alpha]}: then

(2.4.15) p ?? [p.sub.1] ?? [p.sub.2] ?? [p.sub.[Alpha]] ?? [p.sub.2].

Given q ?? p' suppose that for all r, r [[satisfies].sub.A] [Alpha] implies r ?? q'. Then, by Lemma 2.4.1(2), [p.sub.[Alpha]] ?? q' and, since p ?? q', we must have [p.sub.2] ?? q', from Eq. (2.4.15). Hence, [exists]r ?? q' such that r [[satisfies].sub.A] [Beta], namely [p.sub.2]. It now follows from assertion (2.4.12) that p [[satisfies].sub.A] [Alpha] ?? [Beta]. []

Let us say that a formula [Alpha] is in force in the algebraic orthomodel A if [1.sub.L] [[satisfies].sub.A] [Alpha] and in force if it is in force in every algebraic orthomodel. In this case, we write

[satisfies] [Alpha].

We shall prove that the formulas that are in force are precisely the theorems of orthologic. Note first that given a Kripke orthomodel M = <W, [approximately equals], ??> we may associate with it the complete algebraic orthomodel

(2.4.16) [A.sup.M] [equivalent] <Part W, [diamond] [degrees] ??>.

Moreover, given a complete algebraic orthomodel L = <L, [v.sub.L]>, say, we may associate with it another complete algebraic orthomodel, namely

(2.4.17) [A.sub.L] [equivalent] <Part [W.sub.L], [diamond] [degrees] [[Phi].sub.L] [degrees] [v.sub.L]>,

where [W.sub.L] and [[Phi].sub.L]: L [right arrow] R([W.sub.L]) are the entities appearing in Goldblatt's Stonean theorem (Theorem 2.1.2). (Recall that [[Phi].sub.L] is an isomorphism since L is assumed complete.) We note that

(2.4.18) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

LEMMA 2.4.2

(1) With M and [A.sup.M] as above, [Alpha] a formula and E [subset or equal to] W:

(2.4.19) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(2) With L and [A.sub.L] as above, p [element of] L and [Alpha] a formula:

(2.4.20) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

PROOF. Both proofs are by induction on the complexity of [Alpha].

(1) If [Alpha] is an atom and E [subset or equal to] W,

E | [[equivalent].sub.M] [Alpha] iff [diamond]E [subset or equal to] [diamond] ?? ([Alpha]) by Proposition 2.3.1(1) iff [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [Alpha] by definition (F1) which establishes the base case.

Negations:

E | [[equivalent].sub.M] ~ [Alpha] iff [diamond] ?? ([Alpha]) [subset or equal to] [diamond] [([diamond]E).sup.c] by Proposition 2.3.1(2)

iff [diamond]F [subset or equal to] [diamond] ?? ([Alpha]) implies [diamond]F [subset or equal to] [diamond][([diamond]E).sup.c] = ([diamond]E)*

iff F | [[equivalent].sub.M] [Alpha] implies [diamond]F [subset or equal to] ([diamond]E)*, by Proposition 2.3.1(1)

iff [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [Alpha] implies [diamond]F [subset or equal to] ([diamond]E)*, by the induction hypothesis

iff [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [Alpha] from definition (F2).

Conjunctions are similar.

(2) For atomic [Alpha]:

p [[satisfies].sub.L] [Alpha] iff p ?? [v.sub.L]([Alpha]), definition (F1)

iff [[Phi].sub.L](p) [subset or equal to] [[Phi].sub.L]([v.sub.L]([Alpha])), [[Phi].sub.L] being a lattice isomorphism

iff [diamond]([[Phi].sub.L](p)) [subset or equal to] [diamond]([[Phi].sub.L]([v.sub.L]([Alpha]))) by Lemma 2.3.1(5)

iff [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] by definition (F1)

Negations:

P [[satisfies].sub.L] ~ [Alpha] iff q [[satisfies].sub.L] [Alpha] implies q ?? p'

iff [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] implies [diamond]([[Phi].sub.L](q)) [subset or equal to] ([diamond]([[Phi].sub.L](p)))*, by the induction hypothesis and the fact that [diamond] [degrees] [[Phi].sub.L] is an ortholattice isomorphism.

iff [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], since every element of Part [W.sub.L] is of the form [diamond]([[Phi].sub.L](q)) for some q.

The conjunctive case is trivial. []

COROLLARY 2.4.1. For an algebraic orthomodel L = <L, [v.sub.L]> and a formula [Alpha]

p [[satisfies].sub.L] [Alpha] iff p ?? [v.sub.L]([Alpha]).

PROOF. With M [equivalent] <[W.sub.L], [approximately equals], [[Phi].sub.L] [degrees] [v.sub.L]>:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The following result follows immediately from this corollary and Corollary 2.1.1.

THEOREM 2.4.2

[satisfies] [Alpha] iff [[assertion sign].sub.o] [Alpha].

Corollary 2.4.1 asserts that for a given algebraic orthomodel L the forcing relation p [[satisfies].sub.L] [Alpha] is equivalent to the "covering" relation p ?? [v.sub.L]([Alpha]) for any formula [Alpha]. A trivial consequence is that the property of persistence--namely that p [[satisfies].sub.L] [Alpha] and q ?? p imply q [[satisfies].sub.L] [Alpha]--holds for the forcing relation [satisfies].

J. L. Bell's original forcing scheme consists (in part) of (F1), (F2), and (F3) together with a separately appended Joyal-like rule for ??, namely:

(2.4.21) P [[satisfies].sub.L] [Alpha] ?? [Beta] iff [exists]q, r [element of] L with p = q ?? r such that q [[satisfies].sub.L] [Alpha] and r [[satisfies].sub.L] [Beta].

The insistence upon equality in this condition has the effect of obstructing persistence and causing the forcing relation to differ in general from the covering relation. (Although the De Morgan identity (Eq. (2.1.1)) holds for the ?? defined by the condition (2.4.21) when p = [1.sub.L] (Bell [1983, Lemma 2.2], examples show that it does not hold for general p.) This could interfere with the induction invoked in the proof of the characterization Theorem 2.4 of Bell [1983] and is presumably the source of the error alluded to in Bell [1986]. The question of whether or not Bell's forcing conditions produce precisely the theorems of orthologic seems to remain open: this question is interesting in light of Bell [1986] which discusses these nonpersistence phenomena and argues persuasively in favor of the resulting logic being considered as a viable candidate for "quantum" logic, regardless of its status vis-a-vis orthologic.

2.5. THE MODAL TRANSLATION THEOREM. It will not have been lost upon modally inclined readers that our so-called proximity spaces are exactly the Kripke frames for the normal modal system known as the "Brouwersche" or B-system (cf. for example Hughes and Cresswell [1968; 1984] and Chellas [1980]). To describe this system, we introduce the ordinary Boolean connectives ?? (negation), [conjunction] (conjunction) and the modal operator [] (necessity). Material implication [right arrow], and the possibility operator [diamond] are introduced via the usual definitions (for example, [diamond] [equivalent] ?? [] ??). The axioms and inference rules include the usual ones for PC with modus ponens, and the modal additions (for formulas [Alpha], [Beta]):

[]([Alpha] [right arrow] [Beta]) [right arrow] ([][Alpha] [right arrow] [][Beta]) [][Alpha] [right arrow] [Alpha] [Alpha] [right arrow] [][diamond][Alpha] (the "Brouwersche" axiom) If [Alpha], then [] [Alpha] (Necessitation)

We denote the set of modal formulas by [[Phi].sub.M]. The theoremhood of a formula is defined as usual and we write

(2.5.1) [[assertion sign].sub.B] [Alpha]

if [Alpha] is a theorem of the modal B-system.

A (Kripke) B-model is a triple B = <W, [approximately equals], v> where W is a set (of "worlds"), [approximately equals] a proximity relation on W and v: [[Phi].sub.M] x W [right arrow] 2 is a function satisfying:

(V1) For each w [element of] W, v(??, w): [[Phi].sub.M] [right arrow] 2 is a Boolean valuation with respect to ??, and [conjunction]: that is, v(?? [Alpha], w) = ?? v([Alpha], w), and v([Alpha] [conjunction] [Beta], w) = v([Alpha], w) [conjunction] v([Beta], w);

(V2) For any modal formula [Alpha], v([][Alpha], w) = 1 iff v([Alpha], v) = 1 for every v [approximately equals] w.

It follows that:

(V3) v([Alpha] [disjunction] [Beta], w) = v([Alpha], w) [disjunction] v([Beta], w), where [disjunction] denotes the classical disjunct, and

(V4) For any modal formula [Alpha], v([diamond][Alpha], w) = 1 iff [exists]v [approximately equals] w such that v([Alpha], v) = 1.

A modal formula [Alpha] is said to be:

true at the worm w in the B-model B, written w [??.sub.B] [Alpha], iff v([Alpha], w) = 1; true on the set E [subset or equal to] W, written E [??.sub.B] [Alpha], iff w [??.sub.B] [Alpha] for all w [element of] E; true in the B-model B iff W [??.sub.B] [Alpha]; B-valid, written ?? [Alpha], if it is true in all B-models.

These models characterize the B-system:

THEOREM 2.5.1

[[assertion sign].sub.B] [Alpha] iff ?? [Alpha].

(This is proved in the references cited above.)

It seems to have been noticed almost simultaneously and independently by Goldblatt [1974] and Dishkant [1977] that the theorems of orthologic admit a translation into theorems of the B-system. These ideas were extensively elaborated by Dalla Chiara and others (cf. references in Dalla Chiara [1986]; see also Burghardt [1984]). Since this is the representation of orthologic that we will find most useful in the computational context, we will present yet another proof of the translation theorem.

The translation recursively assigns to each orthoformula [Alpha] [element of] [Phi] a modal formula [Alpha] [degrees] [element of] [[Phi].sub.M] as follows:

(T1) For atomic formulas [a.sub.i]:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(T2) [([Alpha] ?? [Beta]).sup.o] = [Alpha] [degrees] [conjunction] [Beta] [degrees]

(T3) [(~[Alpha]).sup.o] = [] ?? [Alpha] [degrees]

(Note that the "quantization" of [a.sub.i], namely [][diamond][a.sub.i], is really a kind of double negation of [a.sub.i] since [][diamond] [equivalent] [] ?? [] ?? which amounts to a double [perpendicular to] on sets of worlds: cf. the remark following Eq. (2.3.5)).

We will prove that [Alpha] is an orthotheorem iff [Alpha] [degrees] is a theorem of the B-system.

Suppose a Kripke orthomodel M = <W, [approximately equals], ??> is given. Then a B-model

(2.5.2) [B.sub.M] = <W, [approximately equals], [v.sub.??]>

may be constructed by defining, for w [element of] W and atomic formulas [a.sub.i]:

(2.5.3) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

which may then be inductively extended to [[Phi].sub.M] according to the rules (V1)-(V4) given above.

Let us write, for each modal formula [Alpha] and B-model B = <W, [approximately equals], v>,

(2.5.4) ||[Alpha][||.sub.B] = {w [element of] W: w [??.sub.B] [Alpha]}.

Then it is clear that:

(2.5.5) ||[Alpha] [conjunction] [Beta][||.sub.B] = ||[Alpha][||.sub.B] [intersection] ||B[||.sub.B],

(2.5.6) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(2.5.7) ||[][Alpha][||.sub.B] = []||[Alpha][||.sub.B]

and

(2.5.8) ||[diamond][Alpha][||.sub.B] = [diamond]||[Alpha][||.sub.B],

where the right-hand sides are as in Eqs. (2.2.1)-(2.2.4). (We will often drop the subscript when the context is clear.)

Returning to the B-model [B.sub.M], we note that

(2.5.9) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

LEMMA 2.5.1. For atomic [a.sub.i] [element of] [Phi]

(1) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(2) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

PROOF

(1) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(2) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Now we note that

(2.5.10) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

In particular,

(2.5.11) [v.sub.??]([(~[a.sub.i]).sup.o], w) = 1 iff [v.sub.??]([] ?? [a.sub.i], w) = 1

so the last lemma can be restated as:

COROLLARY 2.5.1

(1) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(2) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

PROPOSITION 2.5.1. For any [Alpha] [element of] [Phi]

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The proof is an easy induction on the complexity of [Alpha], the base case being covered by the last corollary.

PROPOSITION 2.5.2. For [Alpha] [element of] [Phi]

[assertion sign] [Alpha] [degrees] implies [assertion sign] [degrees] [Alpha].

PROOF. Choose a Kripke orthomodel M = <W, [approximately equals], ??>. Then if [[assertion sign].sub.B] [Alpha] [degrees], [Alpha] [degrees] is true in the B-model associated with M, namely [B.sub.M] = <W, [approximately equals], [v.sub.??]> (Eq. (2.5.2)): that is, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for all w [element of] W. Then, by the last proposition, ?? ([Alpha]) = W, so [Alpha] is true in the arbitrarily chosen Kripke orthomodel M, hence in every such orthomodel, so [assertion sign] [degrees] [Alpha] (Theorem 2.3.1). []

Now, given a B-model B = <W, [approximately equals], v> we may construct a Kripke orthomodel [M.sup.B] [equivalent] = <W, [approximately equals], [??.sub.v]>, where [??.sub.v] is given on atoms by

(2.5.12) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(which is a proposition by Lemma 2.3.1(3)), and defined inductively on [Phi].

The following lemma is again an easy induction on complexity.

LEMMA 2.5.2. For any [Alpha] [element of] [Phi]

[??.sub.v]([Alpha]) = ||[Alpha] [degrees][||.sub.B].

PROPOSITION 2.5.3. For [Alpha] [element of] [Phi]

[assertion sign] [degrees] [Alpha] implies [[assertion sign].sub.B] [Alpha] [degrees].

PROOF. Choose any B-model B = <W, [approximately equals], v>. Then if [assertion sign] [degrees] [Alpha], [Alpha] is true in the associated Kripke orthomodel [M.sup.B] (Theorem 2.3.1): that is, [??.sub.v]([Alpha]) = W. So, by the last lemma, ||[Alpha] [degrees][||.sub.B] = W showing that [Alpha] [degrees] is true in the arbitrary B-model B and hence B-valid. So [[assertion sign].sub.B] [Alpha] [degrees]. []

Thus, from the last two propositions, we obtain the modal translation theorem, namely:

THEOREM 2.5.2. For [Alpha] [element of] [Phi]

[assertion sign] [degrees] [Alpha] iff [[assertion sign].sub.B] [Alpha] [degrees].

2.6. QUANTUM LOGIC AND NEOREALISM. The "orthomodels" that arise in the physics of quantum systems are of the following type. Let H denote a (complex) Hilbert space with inner product <|>. Then, with h denoting the set H - {0} of nonzero vectors in H, and with [Xi] [perpendicular to] [Eta] iff <[Xi]|[Eta]> = 0 for [Xi], [Eta] [element of] h, <h, [perpendicular to]> is an orthogonality space.

Recall that if E is a subset of H then the smallest closed subspace of H containing E, which we shall denote by [E], is just [E.sup.[perpendicular to] [perpendicular to]] [union] {0}. Thus, if E is a subset of h, we have

(2.6.1) [E.sup.[perpendicular to] [perpendicular to]] = {[Eta] [element of] H: [Eta] [perpendicular to] [E.sup.[perpendicular to]] - {0}

= [E] - {0}

so if E is a proposition (of h)

(2.6.2)

E = [E] - {0}.

Thus, a proposition is a closed subspace of H with the zero element removed. Conversely, if F is a closed subspace of H, it is quickly seen that F - {0} is a proposition of h. Thus, the propositions of h correspond with the closed subspaces of H via the assignment E ?? [E], a correspondence immediately seen to be bijective, with inverse F ?? F - {0}. This bijection is also easily seen to preserve the respective ortholattice structures. (Note that in this correspondence ?? ?? [??] = {0}.) That is, the ortholattice R(h) is isomorphic with the ortholattice of closed subspaces of H, which we shall denote by L (H).

Ortholattices of the form L (H) have an additional important property that is of peculiar significance in quantum theory: namely, they are orthomodular. To motivate the introduction of this property we shall attempt first to identify some of its logical consequences.

To each "quantum system" is associated a Hilbert space H: the rays, or one-dimensional subspaces of H, are in one-to-one correspondence with the so-called "pure states" of the system, and the ortholattice of closed subspaces may in general be interpreted as the lattice of "propositions" (whose subject is the underlying quantum system) in keeping with the earlier Kripkean terminology in the context of the proximity space <h, [approximately equals]>. (See, e.g., Varadarajan [1985].)

By contrast the "pure states" of a classical system are just the points of its phase space. (For example, the set of "pure states"-- or just "states"--of a particle moving in space may be taken to be represented by its set of possible spacetime coordinate vectors paired with the possible momentum or velocity vectors associated with that spacetime coordinate vector.) The "propositions" about the classical system are then classified by the Boolean algebra of subsets of the phase space (taking, in the case of a particle, the form of propositions concerning the ranges of values of coordinates and momenta).

Thus, in Kripkean terms, the models corresponding to classical "systems" are those orthomodels of the form <W, =, ??> in which, for any E [subset or equal to] W, [E.sup.[perpendicular to]] = [E.sup.c] so that the ortholattice of classical propositions is exactly the Boolean algebra [2.sup.W], and all modalities collapse. The logic supported by all such orthomodels is of course just ordinary classical PC.

Now in the quantum physics context Boolean subalgebras of ortholattices of the form L (H) play a crucial role: they are intimately associated with the notion of an observable, and, more generally, are generated by sets of "compatible" elements: p is compatible with q in an ortholattice if p = (p ?? q) ?? (p ?? q'). (In the case of L(H), this is equivalent to the commutativity of the respective projection operators onto the subspaces p and q, and is associated in the physical interpretation with the notion of "simultaneous observability". Note that a pair of orthogonal subspaces satisfies this condition.) The existence of such sets of compatible elements is required by any interpretation that seeks to effect a mediation between theory and experiment. Their existence in a general ortholattice L is guaranteed in the presence of the so-called orthomodularity condition:

(2.6.3) p ?? q implies p ?? (p' ?? q) = q,

which turns out to be equivalent to the following condition (Kalmbach [1983, Theorem 2, p. 22]):

if p ?? q, then the smallest subortholattice of L

containing p and q is distributive, hence Boolean.

Ortholattices satisfying this condition are called orthomodular. For such ortholattices, p is compatible with q iff q is compatible with p, and it can be shown that families of mutually compatible elements in such lattices generate Boolean subalgebras (Kalmbach [1983]; Varadarajan [1985]). The term "quantum logic" is almost universally reserved for that logic whose theorems are supported by the orthomodels we have been considering with the orthomodularity condition superimposed upon them. That this logic defies simple axiomatization in terms of Kripke orthomodels was stunningly demonstrated by Goldblatt's discovery that orthomodularity is not elementary [Goldblatt 1984a]. (It seems that this logic might still be too general to deserve its enshrinement as "quantum" logic, since there exist orthomodular lattices with logical properties distinctly different from those of the form L(H) [Greechie 1981]. A logical characterization of the logic supported only by orthomodels associated with ortholattices of the form L(H) still seems to be lacking.)

Quantum logic is distinguished from classical logic not only at the lattice or "propositional" level--that is, at the level at which Boolean algebras are replaced by orthomodular ones (with a concomitantly anomalous implicational structure that we do not discuss here: see, for example, Dalla Chiara [1979; 1986], Hughes [1979])--but also in a broader phenomenological sense. That is to say, while classical logic is flat in the sense that any Boolean algebra may be expressed as a (continuous) product of its Boolean subalgebra 2 (or as the algebra of global sections of a sheaf of 2s over the Stone space of the algebra: cf. Graves and Selesnick [1973], Kalmbach [1983], and Selesnick [1998]), quantum logic is twisted with respect to its Boolean substructure: it is exactly this twisting that confutes efforts to give realist interpretations to quantum theory, as has been recently pointed out by Isham and Butterfield [1998; 1999]). We conclude this section with a brief and much simplified description of their important insight.

As we have noted, Boolean subalgebras of the lattice L (H) play a crucial role in the interpretation of the quantum theory of the system associated to the Hilbert space H. Each such subalgebra in a sense represents a "classical window" through which "states" of the system may be viewed. (Every family of mutually compatible elements generates such a classical window, as we have noted, and, moreover, each observable gives rise to one via its spectral resolution.) Such "windows" are partially ordered by inclusion, a relation that may be interpreted as a coarsening of the "grain", or resolving power, of the "view" afforded by the ambient algebra to that afforded by the included algebra. The "states" that can be viewed "through" a given Boolean subalgebra A of L(H) may be identified with the elements of that algebra's Stone space Spec A, which may in turn be identified with the set of Boolean morphisms, or valuations, of A into 2. Thus each "state" viewable through A corresponds to a classical truth-value assignment to the elements of A. If such a "state" is to have any kind of objective reality vis-a-vis classical observers, then it should be viewable through each classical window and furthermore such a view of it should be independent of any more finely grained view of it.

Such a state will then correspond to a choice, for each Boolean subalgebra A [subset or equal to] L(H), of an element [[Chi].sub.A] [element of] Spec A, such that if A [subset or equal to] B, where B is another Boolean subalgebra of L(H), then

(2.6.4) [[Chi].sub.A] = [[Chi].sub.B]|A,

the vertical line denoting restriction.

As Isham and Butterfield point out, it is a consequence of the Kochen--Specker theorem that no such assignment exists, if the dimension of H is greater than two. They observe, furthermore, that an assignment of the above type, namely A ?? [[Chi].sub.A], is precisely a global section of a certain presheaf, defined as follows. First, regard the set W of Boolean subalgebras of L(H), partially ordered by inclusion, as a category in the usual way. Then the assignment

Spec: W [right arrow] Set,

given for each A in W by Spec(A) = Spec A, with morphisms in W being sent to restrictions in Set, the category of sets, constitutes a contravariant functor, or presheaf, on W. Now the category [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] of such presheaves is a simple example of the structure known as a topos [Asperti and Longo 1991; Barr and Wells 1990; Bell 1988; Goldblatt 1984b] and contains, among other objects, a terminal object, denoted 1: this is the presheaf which assigns to each object in W the singleton set.

For a presheaf S in this topos, a morphism 1 [right arrow] S is called a global section of S. It is clear that the global sections of Spec are exactly the assignments of the form A ?? [[Chi].sub.A] whose existence is thwarted by the Kochen--Specker theorem.

Isham and Butterfield exploit this insight to reevaluate realism. Although global sections of Spec do not exist, local sections certainly do, and in abundance: these are sections over subobjects of the terminal object, and correspond to consistent choices of morphisms [[Chi].sub.A] for some objects A of W. Now in every topos there is an object [Omega], the subobject classifier, with the property that subobjects of any object are classified by morphisms from that object into [Omega]. (In the topos Set it is the set 2.) Local sections of Spec give rise to subobjects of Spec and hence to ("global") presheaf morphisms

(2.6.5) Spec [right arrow] [Omega].

To interpret this in more mundane terms, let A now denote some arbitrary Boolean algebra. If we think of subsets of Spec A as corresponding to, or being, Kripkean "A-propositions", then A is embedded by the Stone theorem as a subalgebra of the algebra of all possible A-propositions, namely [2.sup.SpecA]. Functions of the form

(2.6.6) Spec A [right arrow] 2

correspond one-to-one with A-propositions. In particular, the singletons {[Chi]}, [Chi] [element of] Spec A, correspond to certain A-propositions, namely the atoms in the lattice of A-propositions. If we were now to allow A to vary over the category W, then we would not be able to select even an atomic proposition {[[Chi].sub.A]} for each object A of W in a manner consistent with coarse graining if dim H [is greater than] 2, by the Kochen--Specker theorem (a la Isham and Butterfield). One interpretation of this negative result might be that our notion of A-proposition, with truth-values in 2, is inappropriate to the context in which A varies over the category W. Indeed, since we are working in a topos there is a more appropriate interpretation of the notion of a (varying per object) proposition, namely as a morphism of the type displayed in Eq. (2.6.5). Thus, for each object A of W, propositions of the form Eq. (2.6.6) are replaced by those of the form

(2.6.7) Spec A [right arrow] [Omega](A)

so that the static set of classical truth-values 2 in (2.6.6) is replaced by the context dependent set [Omega](A).

It is a general result that the subobject classifier in a topos is an (internal) Heyting algebra (so that each [Omega](A) is a Heyting algebra) and that the logic modelled by propositions of the form (2.6.5) is intuitionistic.

Thus, Kochen--Specker prohibitions notwithstanding, certain aspects of realism--namely the existence of global valuations--may be reinstated in quantum theory, at the expense of requiring these valuations to lie in contextually dependent Heyting algebras. In Isham and Butterfield [1998; 1999], a finely detailed theory of Heyting algebra valued valuations is developed and interpreted (very roughly along the lines of (2.6.5)) for various presheaf topoi associated with Hilbert spaces. These ideas are likely to have a profound impact on the subject of quantum logic and its interpretation, and we shall return to them elsewhere.

3. Computational Elements

In this concluding section, we attempt to exploit some of the model theory developed above to delineate an essential difference between a "classical" computation (which may be thought of as being implemented within an appropriate model for classical PC) and a "quantum" computation (which we think of as being implemented within an appropriate model for orthologic). Of course, "appropriate models" for quantum logic should be found among the Hilbert space based models discussed in Section 2.6, and these should correspond in turn to actual physical quantum systems, if computing devices exploiting "quantum effects" are ever to be implemented. This is currently an area of extremely intense and accelerating interest, and we can refer the reader to only a tiny sample of references, namely: Deutsch [1985; 1989], Ekert and Jozsa [1996], and Berman et al. [1998].

In keeping with our modest aim of delineating certain logical distinctions between classical and quantum computational paradigms through the use of models for the corresponding logics, we must--and largely shall--sidestep the profoundly difficult problems of overt physical interpretation: indeed, the possibility of doing exactly this was our motivation for using the model-theoretic formalism in the first place.

Specifically, we seek first to model the simplest nontrivial classical computational device, or element, namely the so-called N-gate. The behavior of such a gate may be described through the use of a classical Boolean model, which we may regard as a degenerate Kripkean orthomodel of the form <S, =, v>, where S is the set of classical states of the gate, and the modalities collapse (cf. Section 2.6). Then we find a minimal Hilbert space based, or Hilbertian, orthomodel corresponding to the chosen classical model, and discover the phenomenon of "quantum parallelism", now expressed in modal terms.

3.1. THE CLASSICAL N-GATE. The classical N-gate is a device which can accept one input bit, and outputs that bit's Boolean complement or negation. Let us identify each possible input (two in this case: 0 or 1) with a possible "holding" state, or state of occupancy, or just state, of the gate. Then the "computation" effected by such a gate transforms each state into some other state: in the case of the N-gate this transformation, [Tau]: S [right arrow] S, merely interchanges its two possible states.

To render this into model-theoretic terms, we introduce an alphabet consisting of a single atom a, a set of states S = {[s.sub.0], [s.sub.1]} and a Boolean valuation for each state [S.sub.i] via

(3.1.1) [v.sub.s](a, [s.sub.i]) = i for i = 0, 1.

The interpretation of a in this valuation is as an observable, or register variable: its truth-value in the valuation registers the presence of the corresponding state. Now N [equivalent] (S, =, [v.sub.s]) is a B-model with collapsed modalities and so supports the theorems of classical PC. In particular (omitting the turnstile subscript)

[s.sub.0] ?? a [disjunction] ?? a whose semantics is [s.sub.0] ?? a or [s.sub.0] ?? ?? a.

Only one of these can be true, and for our choice of valuation it is

(3.1.2) [s.sub.0] ?? ?? a.

After the "computational" step, or action of the N-gate, [S.sub.0] is transformed to [S.sub.1] and

(3.1.3) [s.sub.1] ?? a [disjunction] ?? a leading to [s.sub.1] ?? a.

Thus in state [s.sub.0] the N-gate "registers" ?? a (assertion (3.1.2)). After one computational step the N-gate arrives at state [s.sub.1], which registers a (assertion (3.1.3)). (Similar interpretations apply if we had started with [s.sub.1].)

At each state s exactly one of s ?? a or s ?? ?? a obtains: the model is committed to the truth either of a or of ?? a at a state s. The single computational step, such as it is, then proceeds in the presence of such a commitment, after which a new commitment to the truth of one or other of the formulas a, ?? a is asserted at the new state. Thus, the effect of the computation or operation of the N-gate, if started in state So, follows the sequence of assertions

[s.sub.0] ?? ?? a; [s.sub.1] ?? a.

The absence of any kind of parallelism is apparent in this completely trivial example: the truth of a single formula, namely ?? a, at the state [s.sub.0], is a commitment that is independent of the computational step (namely, the transition [s.sub.0] ?? [s.sub.1]). However, as often happens, this trivial classical example yields upon quantization a decidedly non-trivial quantum system which exhibits the phenomenon known as "quantum parallelism". The modal translation theorem (Theorem 2.5.2) may be used to capture this (nonclassical) feature of quantum computation. It is the possibility of implementing the massive parallelism inherent in this feature that drives much of the current interest in so-called quantum computers.

3.2. QUANTIZATION AND THE EMERGENCE OF QUANTUM PARALLELISM. We shall attempt to "quantize" the classical N-gate by specifying first the class of Kripke orthomodels that most closely resemble the classical model described above, and then seeking a Hilbertian member of this class.

The model of the classical N-gate discussed in the last section consisted of a pair N [equivalent] (N, [Tau]) comprising a "classical" or collapsed B-model N [equivalent] <S, = [v.sub.s]>, a bijection [Tau] S [right arrow] S, and, implicitly, a distinguished atomic formula a, interpreted as a "register variable". Our quantization scheme is a slight formalization of the idea that N may be quantized by replacing the trivial relation "=" by a more general proximity relation "[approximately equals]" to obtain a nonclassical B-model, and using the modal translation to "quantize" the theorem satisfied by the register variables, while preserving certain aspects of the original classical model. Namely, we seek the minimal quantum version of some classical pair C = <C, [Tau]> whose ortholattice of propositions contains C's classical propositional structure as a Boolean subalgebra generated by compatible atomic propositions corresponding to the atomic propositions of C. In this way, the original C is recovered as one "classical window" (among many) upon its quantization.

A computation, or quantum computation, in the context of a general proximity space <W, [approximately equals]) will be taken to be a bijection [Sigma]: W [right arrow] W having the property that

(3.2.1) [w.sub.1] [approximately equals] [w.sub.1] iff [Sigma]([w.sub.1]) [approximately equals] [Sigma]([w.sub.2]).

(Note that for any E [subset or equal to] W, [Sigma][(E).sup.[perpendicular to]], from which it follows that [Sigma] induces an ortholattice automorphism on the lattice of propositions of W.)

Given a classical model C = <S, =, [v.sub.s]), a bijection [Tau]: S [right arrow] S and a countable family [[Phi].sub.0] of "register variables", or atoms, let us call the pair <C, [Tau]> a classical computational element.

We define a quantization of the classical computational element <C, [Tau]) to be a pair <M, [Sigma]> comprising a B-model M [equivalent] (W, [approximately equals], [v.sub.W]) and a quantum computation [Sigma] on <W, [approximately equals]>, together with a map q: S [right arrow] W satisfying the following:

(Q1) For all s [element of] S and a [element of] [[Phi].sub.0]: s ?? a iff q(s) ?? a [degrees] That is, the intentions of register variables vis-a-vis states are quantized consistently: the state-register variable relation ?? is preserved upon quantizing both elements of the relation.

(Q2) For [s.sub.1], [s.sub.2] [element of] S, if [s.sub.i] [is not equal to] [S.sub.2] then q([S.sub.1]) [perpendicular to] ([s.sub.2]) (so that q is injective). That is, distinct classical states should give rise to mutually inaccessible quantum states. Note that, in case the B-model M is Hilbertian, the rays containing the elements q(s) are mutually orthogonal, hence mutually compatible, hence generate a Boolean subalgebra of the orthomodular lattice of propositions (which is isomorphic to the Boolean algebra of classical propositions of S, namely [2.sup.s]).

(Q3) q[(S).sup.[perpendicular to]] = ?? or equivalently q[(S).sup.??] = W. No quantum state in the quantization should be inaccessible to all of those quantum states that are quantizations of classical states.

(Q4) The following diagram commutes:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The classical computation should be recoverable when viewed through the "classical window" (see (Q2)) corresponding to C.

It is clear that the proximity spaces <W, [approximately equals]> of Hilbertian quantizations of a given classical system <C, [Tau]> are mutually isomorphic, since, by (Q2) and (Q3), the corresponding Hilbert spaces all have the same dimension, namely the cardinality of S. We note also that if the Hilbert space underlying the Hilbertian proximity space of such a quantization is separable and infinite dimensional, then it follows from a celebrated theorem of Wigner that [Sigma] must be the restriction of a unitary or an antiunitary transformation in the original Hilbert space [Varadarajan 1984, p. 108].

Before moving on to a search for the Hilbertian quantization of the classical N-gate computational element let us consider how the general notion of a "computation" as envisaged in the case of the classical N-gate model may play out in the case of a general quantum computational element <B, [Sigma]>: that is, a pair comprising a B-model B [equivalent] <W, [approximately equals], [v.sub.w]) and a quantum computation [Sigma] (a bijection on W satisfying condition (3.2.1)). Let us assume that the possible propositional "register variables" assemble into an orthotheorem of the form [Alpha] ?? [Beta] (analogous to the classical theorem a [disjunction] ?? a used earlier). Then ([Alpha] ?? [Beta]) [degrees] is true at every state in W by the modal translation theorem.

That is, since

(3.2.2)

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

we have at each w [element of] W,

(3.2.3) w [??.sub.B] [] [diamond] ([Alpha] [degrees] [disjunction] [Beta] [degrees])

which is equivalent to:

(3.2.4) [inverted] Ax [approximately equals] w [exists]y [approximately equals] such that y [??.sub.B] [Alpha] [degrees] or y [??.sub.B] [Beta] [degrees]

or:

from each state accessible to w there is at least one

accessible state at which [Alpha] [degrees] or [Beta] [degrees] is true,

which, [approximately equals] being reflexive, implies:

[exists]y [approximately equals] such that y [??.sub.B] [Alpha] [degrees] or y [??.sub.B] [Beta] [degrees].

Thus, at each w commitment to the truth of [Alpha] [degrees] or [Beta] [degrees] does not have to be made: it is, in a sense, indirect or delayed. Indeed, a quantum computational step mapping w to [Sigma](w) proceeds in the absence of such a commitment. At the end of such a computation, we have

(3.2.5) [Sigma](w) [??.sub.B] [] [diamond] ([Alpha] [degrees] [disjunction] [Beta] [degrees]),

so that a tree-like pattern of possible accessibilities and their "registrations" or outcomes (namely, the truth or otherwise at accessible states of [Alpha] [degrees] or [Beta] [degrees]) similar to the pattern at w, obtains at [Sigma](w). These possible outcomes at appropriate daughter and grand-daughter states of [Sigma](w) are dependent upon both variables [Alpha] [degrees] and [Beta] [degrees]. In particular, there may be some states accessible from [Sigma](w) at which [Alpha] [degrees] is true and others at which [Beta] [degrees] is true: a single quantum computation, namely w ?? [Sigma](w), has apparently implemented a simultaneous processing of both variables [Alpha] [degrees] and [Beta] [degrees]. This is "quantum parallelism" in the context of this model; the absence of this phenomenon from our earlier model of the classical N-gate may be noted.

If the quantum computational step [Sigma]: W [right arrow] W is thought of as being induced by the evolution of the system through some time interval, then the two cases may be contrasted as follows (cf. Bub [1997]). The evolution in time of the state of a classical system leaves unchanged the "possibility structure" associated with the observables of the system (i.e., the probabilities entailed by the Boolean structure of the logic of possibilities). In contradistinction, the evolution in time of the "actual state" of a quantum system entails the evolution also of the possibility structure associated with observables of the system, relative to that state. In the modal setting we have employed, the tree of possible accessibilities and the associated registrations (or outcomes) emanating from the state w (assertion (3.2.4)) itself evolves into a generically different tree at [Sigma](w). Since the tree at w carries the information about both "observables" [Alpha] [degrees] and [Beta] [degrees] relative to w, it is exactly the fact of the evolution in time of this tree that gives rise to the phenomenon of quantum parallelism. In the classical case, the modalities are collapsed and there is no accessibility tree at any state, and therefore no parallelism.

To bring this discussion a little further down to earth, we shall conclude by returning to the Hilbertian quantization of the classical N-gate.

3.3. THE QUANTUM N-GATE. Our model of the classical N-gate is the classical computational element N [equivalent] <N, [Tau]> where N = <{[s.sub.0], [s.sub.1]}), =, [v.sub.s]> where [v.sub.s] is given by Eq. (3.1.1) and [Tau] is the transposition of the states [s.sub.0] and [s.sub.1]. Then a Hilbertian proximity space of the quantization is given, according to (Q2) and (Q3), by choosing q([s.sub.0]) and q([s.sub.1]) to be orthogonal vectors in some two-dimensional Hilbert space, which might as well be [C.sup.2], the vector space of ordered pairs of complex numbers with the standard inner product. We fix some arbitrary choice of two orthogonal vectors in [C.sup.2], which it will be convenient to choose to be normalized, and label them |0> and |1>. Then we put

(3.3.1) q([s.sub.0]) = |0>,

(3.3.2) q([s.sub.1]) = |1>.

Then, with the proximity space for the quantization chosen to be H [equivalent] [C.sup.2] - {0}, (Q3) is satisfied since

(3.3.3) q[(S).sup.[perpendicular to]] = [{|0>, |1>}.sup.[perpendicular to]] = [diameter],

(where S = {[s.sub.0], [s.sub.1]}).

We define a valuation for |[Xi]> [element of] H by

(3.3.4) [v.sub.H](a, |[Xi]>) = {1 if |[Xi]> [element of] [{|1>}.sup.[perpendicular to][perpendicular to]] 0 if |[Xi]> [is not an element of] [{|1>}.sup.[perpendicular to][perpendicular to]]

so that

(3.3.5) [||a||.sub.H] = [{|1>}.sup.[perpendicular to][perpendicular to]]

where H is the B-model H = <H, [approximately equals], [v.sub.H]>. Then

(3.3.6) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where r([Xi]) stands for the ray through |[Xi]> in [C.sup.2] with {0} removed, and it is clear that

(3.3.7) [v.sub.s](a, [s.sub.i]) = [v.sub.H]([a [degrees], |i>) for i = 0, 1

or

(3.3.8) [s.sub.i] [??.sub.N] a iff q([s.sub.i]) a [degrees] for i=0, 1

so that (Q1) is satisfied with these choices.

Finally, we note that since the [[Sigma].sub.H]: H [right arrow] H we seek is supposed to induce an automorphism of the ortholattice L([C.sup.2]) it must be at least additive when extended to [C.sup.2], by a standard theorem of projective geometry [Baer 1952]. Its commutation with multiplication by scalars is fixed only up to an algebraic automorphism of the scalar field C. However, there is a unique linear [[Sigma].sub.H] which renders commutative the diagram in (Q4) and that is the one whose (unitary) matrix representation relative to the basis {|0>, |1>} of [C.sup.2] is

(3.3.9) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

So a quantization [N.sup.Q] of N is obtained by setting

(3.3.10) [N.sup.Q] [equivalent] <H, [[Sigma].sub.H]>.

Since the theorem a [disjunction] ?? a satisfied by the register variable in the classical case is the classical version of the orthotheorem a ?? ~a, the corresponding theorem to be used in the modal translation is:

(3.3.11) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Thus, at each quantum state |[Xi]> [element of] H

(3.3.12) |[Xi]> [??.sub.H] [][diamond](a [disjunction] [] ?? a)

which implies that at each |[Xi]> [element of] H

[inverted] A|[Zeta]> [approximately equals] |[Xi]> [exists]|[Zeta]> such that |[Eta]> [??.sub.H] a [disjunction] [] ?? a

or:

(3.3.13) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Thus, the accessibility tree emanating from any quantum state has leaves lying in both r(0) and r(1). If an actual quantum device were to operate along the lines of our model, then, in order for it to take advantage of the inherent parallelism during the course of the computation (or sequence of computations), it would be necessary for it to pass through at least one state that is not actually in either ray r(0) or r(1): such states are called superpositions (of r(0) and r(1)). By passing through such states, the device could circumvent most of the nodes in the exponentially exploding tree of binary choices of states and outcomes to which it would be condemned in the classical probabilistic case, since at each superpositional state it avoids a commitment to the truth or falsity of either branch, while still having access to them.

Remarkably, physical systems exist that seem to be manipulable in such a way as to implement these notions. We briefly indicate a class of physical systems which could implement our quantum computational element [N.sup.Q]. These systems require the trapping in some way of a charged spin-1/2 particle like an electron, proton or ion whose two spin states could be used to represent a computational basis {|0[is greater than], |1[is greater than]}. By placing such a particle in an electromagnetic field resonating at a certain frequency (the Rabi frequency, denoted [Omega]) transitions between the spin states may be induced, thus implementing our quantum computation [[Sigma].sub.H]. (See, e.g., Berman et al. [1998].)

The unitary operator inducing the transitions may be expressed relative to the computational basis as

(3.3.14) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where t denotes the time during which the electromagnetic pulse has been applied, so that

(3.3.15) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

If we redefine our quantum computational step [[Sigma].sub.H] to be u([Pi]/2[Omega]), say, then our new quantum computation will be represented by

(3.3.16) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

If the system were to start in spin state |0[is greater than], after one of these computational steps it would arrive at the superpositional state

(3.3.17) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

A second step would then produce

(3.3.18) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

After the first computational step a (superpositional) state was arrived at that was accessible to (or from) both |0[is greater than] and |1[is greater than]. Another run of the same computation then produced a state no longer accessible to (or from) |0[is greater than]. This illustrates the phenomenon of quantum interference: the "wrong" target state |0[is greater than] has been removed by a process akin to the interference of waves. (We note that physically there is no distinction between the states |1[is greater than] and i|1>[is greater than].)

These notions may be exploited to solve actual problems: we refer the reader to literature already cited.

It is possible to generalize our example of the classical N-gate to more general reversible classical gates, and then to quantize along the lines of our treatment here. Increasing the number of input/output bits to two or more generates the kind of quantum states known as entangled states whose peculiarities may also be exploitable by quantum computing devices. This topic will be treated elsewhere.

REFERENCES

ASPERTI, A., AND LONGO, G. 1991. Categories, Types, and Structures. An Introduction to Category Theory for the Working Computer Scientist. The MIT Press, Cambridge and London, England.

BAER, R. 1952. Linear Algebra and Projective Geometry. Academic Press, New York.

BARR, M., AND WELLS, C. 1990. Category Theory for Computing Science. Prentice-Hall, New York.

BELL, J. L. 1983. Orthologic, forcing and the manifestation of attributes. In Proceedings of the Southeast Asian Conference on Logic. Studies in Logic, vol. III. North-Holland, Amsterdam, The Netherlands, pp. 13-36.

BELL, J. L. 1986. A new approach to quantum logic. Brit. J. Phil. Sci. 37, 83-99.

BELL, J. L. 1988. Toposes and Local Set Theories. Oxford Logic Guides: 14, Clarendon Press, Oxford, England.

BERMAN, G., DOOLEN, G. D., MAINIERI, R., AND TSIFRINOVICH, V. I. 1998. Introduction to Quantum Computers. World Scientific Publishing, Singapore.

BUB, J. 1997. Interpreting the Quantum World. Cambridge University Press, Cambridge, England.

BURGHARDT, F. J. 1984. Modalities and quantum mechanics. Int. J. Theoret. Phys. 23, 1171-1195.

CHELLAS, B. F. 1980. Modal Logic: An Introduction. Cambridge University Press, Cambridge, England.

DALLA CHIARA, M. L. 1979. Some metalogical pathologies of quantum logic. In Current Issues in Quantum Logic, Workshop on Quantum Logic, (Erice), E. G. Beltrametti and B. C. van Fraassen, Eds. Plenum Press, New York, pp. 147-159.

DALLA CHIARA, M. L. 1986. Quantum logic. In Handbook of Philosophical Logic, Vol. III. D. Gabbay and F. Guenther, Eds. D. Reidel Publishing Company.

DEUTSCH, D. 1985. Quantum theory, the Church-Turing principle and the universal quantum computer. Proc. Royal Soc. London A400, 97-117.

DEUTSCH, D. 1989. Quantum computational networks. Proc. Royal Soc. London A425, 73-90.

DISHKANT, H. 1977. Imbedding of the quantum logic in the modal system of Brower (sic). J. Symb. Logic 42, 3, 321-328.

EKERT, A., AND JOZSA, R. 1996. Quantum computation and Schor's factoring algorithm. Rev. Mod. Phys. 68, 3, 733-753.

GOLDBLATT, R. I. 1973. The stone space of an ortholattice. Bull. London Math. Soc. 7, 45-48.

GOLDBLATT, R. I. 1974. Semantic analysis of orthologic. J. Phil. Logic 3, 19-35.

GOLDBLATT, R. I. 1984a. Orthomodularity is not elementary. J. Symb. Logic 49, 401-404.

GOLDBLATT, R. I. 1984b. Topoi: The Categorial Analysis of Logic. North-Holland, Amsterdam, The Netherlands.

GRAVES, W. H., AND SELESNICK, S. A. 1973. A generalization of the Stone theorem for orthomodular lattices. Colloq. Math. 27, 1, 21-30.

GREECHIE, R. 1981. A non-standard quantum logic with a strong set of states. In Current Issues in Quantum Logic. Vol. 8 of Ettore Majorana International Science Series, E. G. Beltrametti and B. C. van Fraassen, Eds. Plenum Press, New York, pp. 375-380.

HUGHES, G. E., AND CRESSWELL, M. J. 1968. An Introduction to Modal Logic: Methuen and Co., Ltd., London, England.

HUGHES, G. E., AND CRESSWELL, M. J. 1984. A Companion to Modal Logic. Methuen, London, England.

HUGHES, R. I. G. 1979. Realism and quantum logic. Current Issues in Quantum Logic, Workshop on Quantum Logic, (Erice), E. G. Beltrametti and B. C. van Fraassen, Eds. Plenum Press, New York, pp. 77-87.

ISHAM, C. J., AND BUTTERFIELD, J. 1998. Topos perspective on the Kochen--Specker Theorem: I. Quantum states as generalised valuations. Int. J. Theoret. Phys. 37, 2669-2733.

ISHAM, C. J., AND BUTTERFIELD, J. 1999. Topos perspective on the Kochen--Specker Theorem: II Conceptual aspects and classical analogues. Int. J. Theoret. Phys. 38, 827-859.

KALMBACH, G. 1983. Orthomodular Lattices. Cambridge University Press, Cambridge, Mass.

SELESNICK, S. A. 1998. Quanta, Logic and Spacetime: Variations on Finkelstein's Quantum Relativity. World Scientific Publishing, Singapore.

VARADARAJAN, V. S. 1985. Geometry of Quantum Theory (2nd ed.). Springer-Verlag, New York.

RECEIVED SEPTEMBER 1999; REVISED DECEMBER 1999; ACCEPTED JANUARY 2000

J. P. RAWLING AND S. A. SELESNICK

University of Missouri-St. Louis, St. Louis, Missouri

The authors gratefully acknowledge the support of a University of Missouri-St. Louis Research Award and a University of Missouri Research Board Award.

Authors' addresses: J. P. Rawling, Department of Philosophy, University of Missouri-St. Louis, 8001 Natural Bridge Road, St. Louis, MO 63121-4999; S. A. Selesnick, Department of Mathematics and Computer Science, University of Missouri-St. Louis, 8001 Natural Bridge Road, St. Louis, MO 63121-4999.

Permission to make digital/hard copy of part or all of this work for personal or classroom use is granted without fee provided that the copies are not made or distributed for profit or commercial advantage, the copyright notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery (ACM), Inc. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee.

(C) 2000 ACM 0004-5411/00/0700-0721 $05.00

Printer friendly Cite/link Email Feedback | |

Author: | RAWLING, J. P.; SELESNICK, S. A. |
---|---|

Publication: | Journal of the Association for Computing Machinery |

Geographic Code: | 1USA |

Date: | Jul 1, 2000 |

Words: | 14064 |

Previous Article: | Complexity of Finite-Horizon Markov Decision Process Problems. |

Next Article: | Balanced Sequences and Optimal Routing. |

Topics: |