Weakly complete axiomatization of exogenous quantum propositional logic

P. Mateus and A. Sernadas CLC, Department of Mathematics, IST {pmat,acs}@math.ist.utl.pt

November 27, 2006

Abstract
A weakly complete finitary axiomatization for EQPL (exogenous quantum propositional logic) is presented. The proof is carried out using a non trivial extension of the Fagin-Halpern-Megiddo technique together with three Henkin style completions.

1 Introduction

A new logic (EQPL – exogenous quantum propositional logic) was proposed in [17, 18] for modeling and reasoning about quantum systems, embodying all that is stated in the postulates of quantum physics (as presented, for instance, in [9, 21] ). The logic was designed from the semantics upwards, starting with the key idea of adopting superpositions of classical models as the models of the proposed quantum logic.
This novel approach to quantum reasoning is quite different from the traditional approach [12, 8] to the problem that, as initially proposed by Birkhoff and von Neumann [5] , focuses on the lattice of closed subspaces of a Hilbert space. Our exogenous semantics approach has the advantage of closely guiding the design of the language around the underlying concepts of quantum physics while keeping the classical connectives and was inspired by the possible worlds approach originally proposed by Kripke [15] for modal logic.
It is also akin to the society semantics introduced in [7] for many-valued logic and to the possible translations semantics proposed in [6] for paraconsistent logic. The possible worlds approach was also used in [22, 23, 3, 2, 11, 1] for probabilistic logic. Our semantics of quantum logic, although inspired by modal logic, is also completely different from the alternative Kripke semantics given to traditional quantum logics (as first proposed in [10] ) still closely related to the lattice-oriented operations. For other examples of logics based on the exogenous semantics approach see [19] .
Contrarily to traditional quantum logics that replace the classical connectives by new connectives inspired by the lattice-oriented operations, by adopting superpositions of classical models as the models of the quantum logic, we are led to a natural extension of the classical language containing the classical connectives (like modal languages are extensions of the classical language).
Furthermore, the new logic allows quantitative reasoning about amplitudes and probabilities, being in this respect much closer to the possible worlds logics for probability reasoning than to the traditional quantum logics. For other developments in this direction, also motivated by applications in quantum computation and information, see [25, 24] .
Herein, we present a finitary Hilbert calculus for EQPL and show that it is weakly complete relatively to an oracle for arithmetical reasoning.
Strong completeness is out of question since entailment is not compact. The proof of the weak completeness result was carried out using a non trivial extension of the technique proposed by Fagin, Halpern and Megiddo for simple probabilistic logics, together with three Henkin completions.
Although EQPL only provides the means for propositional, quantitative reasoning about quantum states, it is a mandatory step before further developments towards calculi for reasoning about the evolution of quantum systems (as already outlined in [18] ). The weak completeness result established here is interesting from the theoretical point of view and shows that the proposed language fits the proposed exogenous semantics. But, for practical applications in quantum system specification and verification, it seems better to go for model checking techniques.
Such future developments of our approach to quantum reasoning are briefly discussed in Section 6 of the paper. In Section 2, we briefly motivate the EQPL semantic concepts and key design ideas, directly based on the postulates of quantum physics. In Section 3, we present the EQPL language and semantics plus some examples. In Section 4, we introduce the axioms and rules of EQPL. Section 5 is fully dedicated to the proof of the main result (weak completeness of EQPL).

2 Key design ideas

Starting from the postulates of quantum mechanics (closely following [9] ) we present the key ideas that guided the design of EQPL (together with a brief review of the relevant concepts and results of operator theory).
Postulate 1: Every isolated quantum system is described by a Hilbert space. The states of the quantum system are the unit vectors of the corresponding Hilbert space.
Recall that a Hilbert space is a complete inner product space over C   (the field of complex numbers). For example, the states of an isolated qubit are vectors of the form z 0 | 0 〉 + z 1 | 1 〉   where z 0 , z 1 ∈ C   and | z 0 | 2 + | z 1 | 2 = 1   . In other words, they are unit vectors in the (unique up to isomorphism) Hilbert space of dimension two. Concerning EQPL, it is natural to represent each qubit by a propositional symbol (more appropriately called a qubit symbol).
Furthermore, each qubit state (better called qubit valuation) should be a superposition of the two possible classical valuations.
Postulate 2: The Hilbert space of a quantum system composed of a finite number of independent components is the tensor product of the component Hilbert spaces.
For example, z 00 | 00 〉 + z 01 | 01 〉 + z 10 | 10 〉 + z 11 | 11 〉   , where z 00 , z 10 , z 01 , z 11 ∈ C   and | z 00 | 2 + | z 01 | 2 + | z 10 | 2 + | z 11 | 2 = 1   , is the general form of the states of an isolated pair of qubits. Returning to the design of EQPL, we conclude that we need two qubit symbols for working with two qubits. Moreover, in this case, a quantum valuation should be a superposition of the four possible classical valuations.
It is easy to generalize this idea to a finite set of qubits. However, as usual in logic, we would like to work with a fixed, denumerable alphabet of qubit symbols:
q B = { q b k : k ∈ N } .   But, then, what should be the Hilbert space for q B   ? The answer, a key ingredient of the envisaged EQPL semantics, is the Hilbert space ℋ = ℋ ( 2 q B )   that we define by free construction from the set 2 q B   of all classical valuations over q B   . This free construction is as follows. Given an arbitrary set V   , the Hilbert space ℋ ( V )   is as follows:
  • ∙ Each element of ℋ   is a map | ψ 〉 : V → C   such that:
    • – s u p p ( | ψ 〉 ) = { v : | ψ 〉 ( v ) ≠ 0 }   is countable;
    • – ∑ v ∈ V | | ψ 〉 ( v ) | 2 = ∑ v ∈ s u p p ( | ψ 〉 ) | | ψ 〉 ( v ) | 2 < ∞   .
  • ∙ | ψ 1 〉 + | ψ 2 〉 = λ v . | ψ 1 〉 ( v ) + | ψ 2 〉 ( v )   .
  • ∙ α | ψ 〉 = λ v . α | ψ 〉 ( v )   .
  • ∙ 〈 ψ 1 | ψ 2 〉 = ∑ v ∈ V | ψ 1 〉 ( v ) ¯ | ψ 2 〉 ( v )   .
