A Note on the Use of Sum in the Logic of Proofs

The Logic of Proofs~LP, introduced by Artemov, encodes the same reasoning as the modal logic~S4 using proofs explicitly present in the language. In particular, Artemov showed that three operations on proofs (application~$\cdot$, positive introspection~!, and sum~+) are sufficient to mimic provability concealed in S4~modality. While the first two operations go back to G{\"o}del, the exact role of~+ remained somewhat unclear. In particular, it was not known whether the other two operations are sufficient by themselves. We provide a positive answer to this question under a very weak restriction on the axiomatization of LP.

Canonical proof nets for classical logic

Proof nets provide abstract counterparts to sequent proofs modulo rule permutations; the idea being that if two proofs have the same underlying proof-net, they are in essence the same proof. Providing a convincing proof-net counterpart to proofs in the classical sequent calculus is thus an important step in understanding classical sequent calculus proofs. By convincing, we mean that (a) there should be a canonical function from sequent proofs to proof nets, (b) it should be possible to check the correctness of a net in polynomial time, (c) every correct net should be obtainable from a sequent calculus proof, and (d) there should be a cut-elimination procedure which preserves correctness. Previous attempts to give proof-net-like objects for propositional classical logic have failed at least one of the above conditions. In Richard McKinley (2010) [22], the author presented a calculus of proof nets (expansion nets) satisfying (a) and (b); the paper defined a sequent calculus corresponding to expansion nets but gave no explicit demonstration of (c). That sequent calculus, called LK∗ in this paper, is a novel one-sided sequent calculus with both additively and multiplicatively formulated disjunction rules. In this paper (a self-contained extended version of Richard McKinley (2010) [22]), we give a full proof of (c) for expansion nets with respect to LK∗, and in addition give a cut-elimination procedure internal to expansion nets – this makes expansion nets the first notion of proof-net for classical logic satisfying all four criteria.

Heaven's Gate nach der kognitiven Wende: Sind wir mit emotionszentrierten Ansätzen endlich im Psychotherapiehimmel angekommen?

Auswirkungen von Störungen des emotionalen Erlebens auf psychopathologische Zustände und emotionszentrierte Ansätze der Psychotherapie werden erläutert. Nach einem historischen Abriss über die Rolle von Emotionen in Theorie und Praxis der Psychotherapie werden zunächst biologische und neuromodulatorische Prozesse der Emotionsregulation beschrieben. Anschließend werden auf der Basis psychologischer Konzepte Funktionen von Emotionen und emotionale Kontrollprozesse reflektiert. Vor diesem Hintergrund werden Veränderungen emotionaler Regulationsstrategien durch Psychotherapie erörtert und Möglichkeiten der emotionalen Kompetenzsteigerung diskutiert.