Intuitionistic logic, in which the double negation law not-not-P = P fails,is dominant in categorical logic, notably in topos theory. This paper follows adifferent direction in which double negation does hold. The algebraic notionsof effect algebra/module that emerged in theoretical physics form thecornerstone. It is shown that under mild conditions on a category, its maps ofthe form X -> 1+1 carry such effect module structure, and can be used aspredicates. Predicates are identified in many different situations, and capturefor instance ordinary subsets, fuzzy predicates in a probabilistic setting,idempotents in a ring, and effects (positive elements below the unit) in aC*-algebra or Hilbert space. In quantum foundations the duality between states and effects plays animportant role. It appears here in the form of an adjunction, where we use maps1 -> X as states. For such a state s and a predicate p, the validityprobability s |= p is defined, as an abstract Born rule. It captures many formsof (Boolean or probabilistic) validity known from the literature. Measurement from quantum mechanics is formalised categorically in terms of`instruments', using Lüders rule in the quantum case. These instruments arespecial maps associated with predicates (more generally, with tests), whichperform the act of measurement and may have a side-effect that disturbs thesystem under observation. This abstract description of side-effects is one ofthe main achievements of the current approach. It is shown that in the specialcase of C*-algebras, side-effect appear exclusively in the non-commutativecase. Also, these instruments are used for test operators in a dynamic logicthat can be used for reasoning about quantum programs/protocols. The paper describes four successive assumptions, towards a categoricalaxiomatisation of quantitative logic for probabilistic and quantum systems.
展开▼