The inner product induces the norm | | | ψ 〉 | | = 〈 ψ | ψ 〉   and, so, the distance d ( | ψ 1 〉 , | ψ 2 〉 ) = | | | ψ 1 〉 − | ψ 2 〉 | |   . Since ℋ ( V )   is complete for this distance, ℋ ( V )   is a Hilbert space 1   .
Given v ∈ 2 q B   , | v 〉   is the vector of ℋ   defined as follows: | v 〉 ( v ) = 1   and | v 〉 ( v ′ ) = 0   for every v ′ ≠ v   . Observe that { | v 〉 : v ∈ V }   is an orthonormal basis of ℋ   . This basis will play an important role in the semantics of EQPL and for this reason we refer to it as being the logical basis of ℋ   .
The unit vectors of ℋ   are the envisaged quantum valuations over q B   .
Given a quantum valuation | ψ 〉   and a classical valuation v   , the inner product 〈 v | ψ 〉   is said to be the logical amplitude of | ψ 〉   for v   . As we shall see, these logical amplitudes are at the core of EQPL. Observe that it is useful to be able to work with a constrained set V   of admissible classical valuations. That is, it is sometimes convenient to work with V ⊊ 2 q b   . Indeed, we may want to impose classical constraints on the quantum valuations. For example, we may want to impose ( q b 1 ∨ q b 2 )   , constraining the quantum system to states giving amplitude zero to every valuation not satisfying this classical formula. Therefore, concerning the semantics of EQPL, we conclude that a quantum interpretation structure w   should contain at least a set V ⊆ 2 q B   (the set of admissible classical valuations) and a unit vector | ψ 〉   in ℋ   (the quantum valuation or the quantum state) such that 〈 v | ψ 〉 = 0   for every v ∉ V   .
Since we start with the semantics for the whole system (composed of the denumerable set q B   of qubits), what is the role of Postulate 2? More precisely, how can we identify an independent subsystem? The solution is “tensor factorization” that we proceed to explain.
Given S ⊆ q B   and V ⊆ 2 q B   , we introduce V [ S ] = { v | S : v ∈ V }   and V ] S [ = { v | q B \ S : v ∈ V }   . We also need ℋ [ S ] = ℋ ( ( 2 q B ) [ S ] )   and ℋ ] S [ = ℋ ( ( 2 q B ) ] S [ )   . Then, ℋ ( V )   is a subspace of ℋ ( 2 q B )   ; ℋ = ℋ [ S ] ⊗ ℋ ] S [   ; and ℋ ( V ) ⊆ ℋ ( V [ S ] ) ⊗ ℋ ( V ] S [ )   where equality does not hold in general.
Given a unit | ψ 〉 ∈ ℋ   , if there are unit | ψ ′ 〉 ∈ ℋ [ S ]   and unit | ψ ′ ′ 〉 ∈ ℋ ] S [   such that | ψ 〉 = | ψ ′ 〉 ⊗ | ψ ′ ′ 〉   then we say that, at state | ψ 〉   , the qubits in S   are not entangled with those outside S   . In this situation, the state | ψ 〉   is said to be S   -factorizable. Furthermore, a vector | ψ 〉 ∈ ℋ [ S ]   is said to be non factorizable if there is no proper subset S ′   of S   such that there are unit | ψ ′ 〉 ∈ ℋ [ S ′ ]   and unit | ψ ′ ′ 〉 ∈ ℋ [ S \ S ′ ]   such that | ψ 〉 = | ψ ′ 〉 ⊗ | ψ ′ ′ 〉   .
Having in mind these semantic notions, given a finite set F   of qubit symbols, we conclude that the language of EQPL should provide the means for writing assertions about:
  • ∙ non entanglement: “the qubits in F   are not entangled with the other qubits” (that is, the quantum state at hand is F   -factorizable); this assertion is made, as we shall see, with the EQPL formula [ F ]   ;
  • ∙ logical amplitudes: “the amplitude of a classical valuation over F   is equal to a complex number”; that is, we need terms denoting arbitrary complex numbers and terms denoting logical amplitudes; more precisely, as we shall see, when the quantum state is F   -factorizable, the EQPL term | ⊤ 〉 F A   denotes the amplitude of the (unique) classical valuation v A F   over target F   that satisfies the qubits in A ⊆ F   and does not satisfy the qubits in F \ A   .
Other useful quantum constructions will be introduced as abbreviations, including inter alia:
  • ∙ [ G | F ]   – formula stating that the quantum state is G   -factorizable if it is F   -factorizable.
  • ∙ | α 〉 F A   – term roughly denoting the amplitude of v A F   if this classical valuation satisfies α   , and equal to zero otherwise.
  • ∙ ( [ F ] ◊ α : u )   – formula stating that the quantum state is F   -factorizable and that there is a classical valuation over F   in the F   -component of the quantum state satisfying α   and with non null amplitude u   .
Unfortunately, the amplitude terms are not always meaningful on a given pair ( V , | ψ 〉 )   . Namely, they require that the target qubits are not entangled with the others. Therefore, we need more information in the envisaged notion of quantum interpretation structure. But, before we are ready to give the definition, we need some additional notation about partitions of q B   . Given a partition S   of q B   , let ∪ S   be the set of all unions of elements of S   . That is, ∪ S = { ∪ S ∈ ℛ S : ℛ ⊆ S }   .
A quantum interpretation structure is a tuple w = ( V , S , | ψ 〉 , ν )   where:
  • ∙ V   is a nonempty subset of 2 q B   .
  • ∙ S   is a finite partition of q B   .
  • ∙ | ψ 〉 = { | ψ 〉 [ R ] } R ∈ ∪ S   where each | ψ 〉 [ R ]   is a unit vector of ℋ [ R ]   and such that:
    • 1. | ψ 〉 [ ∅ ] = e i 0   ;
    • 2. | ψ 〉 [ R ] = ⊗ S ∈ S S ⊆ R | ψ 〉 [ S ]   for each non empty R ∈ ∪ S   ;
    • 3. | ψ 〉 [ S ]   is non factorizable for each S ∈ S   ;
    • 4. 〈 v | ψ 〉 [ q B ] = 0   if v ∉ V   .
  • ∙ ν : { ν F A } F ⊆ fin q B , A ⊆ F   where each ν F A ∈ C   and ν F A = 〈 v A F | ψ 〉 [ F ]   if F ∈ ∪ S   .
In such a structure we recognize the key elements V   (the set of admissible classical valuations) and | ψ 〉 [ q B ]   (the quantum state of the whole system).
The additional information is the factorization of | ψ 〉 [ q B ]   and the map ν   that provides the means for interpreting amplitude terms even when they are physically undefined. In this way we avoided the need to work with partial interpretation structures. Observe also that, although we work in ℋ = ℋ ( 2 q B )   , clause 4 in the definition above imposes that (up to isomorphism) we only consider quantum states in ℋ ( V )   .
As we just saw, Postulates 1-2 were sufficient to guide us in the task of setting up the notion of quantum interpretation structure over which we shall be able to define the semantics of EQPL. Now, we turn our attention to the postulates concerning measurements of physical quantities.
Postulate 3: Every measurable physical quantity of an isolated quantum system is described by an observable acting on its Hilbert space.
Recall that an observable is a Hermitian operator such that the direct sum of its eigensubspaces coincides with the underlying Hilbert space. Since the operator is Hermitian, its spectrum Ω   (the set of its eigenvalues) is a subset of R   . For each e ∈ Ω   , we denote the corresponding eigensubspace by E e   and the projector onto E e   by P e   .
Postulate 4: The possible outcomes of the measurement of a physical quantity are the eigenvalues of the corresponding observable. When the physical quantity is measured using observable A   on a system in a state | ψ 〉   , the resulting outcomes are ruled by the probability space P | ψ 〉 A = ( Ω , ℬ | Ω , μ | ψ 〉 A )   where in the case of a countable spectrum μ | ψ 〉 A = λ B . ∑ e ∈ Ω χ B ( e ) | P e | ψ 〉 | 2 .   For the applications we have in mind in quantum computation and information, only logical projective measurements over a finite set of qubits are relevant. Given a quantum structure w = ( V , S , | ψ 〉 , ν )   , for each finite set F   of qubits, such measurements are defined using some observable A F   on ℋ   such that:
  • ∙ The spectrum of A F   is equipotent 2   to V [ F ]   .
  • ∙ For each v ′ ∈ V [ F ]   , the corresponding eigenspace E v ′   is generated by all vectors of the form | v ′ 〉 ⊗ | v ′ ′ 〉   in ℋ   . Thus, each projector P v ′   is | v ′ 〉 〈 v ′ | ⊗ 1 ℋ ] F [   .
For example, if the system is in the particular state α 00 ω 1 | 00 ω 1 〉 + α 01 ω 2 | 01 ω 2 〉 + α 01 ω 3 | 01 ω 3 〉 + α 10 ω 4 | 10 ω 4 〉   then the probability of observing the first two qubits q b 0 , q b 1   in the classical valuation 01   is given by | α 01 ω 2 | 2 + | α 01 ω 3 | 2   .
In general, the stochastic result of making a logical projective measurement of a finite set F   of qubits of the system at w = ( V , S , | ψ 〉 , ν )   is fully described by the finite probability space P w F = ( V [ F ] , ℘ V [ F ] , μ w F )   where, for each U ⊆ V [ F ]   :
μ w F ( U ) = ∑ v ′ ∈ U ∑ v ′ ′ ∈ V ] F [ | 〈 ( v ′ ⊕ v ′ ′ ) | ψ 〉 | 2 .   Here, v ′ ⊕ v ′ ′   denotes the (unique) classical valuation over all qubits determined by v ′   and v ′ ′   . Thus, we are able to say what is the probability in a given quantum state of observing a classical formula α   as being true. That is, given a quantum structure w   , we have the means for interpreting EQPL terms of the form ( ∫ α )   that denote such probabilities.
Finally, although irrelevant to the design of EQPL, we mention en passant Postulate 5 that rules how quantum systems evolve.
Postulate 5: Excluding measurements, the evolution of a quantum system is described by unitary transformations.
This last postulate becomes relevant only when designing a dynamical extension of EQPL (see [18] ).

1   Isomorphic to L 2 ( V , # )   where #   is the counting measure over V   .

3 Language and semantics

The language of EQPL is composed of classical formulae, real terms, complex terms and quantum formulae that we proceed to introduce using an abstract version of the BNF notation [20] for a compact presentation of inductive definitions. For building terms, it is convenient to use real variables X = { x k : k ∈ N }   and complex variables Z = { z k : k ∈ N }   .
Classical formulae:
α : = q b ∀ ( ¬ α ) ∀ ( α ⇒ α )   As usual, other classical connectives like ∧ , ∨ , ⇔   , verum ⊤   and falsum ⊥   are introduced as abbreviations. We denote the set of qubit symbols occurring in α   by q B ( α )   . We say that a classical formula α   is over a set S   of qubit symbols if q B ( α ) ⊆ S   .
Real and complex terms (with the provisos computable real constant r   , finite F ⊂ q B   and A ⊆ F   ):
{ t : = x ∀ r ∀ ( ∫ α ) ∀ ( t + t ) ∀ ( t t ) ∀ R e ( u ) ∀ I m ( u ) ∀ arg ( u ) ∀ | u | u : = z ∀ | ⊤ 〉 F A ∀ ( t + i t ) ∀ t e i t ∀ u ¯ ∀ ( u + u ) ∀ ( u u ) ∀ ( α ⊲ u ; u )   Most of these terms are self-explanatory or already motivated in the previous section. An explanation is needed concerning complex alternative terms: a term ( α ⊲ u 1 ; u 2 )   denotes the value denoted by u 1   if α   is true, and denotes the value denoted by u 2   otherwise.
Quantum formulae (with the proviso finite F ⊂ q B   ):
γ : = α ∀ ( t ≤ t ) ∀ [ F ] ∀ ( ⊟ γ ) ∀ ( γ ⊐ γ )   Quantum negation ⊟   and quantum implication ⊐   are global operators and should not be confused with their classical (local) counterparts. As expected, other quantum connectives will be introduced as abbreviations. But, before introducing the whole set of useful abbreviations, we present the semantics of the language.
Given a set S   of qubit symbols and a set V   of valuations, the extent at V   of classical formulae over S   is as follows:
  • ∙ | α | V S = { v ∈ V [ S ] : v ⊩ c α }   .
By an assignment ρ   we mean a map such that ρ ( x ) ∈ R   for each x ∈ X   and ρ ( z ) ∈ C   for each z ∈ Z   .
The denotation of terms at w = ( V , S , | ψ 〉 , ν )   and ρ   is inductively defined as follows (we refrain from spelling out the obvious clauses for interpreting arithmetical expressions):
  • ∙ [ [ x ] ] w ρ = ρ ( x )   ;
  • ∙ [ [ r ] ] w ρ = r   ;
  • ∙ [ [ ( ∫ α ) ] ] w ρ = μ w q B ( α ) ( | α | V q B ( α ) )   ;
  • ∙ [ [ z ] ] w ρ = ρ ( z )   ;
  • ∙ [ [ | ⊤ 〉 F A ] ] w ρ = ν F A   ;
  • ∙ [ [ ( α ⊲ u 1 ; u 2 ) ] ] w ρ = { [ [ u 1 ] ] w ρ if w ρ ⊩ α [ [ u 2 ] ] w ρ otherwise   ;
  • ∙ . . .
The satisfaction of quantum formulae at w = ( V , S , | ψ 〉 , ν )   and ρ   is inductively defined as follows:
  • ∙ w ρ ⊩ α   iff v ⊩ c α   for every v ∈ V   ;
  • ∙ w ρ ⊩ ( t 1 ≤ t 2 )   iff [ [ t 1 ] ] w ρ ≤ [ [ t 2 ] ] w ρ   ;
  • ∙ w ρ ⊩ [ F ]   iff F ∈ ∪ S   ;
  • ∙ w ρ ⊩ ( ⊟ γ )   iff w ρ ⊮ γ   ;
  • ∙ w ρ ⊩ ( γ 1 ⊐ γ 2 )   iff w ρ ⊮ γ 1   or w ρ ⊩ γ 2   .
As anticipated in the previous section, the proposed quantum language with the semantics above is rich enough to express interesting properties of quantum systems. To this end, it is quite useful to introduce other operations, connectives and modalities through abbreviations. We start with some additional quantum connectives:
  • ∙ quantum disjunction: ( γ 1 ⊔ γ 2 )   for ( ( ⊟ γ 1 ) ⊐ γ 2 )   ;
  • ∙ quantum conjunction: ( γ 1 ⊓ γ 2 )   for ( ⊟ ( ( ⊟ γ 1 ) ⊔ ( ⊟ γ 2 ) ) )   ;
  • ∙ quantum equivalence: ( γ 1 ≡ γ 2 )   for ( ( γ 1 ⊐ γ 2 ) ⊓ ( γ 2 ⊐ γ 1 ) )   .
Observe that the quantum connectives are classical in the sense that quantum tautologies hold. For instance, ( ( ( ⊟ γ 2 ) ⊐ ( ⊟ γ 1 ) ) ⊐ ( γ 1 ⊐ γ 2 ) )   is satisfied by every quantum structure and assignment. But they do not coincide with the classical connectives! For instance, ( ¬ α )   entails ( ⊟ α )   but not the other way around. For a more detailed discussion of the differences and relationship between these two versions of classical logic refer to [19] .
It is also useful to introduce some additional comparison predicate symbols:
  • ∙ ( t 1 < t 2 )   for ( ( t 1 ≤ t 2 ) ⊓ ( ⊟ ( t 2 ≤ t 1 ) ) )   ;
  • ∙ ( t 1 = t 2 )   for ( ( t 1 ≤ t 2 ) ⊓ ( t 2 ≤ t 1 ) )   ;
  • ∙ ( u 1 = u 2 )   for ( ( R e ( u 1 ) = R e ( u 2 ) ) ⊓ ( I m ( u 1 ) = I m ( u 2 ) ) )   .
Classical molecular formulae (classical conjunctions of literals) are used profusely in the sequel. To this end, we introduce the following abbreviation (with the provisos finite F ⊂ q B   and A ⊆ F   ):
  • ∙ ( ∧ F A )   for ( ( ∧ q b k ∈ A q b k ) ∧ ( ∧ q b k ∈ ( F \ A ) ( ¬ q b k ) ) )   .
Observe that the formula ( ∧ F A )   specifies the unique classical valuation v A F   over F   that satisfies the qubits in A   and does not satisfy the qubits in F \ A   .
Logical amplitude terms are easily extended to any classical formula besides verum (with the provisos q B ( α ) ⊆ F   , finite F ⊂ q B   and A ⊆ F   ):
  • ∙ | α 〉 F A   for ( ( ( ∧ F A ) ⇒ α ) ⊲ | ⊤ 〉 F A ; 0 )   .
Intuitively, | α 〉 F A   coincides with | ⊤ 〉 F A   if v A F   satisfies α   , and it is zero otherwise.
Logical amplitude vector terms are introduced as follows (with the proviso q B ( α ) ⊆ F   ):
  • ∙ | α 〉 F   for ( | α 〉 F A ) A ⊆ F   .
It turns out that it is convenient to introduce the additional syntactic category of logical amplitude vector terms for each finite set F   of qubit symbols:
| ω 〉 F = | α 〉 F ∀ ( u | ω 〉 F ) ∀ ( | ω 〉 F + | ω 〉 F )   with the obvious abbreviation rules for multiplication by scalar and addition.
Still concerning amplitude vector terms, the following abbreviations are handy:
  • ∙ | 0 〉 F   for ( 0 | ⊤ 〉 F )   ;
  • ∙ ( | ω 1 〉 F = | ω 2 〉 F )   for ( ⨅ A ⊆ F ( | ω 1 〉 F A = | ω 2 〉 F A ) )   ;
  • ∙ ( | ω 1 〉 F ⊆ | ω 2 〉 F )   for ( ⨅ A ⊆ F ( ( | ω 1 〉 F A ≠ 0 ) ⊐ ( | ω 1 〉 F A = | ω 2 〉 F A ) ) )   .
Finally, we are ready to introduce the rest of the interesting quantum operations, predicates and modalities:
  • ∙ [ G | F ]   for ( ⨅ A ′ ⊆ G ⨅ A ′ ′ ⊆ F \ G ( | ⊤ 〉 F ( A ′ A ′ ′ ) = | ⊤ 〉 G A ′ | ⊤ 〉 ( F \ G ) A ′ ′ ) )   ;
  • ∙ ( q b k 1 ∼ F q b k 2 )   for ( ⊟ ( ⨆ G ⊂ F q b k 1 ∈ G q b k 2 / ∈ G [ G ] ) )   ;
  • ∙ ( [ F ] ◊ α : u )   for ( [ F ] ⊓ | u | > 0 ⊓ ( ⨆ A ⊆ F ( | α 〉 F A = u ) ) )   ;
  • ∙ ( [ F ] ◊ α 1 : u 1 , . . . , α n : u n )   for ( ( [ F ] ◊ α 1 : u 1 ) ⊓ . . . ⊓ ( [ F ] ◊ α n : u n ) )   ;
  • ∙ ( ◊ α )   for ( 0 < ( ∫ α ) )   ;
  • ∙ ( □ α )   for ( 1 = ( ∫ α ) )   .
Most of these quantum constructions were already discussed in the previous section. The entanglement formula ( q b k 1 ∼ F q b k 2 )   states that the two qubits are entangled.
Quantum molecular formulae (quantum conjunctions of literals) are also very useful. Note that a quantum literal is either a quantum atom or the quantum negation of a quantum atom. Looking at the grammar of quantum formulae, it is clear that quantum atoms are either classical formulae, or comparisons between real terms or non entanglement assertions:
q A t o m : = α ∀ ( t ≤ t ) ∀ [ F ]   To this end, we introduce the following abbreviation (with the provisos finite Q ⊂ q A t o m   and D ⊆ Q   ):
  • ∙ ( ⨅ Q D )   for ( ( ⨅ δ ∈ D δ ) ⊓ ( ⨅ δ ∈ ( Q \ D ) ( ⊟ δ ) ) )   .
Observe that a quantum molecular formula defines a set of quantum structures that may be empty because, for instance, the quantum molecular formula ( α ⊓ ( ¬ α ) )   has no models (here Q = { α , ( ¬ α ) } = D   ).
We finish this section with a simple example. Consider the following variant of Schrödinger's cat. The relevant attributes of the cat are: being inside or outside the box, alive or dead, and moving or still. These three attributes are represented by the qubits q b 0 , q b 1 , q b 2   , respectively. For the sake of readability we use instead cat-in-box , cat-alive , cat-moving   , respectively.
The following EQPL formulae constrain the state of the cat at different levels of detail:
  • 1. [ cat-in-box , cat-alive , cat-moving ]   ;
  • 2. ( cat-moving ⇒ cat-alive )   ;
  • 3. ( ( ◊ cat-alive ) ⊓ ( ◊ ( ¬ cat-alive ) ) )   ;
  • 4. ( ⊟ [ cat-alive ] )   ;
  • 5. ( ( ∫ cat-alive ) = 1 3 )   ;
  • 6. ( [ cat-alive , cat-moving ] ◊ ( cat-alive ∧ cat-moving ) : 1 6 , ( cat-alive ∧ ( ¬ cat-moving ) ) : 1 6 , ( ( ¬ cat-alive ) ∧ ( ¬ cat-moving ) ) : e i π 3 2 3 )   .
Observe that the assertions above are consistent with each other. Intuitively, assertion 1 states that the qubits cat-in-box , cat-alive , cat-moving   are not entangled with the other qubtis of the cat system. Assertion 2 is a classical constraint on the set of admissible valuations: if the cat is moving then it is alive.
Assertion 3 states the famous paradox: the cat can be in a state where it is possible that the cat is alive and it is possible that the cat is dead. Assertion 4 states that the qubit cat-alive   is entangled with other qubits. Assertion 5 states that the cat is in a state where the probability of observing it alive (after collapsing the wave function) is 1 3   . Finally, assertion 6 states that the qubits cat-alive , cat-moving   are not entangled with other qubits and that in the quantum state there is a classical valuation with amplitude 1 6   where the cat is alive and moving, there is another classical valuation also with amplitude 1 6   where the cat is alive and not moving, and there is a classical valuation with amplitude e i π 3 2 3   where the cat is dead (and, thus, thanks to 2, also not moving).

4 Axiomatization

Entailment for EQPL may be defined as expected – we say that Γ   entails δ   , written Γ ⊨ η   , if w ρ ⊩ η   for every w   and ρ   satisfying every element of Γ   .
But a finitely bounded version of entailment turns out to be more relevant.
Given a finite set F   of qubit symbols, a quantum structure w = ( V , S , ψ , ν )   is said to be F   -factorizable if F ∈ ∪ S   . Given a set Γ   of quantum formulae over F   and a quantum formula η   also over F   , we say that the former F   -entails the latter, written Γ ⊨ F η   if w ρ ⊩ η   for every F   -factorizable w   and ρ   satisfying every element of Γ   .
Observe that Γ ⊨ η   implies Γ ⊨ F η   for every F   . Furthermore, for any Γ   and η   over F 1   , if F 1 ⊆ F 2   and Γ ⊨ F 2 η   then Γ ⊨ F 1 η   . Note also that Γ , η 1 ⊨ F η 2   iff Γ ⊨ F ( η 1 ⊐ η 2 )   , and a similar result holds for the unbounded entailment. That is, quantum implication does internalize the notion of quantum entailment in EQPL. It is also straightforward to verify that both entailments (unbounded and bounded) are not compact in the sense that there are Γ   and η   such that η   is entailed by Γ   but it is not entailed by any finite subset of Γ   . Therefore, there is no hope of setting up a finitary axiomatization (that is, using only finitary rules) achieving strong completeness. But, it is possible to establish a finitary axiomatization that achieves F   -bounded weak completeness for any finite F   : ⊨ F η   iff ⊢ F η   . Indeed, the axioms and rules presented below are sound and adequate for F   -validity as will be proved in the next section.
Before listing all axioms and rules we need to introduce the concept of tautological quantum formula or quantum tautology. A quantum formula γ   is said to be tautological if there are a classical tautology α   and a substitution map σ : q B → q A t o m   such that γ   coincides with α ⊟ , ⊐ ¬ , ⇒ σ   . For instance, the quantum formula ( ( x 1 ≤ x 2 ) ⊐ ( x 1 ≤ x 2 ) )   is tautological (obtained, for example, from the classical tautology ( q b 1 ⇒ q b 1 )   ). We also need the concept of arithmetical language:
υ : = ( a ≤ a ) ∀ ( ⊟ υ ) ∀ ( υ ⊐ υ )
a : = x ∀ r ∀ ( a + a ) ∀ ( a a ) ∀ R e ( b ) ∀ I m ( b ) ∀ arg ( b ) ∀ | b |
b : = z ∀ ( a + i a ) ∀ a e i a ∀ b ¯ ∀ ( b + b ) ∀ ( b b )
Observe that an assignment ρ   is enough to interpret arithmetical formulae.
An arithmetical formula υ   is said to be valid if it is satisfied by every assignment. For instance, ( ( ( t 1 ≤ t 2 ) ⊓ ( t 2 ≤ t 3 ) ) ⊐ ( t 1 ≤ t 3 ) )   and ( ( u 1 2 = − 1 ) ⊐ ( ( u 1 = i ) ⊔ ( u 1 = − i ) ) )   are both universal arithmetical formulae (the latter using equality between complex numbers introduced as an abbreviation). We are now ready to list the axioms and rules of our calculus for each finite set F   of qubit symbols:
  • ∙ ⊢ F α   for each classical tautology α   [CTaut].
  • ∙ α 1 , ( α 1 ⇒ α 2 ) ⊢ F α 2   [CMP].
  • ∙ ⊢ F γ   for each quantum tautology γ   [QTaut].
  • ∙ γ 1 , ( γ 1 ⊐ γ 2 ) ⊢ F γ 2   [QMP].
  • ∙ ⊢ F υ t ⃗ u ⃗ x ⃗ z ⃗   for each valid arithmetical formula υ   [Oracle].
  • ∙ ⊢ F ( ( α 1 ⇒ α 2 ) ⊐ ( α 1 ⊐ α 2 ) )   [Lift ⇒   ].
  • ∙ ⊢ F ( ( α 1 ⊓ α 2 ) ⊐ ( α 1 ∧ α 2 ) )   [Ref ⊓   ].
  • ∙ ⊢ F ( α ⊐ ( ( α ⊲ u 1 ; u 2 ) = u 1 ) )   [If ⊤   ].
  • ∙ ⊢ F ( ( ⊟ α ) ⊐ ( ( α ⊲ u 1 ; u 2 ) = u 2 ) )   [If ⊥   ].
  • ∙ ⊢ F [ F ]   [NEtg F   ].
  • ∙ ⊢ F ( [ G 2 ] ⊐ ( [ G 1 ] ≡ [ G 1 | G 2 ] ) )   for any G 1 ⊆ G 2   [NEtg |   ].
  • ∙ ⊢ F ( [ G 1 ] ⊐ ( [ G 2 ] ⊐ [ G 1 ∪ G 2 ] ) )   [NEtg ∪   ].
  • ∙ ⊢ F ( [ G 1 ] ⊐ ( [ G 2 ] ⊐ [ G 1 \ G 2 ] ) )   [NEtg \   ].
  • ∙ ⊢ F ( | ⊤ 〉 ∅ ∅ = 1 )   [Empty].
  • ∙ ⊢ F ( ( ¬ ( ∧ F A ) ) ⊐ ( | ⊤ 〉 F A = 0 ) )   [NAdm].
  • ∙ ⊢ F ( [ G ] ⊐ ( ( ∑ A ⊆ G | | ⊤ 〉 G A | 2 ) = 1 ) )   [Unit].
  • ∙ ⊢ F ( ( ∫ α ) = ( ∑ A ⊆ F | | α 〉 F A | 2 ) )   [Prob].
In total, we have only two rules (modus ponens for classical implication [CMP] and for quantum implication [QMP] 3   ) and fifteen axioms. The axioms are better understood in the following groups.
We have as axioms the classical tautologies and the quantum tautologies ([CTaut] and [QTaut], respectively). Since the set of classical tautologies and the set of quantum tautologies are both recursive, there is no need to spell out the details of tautological reasoning. Axiom [Oracle] is more controversial – we accept as an axiom any valid arithmetical formula. The set of valid arithmetical formulae is not even recursively enumerable, hence the name we chose for the axiom. We decided to use an arithmetical oracle for two reasons. First, we wanted to focus our attention on reasoning about quantum aspects without becoming lost in arithmetical details. And, second, the alternative of presenting a recursive axiomatization based on the theory of algebraic closed fields would require, in order to maintain completeness, a relaxation of our semantics, maybe towards a point too far away from its intuitive roots in the postulates of quantum mechanics. However, this alternative is interesting also for other reasons and we shall come back to the issue in the last section of the paper.
Axioms [Lif ⇒   ] and [Ref ⊓   ] are sufficient to relate (local) classical reasoning and (global) quantum tautological reasoning. Again, we refer to [19] for more details.
Axioms [If ⊤   ] and [If ⊥   ] are self explanatory. They will be used in the completeness proof to remove alternative terms.
Axioms [NEtg F   ], [NEtg |   ], [NEtg ∪   ] and [NEtg \   ] are enough to reason about non entanglement. Among other things they impose that non entanglement is closed under set theoretic operations (closure under intersection appears as a theorem as we shall see).
Axioms [Empty], [NAdm] and [Unit] rule logical amplitudes. Each of them closely reflects a property of our semantic structures.
Finally, axiom [Prob] relates probabilities and amplitudes, closely following Postulate 4.
As expected, we say that a formula η   over F   is an F   -theorem, written ⊢ F η   if we can build a derivation of η   from the axioms using the rules (for F   ). As an illustration, consider the following derivation that establishes for any finite F   :
  • ∙ ⊢ F ( ( ∫ ⊤ ) = 1 )   [PUnit].
1 [ F ]   NEtg F   2 ( [ F ] ⊐ ( ( ∑ A ⊆ F | | ⊤ 〉 F A | 2 ) = 1 ) )   Unit 3 ( ( ∑ A ⊆ F | | ⊤ 〉 F A | 2 ) = 1 )   QMP:1,2 4 ( ( ∫ ⊤ ) = ( ∑ A ⊆ F | | ⊤ 〉 F A | 2 ) )   Prob 5 ( ( ( ∫ ⊤ ) = ( ∑ A ⊆ F | | ⊤ 〉 F A | 2 ) ) ⊐ ( ( ( ∑ A ⊆ F | | ⊤ 〉 F A | 2 ) = 1 ) ⊐ ( ( ∫ ⊤ ) = 1 ) ) )   Oracle 6 ( ( ( ∑ A ⊆ F | | ⊤ 〉 F A | 2 ) = 1 ) ⊐ ( ( ∫ ⊤ ) = 1 ) )   QMP:4,5 7 ( ( ∫ ⊤ ) = 1 )   QMP:3,6
We finish this section with a list of interesting F   -theorems. Some of them will be used in the proof of weak completeness presented in the next section, but others are mentioned just for illustration purposes.
The following theorem is a direct consequence of the non entanglement axioms and completes the picture of non entanglement being closed under set theoretic operations.
  • ∙ ⊢ F ( [ G 1 ] ⊐ ( [ G 2 ] ⊐ [ G 1 ∩ G 2 ] ) )   [NEtg ∩   ].
The following theorems give some insight on the major properties of logical amplitudes.
  • ∙ ⊢ F ( ( | ( α 1 ∨ α 2 ) 〉 G + | ( α 1 ∧ α 2 ) 〉 G ) = ( | α 1 〉 G + | α 2 〉 G ) )   [AAdd].
  • ∙ ⊢ F ( ( α 1 ⇒ α 2 ) ⊐ ( | α 1 〉 G ⊆ | α 2 〉 G ) )   [AMon].
  • ∙ ⊢ F ( ( α 1 ⇔ α 2 ) ⊐ ( | α 1 〉 G = | α 2 〉 G ) )   [ASoE].
  • ∙ ⊢ F ( α ⊐ ( | α 〉 G = | ⊤ 〉 G ) )   [ANec].
  • ∙ ⊢ F ( ( | α 〉 G + | ( ¬ α ) 〉 G ) = | ⊤ 〉 G )   [AMExc].
The first of the following theorems about probability after measurements just states finite additivity. The second is an obvious instance of Postulate 4. The third relates logical reasoning with probability reasoning (monotonicity).
  • ∙ ⊢ F ( ( ( ∫ ( α 1 ∨ α 2 ) ) + ( ∫ ( α 1 ∧ α 2 ) ) ) = ( ( ∫ α 1 ) + ( ∫ α 2 ) ) )   [PAdd].
  • ∙ ⊢ F ( ( [ G ] ◊ ( ∧ G A ) : u ) ⊐ ( ( ∫ ( ∧ G A ) ) = | u | 2 ) )   [Meas].
  • ∙ ⊢ F ( ( α 1 ⇒ α 2 ) ⊐ ( ( ∫ α 1 ) ≤ ( ∫ α 2 ) ) )   [PMon].
The following theorems show that the quantum and probability modalities do behave as normal modalities.
  • ∙ ⊢ F ( ( [ G ] ◊ ( α ∨ α ′ ) : u ) ≡ ( ( [ G ] ◊ α : u ) ⊔ ( [ G ] ◊ α ′ : u ) ) )   [QNorm].
  • ∙ ⊢ F ( ( α ⇒ α ′ ) ⊐ ( ( [ G ] ◊ α : u ) ⊐ ( [ G ] ◊ α ′ : u ) ) )   [QMon].
  • ∙ ⊢ F ( ( u = u ′ ) ⊐ ( ( [ G ] ◊ α : u ) ⊐ ( [ G ] ◊ α : u ′ ) ) )   [QCong].
  • ∙ ⊢ F ( α ⊐ ( □ α ) )   [PNec].
  • ∙ ⊢ F ( ( □ ( α ⇒ α ′ ) ) ⊐ ( ( □ α ) ⊐ ( □ α ′ ) ) )   [PNorm].

3   Actually, [CMP] can be derived from [QMP] and [Lift ⇒   ].

5 Proof of bounded weak completeness

It is straightforward to prove that the calculus presented in the last section is strongly sound – for any finite F ⊂ q B   , if Γ ⊢ F η   then Γ ⊨ F η   .
Therefore, it is also weakly sound.
On the other hand, as already pointed out, it is not possible to achieve strong adequacy with a finitary calculus. But, for arbitrary finite F ⊂ q B   , we were able to prove F   -bounded adequacy of the calculus – if ⊨ F η   then Γ ⊢ F η   . Therefore, since we have soundness, our calculus is F   -bounded weakly complete – ⊨ F η   iff ⊢ F η   .
The quantitative nature of the language of EQPL raises specific problems when proving an adequacy result. These problems appear on top of those raised by the fact the calculus is not strongly complete. Thus, the traditional Henkin approach to adequacy proofs [13] is not the answer here, or, at least, is not the full answer.
In the end, we were inspired by the Fagin-Halpern-Megiddo technique that was successfully applied in proving adequacy results for probability calculi [11] . The key step of this technique is the reduction of any formula to a disjunction of systems of linear inequations over the real numbers where each variable represents the probability of a classical molecular formula. A close exam of the technique suggests that it should be applicable (possibly after a suitable non trivial extension) to any quantitative logic where the disjunctive normal form lemma holds.
Actually, a quite significant revamp of the Fagin-Halpern-Megiddo technique was needed in order to cope with the novel aspects of EQPL: (i) classical formulae mixed with arithmetic (in)equations; (ii) global semantics of quantum connectives; (iii) non entanglement atoms; (iv) amplitude terms besides probability terms; and (v) quantum structures instead of probability spaces.
Note that the Fagin-Halpern-Meggido technique was first developed for a probabilistic logic somewhat simpler than the probabilistic fragment of EQPL. In addition, we used the Henkin technique thrice: (i) for removing alternative terms; (ii) for constructing the set of admissible valuations; and (iii) for building the finite partition of the set of qubits.
The rest of this section contains a step by step presentation of the proof of the F   -bounded weak adequacy of EQPL. Given a quantum formula γ   over F   we say that it is F   -consistent if ⊬ F ( ⊟ γ )   . The proof is carried out by contraposition:
  • 1. Assume that ⊬ F γ   .
  • 2. So, quantum tautologically, also ⊬ F ( ⊟ ( ⊟ γ ) )   .
  • 3. Thus, ( ⊟ γ )   is F   -consistent.
  • 4. Therefore, by the main lemma proved below, there are F   -factorizable w   and ρ   such that w ρ ⊩ ( ⊟ γ )   .
  • 5. And, hence, it is not true that every such pair satisfies γ   , that is, we established that ⊭ F γ   .
It remains to prove the model existence lemma: If γ   is F   -consistent then there are F   -factorizable w   and ρ   such that w ρ ⊩ γ   .
The quantum disjunctive normal form lemma holds in EQPL. Thus: ⊢ F ( γ ≡ ⨆ D ∈ qmols ( γ ) ( ⊓ Q γ D ) )   where qmols ( γ ) = { D ⊆ Q γ : ⊢ F ( ( ⊓ Q γ D ) ⊐ γ ) }   and Q γ   is the set of F   -quantum atoms used in γ   .
Clearly, γ   is F   -consistent iff there is D ∈ qmols ( γ )   such that ( ⊓ Q γ D )   is F   -consistent. Therefore, it is sufficient to prove the following restricted model existence lemma: If ( ⊓ Q D )   is F   -consistent then there are F   -factorizable w   and ρ   such that w ρ ⊩ ( ⊓ Q D )   .
Since D = D c ∪ D ≤ ∪ D [ ]   , where D c ⊆ Q c = { α : α ∈ Q }   , D ≤ ⊆ Q ≤ = { ( t ≤ t ′ ) : ( t ≤ t ′ ) ∈ Q }   , and D [ ] ⊆ Q [ ] = { [ G ] : [ G ] ∈ Q }   , we have:
( ⊓ Q D ) = ( ( ⊓ Q c D c ) ⊓ ( ⊓ Q ≤ D ≤ ) ⊓ ( ⊓ Q [ ] D [ ] ) ) .   Our goal is to reduce everything to inequations. We start by getting rid of the non entanglement atoms.
Thanks to NEtg F   and NEtg |   , we know that there is a quantum formula δ [ ]   without non entanglement atoms such that ⊢ F ( ( ⊓ Q [ ] D [ ] ) ≡ δ [ ] )   . Thus, ⊢ F ( ( ⊓ Q D ) ≡ δ )   where δ = ( ( ⊓ Q c D c ) ⊓ ( ⊓ Q ≤ D ≤ ) ⊓ δ [ ] )   .
Note that δ [ ]   and, hence, δ   are not necessarily conjunctions of quantum literals (because it may happen that a [ G ]   appears in Q [ ] \ D [ ]   and such a negation involves a disjunction). Using again the quantum disjunctive normal form lemma we have: ⊢ F ( δ ≡ ⨆ D ∈ qmols ( δ ) ( ⊓ Q δ D ) ) .   So, δ   is F   -consistent iff there is D ∈ qmols ( δ )   such that ( ⊓ Q δ D )   is F   -consistent.
Therefore, it is sufficient to prove the following even more restricted model existence lemma: If ( ⊓ Q D )   without entanglement atoms is F   -consistent then there are F   -factorizable w   and ρ   such that w ρ ⊩ ( ⊓ Q D )   .
Assume that ( ⊓ Q D )   is F   -consistent and does not involve non entanglement atoms (that is, Q = Q c ∪ Q ≤   and D = D c ∪ D ≤   ). Our goal is to find an F   -factorizable w = ( V , S , | ψ 〉 , ν )   and a ρ   satisfying this molecular formula.
We start by looking for V   .
Before setting up V   , it is necessary to eliminate the probability and alternative terms and to add maximally consistent information about the admissible classical valuations. This desideratum is achieved as follows:
  • 1. First, we replace in ( ⊓ Q D )   each term ( ∫ α )   by ∑ A ⊆ F | α 〉 F A   . Let ( ⊓ Q ¯ D ¯ )   be the result.
  • 2. Consider an ordering α 1 , . . . , α m   of the guards of alternative terms occurring in ( ⊓ Q ¯ D ¯ )   .
  • 3. Consider the following sequence of formulae:
    • ∙ η 0 = ( ⊓ Q ¯ D ¯ )   ;
    • ∙ η k + 1 = { ( η k ⊓ α k ) if ⊢ F ( η k ⊐ α k ) ( η k ⊓ ( ⊟ α k ) ) otherwise   .
  • 4. Observe that each η k   is still F   -consistent and a quantum molecular formula. Furthermore, η m   is maximal with respect to guards.
  • 5. Now we can replace each term ( α ⊲ u 1 ; u 2 )   occurring in η m   by:
    • ∙ u 1   if α   is a quantum literal in η m   ;
    • ∙ u 2   if ( ⊟ α )   is a quantum literal in η m   .
    Let η ¯ m   be the resulting formula.
  • 6. Consider an ordering A 1 , . . . , A m ′   of the subsets of F   .
  • 7. Consider the following sequence of formulae:
    • ∙ η 0 ′ = η ¯ m   ;
    • ∙ η k + 1 ′ = { ( η k ′ ⊓ ( ¬ ( ∧ F A k ) ) ) if ⊢ F ( η k ′ ⊐ ( ¬ ( ∧ F A k ) ) ) ( η k ′ ⊓ ( ⊟ ( ¬ ( ∧ F A k ) ) ) ) otherwise   .
  • 8. Observe that each η k ′   is still F   -consistent and a quantum molecular formula. Furthermore, η m ′ ′   does not contain probability terms or alternative terms and is maximal with respect to admissible classical valuations.
  • 9. Thanks to Prob, If ⊤   and If ⊥   , denoting the resulting still F   -consistent molecular formula by ( ⊓ Q ′ D ′ ) = ( ( ⊓ Q c ′ D c ′ ) ⊓ ( ⊓ Q ≤ ′ D ≤ ′ ) )   , we have ⊢ F ( ( ⊓ Q ′ D ′ ) ⊐ ( ⊓ Q D ) ) .  
  • 10. Therefore, we may proceed working towards the envisaged w   and ρ   with the new formula.
Having (while preserving F   -consistency) eliminated the probability and alternative terms and having determined the classical valuations, we are ready to build V   . Let V   be composed of each v ∈ 2 [ F ] q B   such that v ⊩ α   for each α ∈ D c ′   . Now we have to analyze two cases:
  • a) Either for each α ∈ Q c ′ \ D c ′   there is a v ∈ V   such that v ⊮ c α   and, therefore, this V   is viable because ( V , . . . ) ⊩ F ( ⊓ Q c ′ D c ′ ) .  
  • b) Or that is not the case. But, then, we would be able to contradict the F   -consistency of ( ⊓ Q ′ D ′ )   as follows:
    • 1. Indeed, if it is not the case then there is a α ∈ Q c ′ \ D c ′   such that v ⊩ c α   for all v ∈ V   . That is, by construction of V   , there is α ∈ Q c ′ \ D c ′   such that ⊨ c ( ( ⋀ α ′ ∈ D c ′ α ′ ) ⇒ α ) .  
    • 2. So, by CTaut, there is α ∈ Q c ′ \ D c ′   such that ⊢ F ( ( ⋀ α ′ ∈ D c ′ α ′ ) ⇒ α ) .  
    • 3. Thus, by Lift ⇒   , there is α ∈ Q c ′ \ D c ′   such that ⊢ F ( ( ⋀ α ′ ∈ D c ′ α ′ ) ⊐ α ) .  
    • 4. Thus, by Ref ⊓   and QTaut (transitivity of ⊐   ), there is α ∈ Q c ′ \ D c ′   such that ⊢ F ( ( ⨅ α ′ ∈ D c ′ α ′ ) ⊐ α ) .  
    • 5. Therefore, by QTaut (right weakening of ⊐   ) ⊢ F ( ( ⨅ α ′ ∈ D c ′ α ′ ) ⊐ ( ⨆ α ∈ Q c ′ \ D c ′ α ) )   leading to ⊢ F ( ⊟ ( ( ⨅ α ′ ∈ D c ′ α ′ ) ⊓ ( ⨅ α ∈ Q c ′ \ D c ′ ( ⊟ α ) ) ) )   by several obvious tautological steps.
    • 6. That is, we have ⊢ F ( ⊟ ( ⊓ Q c ′ D c ′ ) )   , contradicting the F   -consistency of ( ⊓ Q c ′ D c ′ )   .
In short, we did find V   satisfying the classical part of ( ⊓ Q ′ D ′ )   . Let us proceed with the construction of the partition S   . The idea is to find a maximally fine partition S F   of F   such that ( ( ⊓ Q ′ D ′ ) ⊓ ( ⊓ S ∈ S F [ S | F ] ) )   is F   -consistent, as follows:
  • 1. Let G 1 , . . . , G n   be an ordering of the subsets of F   .
  • 2. Consider the following sequence of formulae:
    • ∙ γ 0 = ( ⊓ Q ′ D ′ )   ;
    • ∙ γ k + 1 = { ( γ k ⊓ [ G k + 1 | F ] ) if this formula is F -consistent γ k otherwise   .
  • 3. Observe that each γ k   is F   -consistent and, furthermore, γ n   is maximally so with respect to non entanglement assertions.
  • 4. Let U = { G : [ G | F ] is a factor of γ n }   .
  • 5. Let S F   be composed of all minimal (with respect to inclusion) elements of U   . Then, thanks to NEnt ∩   , NEnt ∪   and NEnt \   , it is straightforward to prove that S F   is a partition of F   . Moreover, ∪ S F = U   .
  • 6. Let S = S F ∪ { q B \ F }   . Observe that S   is finite.
  • 7. Since ⊢ F ( γ n ⊐ η m )   , we proceed working with γ n   in our task of completing the construction of w   and ρ   .
It remains to find F   -factorizable | ψ 〉   , together with ν   and ρ   . As already mentioned, the key idea is to reduce everything to a system of (in)equations on variables representing amplitudes. But, first we need to add the constraints imposed by the relevant axioms. Thanks to Unit, for every G ∈ ∪ S F   , we can establish: ⊢ F ( γ n ⊐ ( ( ∑ A ⊆ G | | ⊤ 〉 G A | 2 ) = 1 ) )   . Thanks to NAdm, for every ( ¬ ( ∧ F A ) )   occurring in γ n   , we have: ⊢ F ( γ n ⊐ ( | ⊤ 〉 F A = 0 ) )   .
Let γ n ∙   be the formula ( γ n ⊓ ( ⨅ G ∈ ∪ S F ( ( ∑ A ⊆ G | | ⊤ 〉 G A | 2 ) = 1 ) ) ⊓ ( ⨅ ( ¬ ( ∧ F A ) ) in γ n ( | ⊤ 〉 F A = 0 ) ) ) .   Observe that we can derive: ⊢ F ( γ n ≡ γ n ∙ )   . Let ( γ n ∙ ) ≤   the conjunction of the (in)equations in γ n ∙   . Consider the finite system of (in)equations obtained from ( γ n ∙ ) ≤   by replacing at each term of the form | ⊤ 〉 G A   by a fresh variable z | ⊤ 〉 G A   . Now we have to analyse two cases:
  • a) Either the system of (in)equations has no solution. But, in this case we would be able to contradict the F   -consistency of γ n   as follows (using the arithmetical oracle):
    • 1. Let Λ ≤   be the (finite) set of arithmetic literals occurring in ( γ n ∙ ) ≤   and Λ c   be the (finite) set of non-arithmetic literals in ( γ n ∙ ) c   .
    • 2. Since ( γ n ∙ ) ≤ = ( ⊓ υ ∈ Λ ≤ υ )   , there is a bijection between Λ ≤   and the set of inequations composing the system described above.
    • 3. From the fact that the system of inequations induced by ( γ n ∙ ) ≤   has no solution, we conclude that there is no assignment ρ   such that ρ ⊩ υ   for all υ ∈ Λ ≤   .
    • 4. In other words, for all assignment ρ   there exists υ ∈ Λ ≤   such that ρ ⊩ ( ⊟ υ )   and so, thanks to Oracle, we have: ⊢ F ( ⊔ υ ∈ Λ ≤ ( ⊟ υ ) )   .
    • 5. Hence, a fortiori, we obtain: ⊢ F ( ( ⊔ γ ∈ Λ c ( ⊟ γ ) ) ⊔ ( ⊔ υ ∈ Λ ≤ ( ⊟ υ ) ) ) .  
    • 6. That is, since
      ( ( ⊔ γ ∈ Λ c ( ⊟ γ ) ) ⊔ ( ⊔ υ ∈ Λ ≤ ( ⊟ υ ) ) ) ≡ ( ⊟ ( ( ⊓ γ ∈ Λ c γ ) ⊓ ( ⊓ υ ∈ Λ ≤ υ ) ) )
      = ( ⊟ ( ( γ n ∙ ) c ⊓ ( γ n ∙ ) ≤ ) )
      = ( ⊟ γ n ∙ )
      ≡ ( ⊟ γ n ) ,
      we can conclude ⊢ F ( ⊟ γ n )   , contradicting the F   -consistency of γ n   .
  • b) Or the system has at least one solution and then we can build the envisaged F   -factorizable w = ( V , S , | ψ 〉 , ν )   and ρ   from any of the solutions in the following way:
    • ∙ V   is as described above.
    • ∙ S   is as described above.
    • ∙ | ψ 〉 = { | ψ 〉 [ R ] } R ∈ ∪ S   is obtained as follows:
      • – | ψ 〉 [ G ] ( v A G )   is the solution value of z | ⊤ 〉 G A   for every G ∈ S F   (note that | ψ 〉 [ G ]   is non-factorizable by construction of S F   );
      • – | ψ 〉 [ q B \ F ]   is any non-factorizable unit vector in ℋ ( 2 [ q B \ F ] q B )   such that 〈 v | ψ 〉 [ q B \ F ] = 0   for every v ∉ V [ q B \ F ]   ;
      • – | ψ 〉 [ ∅ ] = e i 0   and | ψ 〉 [ R ] = ⊗ S ∈ S S ⊆ R | ψ 〉 [ S ]   for each non empty R ∈ ∪ S   .
    • ∙ ν = { ν G A } G ⊂ fin q B , A ⊆ G   is chosen as follows:
      • – If z | ⊤ 〉 G A   is a variable of the system then ν G A   takes the value of this variable in the adopted solution.
      • – Otherwise: If G ∈ S F   then ν G A = 〈 v A G | ψ 〉 [ G ]   ; otherwise, the value of ν G A   can be chosen freely in C   .
    • ∙ ρ   is established as follows:
      • – ρ ( x )   is equal to the value of x   if this variable occurs in the system, and given an arbitrary value otherwise;
      • – ρ ( z )   is equal to the value of z   if this variable occurs in the system, and given an arbitrary value otherwise.
    Such a pair w ρ   satisfies ( γ n ∙ ) ≤   and, so, also satisfies ( ⊓ Q D )   . QED

6 Concluding remarks

Using a non trivial extension of the Fagin-Halpern-Megiddo technique together with three Henkin like completions we were able to prove the finitely bounded weak completeness of the proposed finitary axiomatization for EQPL. The arithmetical oracle was used once for obtaining a contradiction in the case where the induced system of (in)equations has no solution.
The adoption of an arithmetical oracle for abstracting away the reasoning about real and complex numbers allowed us to concentrate on the quantum aspects of the calculus. Since the set of valid arithmetical formulae is not recursively enumerable there is no hope to find a recursive axiomatization while preserving weak completeness over the proposed semantics. But, it is viable and possible interesting to relax the semantics and replace the oracle with a recursive axiomatization of the algebraic closed fields. Parallel developments in probabilistic logic [11, 1] , give us hope of obtaining even decidable calculi. But, then, we have to pay the price of working with relaxed quantum structures that are far away from their roots in the postulates of quantum mechanics. Nevertheless, this seems to be the solution towards model checking techniques for EQPL and its dynamical extensions. Such model checking techniques also require the development of the theory of quantum automata [16] .
The weak completeness result obtained in this paper shows that the proposed language of EQPL is appropriate for the proposed exogenous semantics. Therefore, EQPL constitutes a sound basis for further developments of our approach to quantum reasoning, namely towards dynamical extensions for reasoning about the evolution of quantum systems and protocols. For preliminary results in this direction, see [18] where DEQPL (a dynamical extension of EQPL) is outlined. Recent work on dynamical versions of traditional quantum logic [4] should also be taken into account. Another interesting development, also from the applications point of view, will be directed at a EQFOL (a FOL version of exogenous quantum logic).
The detailed analysis of the weak completeness proof reinforces the idea (already present in the choice of the EQPL abbreviations) of the key role, when using EQPL for reasoning, of a finite context of qubit symbols. One wonders if this assumption can be relaxed to any recursive set of qubits by starting with classical ω   -infinitary propositional logic [14] . At least from a theoretical point of view, this line of work should be explored.
As we saw, the semantics of EQPL is based on pure quantum states of collections of qubits. Recall that pure quantum states are unit vectors of the underlying Hilbert space. In consequence, EQPL provides the means for asserting properties of and reason about such vectors. Therefore, EQPL is not insensitive to the global phase of the quantum state. One may argue that it should be insensitive since no physical measurement will ever be able to distinguish two quantum states that are equivalent up to global phase.
We decided to make EQPL as it is (that is, sensitive to global phase) for two reasons. In practice, physicists and quantum computer scientists need to work with both levels of abstraction. Sometimes they want to work with states as unit vectors. Sometimes they want to abstract away the global phase. Therefore, a calculus supporting the former level of abstraction is also useful. The second reason is a consequence of the fact that forgetting global phase requires a major semantic shift. Indeed, it is better solved by identifying a quantum state, not with a unit vector of the underlying Hilbert space, but, instead, with a density operator working on that space, that is, working with ensembles or mixed quantum states in general.
Such shift towards a semantics based on density operators will lead to a quite different quantum logic (but still extending classical logic by applying the exogenous approach) that will also be useful for reasoning about quantum systems evolving under partial tracing, besides unitary transformations and measurements. Clearly, this is yet another line of research that will deserve attention.
Finally, the relationship between the exogenous quantum logics and the more traditional quantum logics (based on the original Birkhoff and von Neumann proposal) should be explored. At the preliminary stage of work in this direction, it seems that most of the qualitative assertions possible in the latter can be made in the former and that most of the quantitative assertions possible in the former can be borrowed by extensions of the latter.
Acknowledgments The authors wish to express their deep gratitude to the regular participants in the QCI Seminar at CLC, specially Ana Maria Martins and Vítor Rocha Vieira, who attended early presentations of EQPL and gave very useful feedback that helped us to get over our initial difficulties in and misunderstandings of quantum physics. This work was partially supported by FCT and FEDER through POCTI, namely via QuantLog POCTI/MAT/55796/2004 Project. References

  1. M. Abadi and J. Y. Halpern. Decidability and expressiveness for first-order logics of probability. Information and Computation, 112(1):1–36, 1994.
  2. F. Bacchus. On probability distributions over possible worlds. In Uncertainty in Artificial Intelligence, 4, volume 9 of Machine Intelligence and Pattern Recognition, pages 217–226. North-Holland, 1990.
  3. F. Bacchus. Representing and Reasoning with Probabilistic Knowledge. MIT Press Series in Artificial Intelligence. MIT Press, 1990.
  4. A. Baltag and S. Smets. The logic of quantum programs. In P. Selinger, editor, Proceeding of the 2nd Workshop on Quantum Programming Languages, pages 39–56. Turku Centre for Computer Science, 2004.
  5. G. Birkhoff and J. von Neumann. The logic of quantum mechanics. Annals of Mathematics, 37(4):823–843, 1936.
  6. W. A. Carnielli. Possible-translations semantics for paraconsistent logics. In Frontiers of Paraconsistent Logic (Ghent, 1997), volume 8 of Studies in Logic and Computation, pages 149–163. Research Studies Press, 2000.
  7. W. A. Carnielli and M. Lima-Marques. Society semantics and multiple-valued logics. In Advances in Contemporary Logic and Computer Science (Salvador, 1996), volume 235 of Contemporary Mathematics, pages 33–52. AMS, 1999.
  8. M. L. D. Chiara, R. Giuntini, and R. Greechie. Reasoning in Quantum Theory. Kluwer Academic Publishers, 2004.
  9. C. Cohen-Tannoudji, B. Diu, and F. Laloë. Quantum Mechanics. John Wiley, 1977.
  10. H. Dishkant. Semantics of the minimal logic of quantum mechanics. Studia Logica, 30:23–32, 1972.
  11. R. Fagin, J. Y. Halpern, and N. Megiddo. A logic for reasoning about probabilities. Information and Computation, 87(1-2):78–128, 1990.
  12. D. J. Foulis. A half-century of quantum logic. What have we learned? In Quantum Structures and the Nature of Reality, volume 7 of Einstein Meets Magritte, pages 1–36. Kluwer Acad. Publ., 1999.
  13. L. Henkin. Completeness in the theory of types. Journal of Symbolic Logic, 15:81–91, 1950.
  14. C. Karp. Languages with Expressions of Infinite Length. North-Holland, 1964.
  15. S. A. Kripke. Semantical analysis of modal logic. I. Normal modal propositional calculi. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 9:67–96, 1963.
  16. A. M. Martins, P. Mateus, and A. Sernadas. Minimization of quantum automata. Preprint, CLC, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2005. Submitted for publication.
  17. P. Mateus and A. Sernadas. Exogenous quantum logic. In W. A. Carnielli, F. M. Dionísio, and P. Mateus, editors, Proceedings of CombLog'04, Workshop on Combination of Logics: Theory and Applications, pages 141–149, 1049-001 Lisboa, Portugal, 2004. Departamento de Matemática, Instituto Superior Técnico. Extended abstract.
  18. P. Mateus and A. Sernadas. Reasoning about quantum systems. In J. Alferes and J. Leite, editors, Logics in Artificial Intelligence, Ninth European Conference, JELIA'04, volume 3229 of Lecture Notes in Artificial Intelligence, pages 239–251. Springer-Verlag, 2004.
  19. P. Mateus, A. Sernadas, and C. Sernadas. Exogenous semantics approach to enriching logics. Preprint, CLC, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2005. Submitted for publication.
  20. P. Naur. Revised report on the algorithmic language Algol 60. The Computer Journal, 5:349–367, 1963.
  21. M. A. Nielsen and I. L. Chuang. Quantum Computation and Quantum Information. Cambridge University Press, 2000.
  22. N. J. Nilsson. Probabilistic logic. Artificial Intelligence, 28(1):71–87, 1986.
  23. N. J. Nilsson. Probabilistic logic revisited. Artificial Intelligence, 59(1-2):39–42, 1993.
  24. R. van der Meyden and M. Patra. Knowledge in quantum systems. In M. Tennenholtz, editor, Theoretical Aspects of Rationality and Knowledge, pages 104–117. ACM, 2003.
  25. R. van der Meyden and M. Patra. A logic for probability in quantum systems. In M. Baaz and J. A. Makowsky, editors, Computer Science Logic, volume 2803 of Lecture Notes in Computer Science, pages 427–440. Springer-Verlag, 2003.