Quantum Information Logic

Origin. Coecke and others (2000s). Logic for quantum information flow. Entanglement and measurement. Categorical quantum mechanics. Types for quantum protocols.

Models. Qubits, entanglement, measurement. No-cloning, no-deleting. Teleportation protocol. Information-theoretic primitives. Type systems for quantum.

Formalism.

Quantum data types: qubit: 2-dimensional Hilbert space qubit ⊗ qubit: entangled pairs possible bit: classical measurement outcome

No-cloning theorem: ¬∃U. U|ψ⟩|0⟩ = |ψ⟩|ψ⟩ for all |ψ⟩ Cannot copy unknown quantum state.

Quantum teleportation: Alice has |ψ⟩ to send. Shared EPR pair |Φ⁺⟩ = (|00⟩ + |11⟩)/√2. Alice measures, sends 2 classical bits. Bob applies correction, gets |ψ⟩.

Types for quantum: Linear types enforce no-cloning. |ψ⟩: qubit cannot be duplicated. Classical bits can be copied.

Entanglement types: Bell states: maximally entangled. Separable: no entanglement. Type system can track entanglement.

Measurement: measure: qubit → bit Destroys superposition. |⟨0|ψ⟩|² + |⟨1|ψ⟩|² = 1

Quantum protocols: BB84 (key distribution). Superdense coding. Quantum error correction.

Symbols.

Symbol	Unicode	Name	Meaning
\|ψ⟩	—	Ket	Quantum state
⊗	U+2297	Circled times / Tensor	Composite system
⟨ψ\|φ⟩	—	Inner product	Amplitude
⟨	U+27E8	Mathematical left angle bracket	Opens a bra
⟩	U+27E9	Mathematical right angle bracket	Closes a ket
¬	U+00AC	Not	Negation in the no-cloning statement
∃	U+2203	There exists	Quantified over unitaries
Φ⁺	U+03A6, U+207A	Phi with superscript plus / Bell state	(\|00⟩ + \|11⟩)/√2, maximally entangled
ψ	U+03C8	Psi	State vector label
√	U+221A	Square root	Normalization factor
†	U+2020	Dagger	Adjoint; the involution of the categorical model
U	—	Unitary	Quantum gate
M	—	Measure	Measurement
EPR	—	Einstein–Podolsky–Rosen pair	Shared entangled resource

Metatheory. The no-go results are theorems with definite scopes. No-cloning (Wootters and Zurek 1982; Dieks 1982) rules out a unitary copying an arbitrary unknown state exactly, and no-broadcasting (Barnum, Caves, Fuchs, Jozsa, and Schumacher 1996) extends this to mixed states whenever the states to be broadcast fail to commute. No-deleting (Pati and Braunstein 2000) is the time-reverse. Holevo's bound (1973) caps the classical information extractable from n qubits at n bits, which is why superdense coding needs pre-shared entanglement to reach 2 bits per transmitted qubit. Abramsky and Coecke (2004) showed that teleportation, entanglement swapping, and dense coding are derivable in any dagger compact closed category from the cup-cap yanking equations alone, so these protocols depend on compact structure rather than on Hilbert space specifics; Selinger later proved that finite-dimensional Hilbert spaces are complete for that axiomatization, so the diagrammatic derivations lose nothing. Tsirelson's bound (1980) fixes the maximal quantum CHSH value at 2√2 against the classical 2.

Applies to. Quantum protocol design. Verification. Cryptography. Error correction. Quantum software.

Limitations. The no-go theorems are exact statements and do not forbid approximation: universal approximate cloning is possible, with optimal fidelity 5/6 for a qubit (Bužek and Hillery 1996), so a type system that reads no-cloning as linearity overstates the physical prohibition. Linear types enforce that a qubit is used once but do not track entanglement, and they cannot decide separability — the weak membership problem for the separable states is NP-hard (Gurvits 2003). The categorical layer is qualitative: dagger compact structure derives teleportation but not the Born rule, not Holevo's bound, and not Tsirelson's bound, all of which need the amplitudes the diagrams abstract away. Compact closure requires finite dimension, so continuous-variable protocols are outside the model. And there is no proof theory here in the ordinary sense: the subject supplies a semantics and a set of no-go constraints, not a consequence relation with its own completeness theorem.