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.

Multiple osteosclerotic lesions in an Iron Age skull from Switzerland (320 - 250 BC) - An unusual case

The single Hochdorf burial was found in 1887 during construction work in the Canton of Lucerne, Switzerland. It dates from between 320 and 250 BC. The calvarium, the left half of the pelvis and the left femur were preserved. The finding shows an unusual bony alteration of the skull. The aim of this study was to obtain a differential diagnosis and to examine the skull using various methods. Sex and age were determined anthropologically. Radiological examinations were performed with plain X-ray imaging and a multislice computed tomography (CT) scanner. For histological analysis, samples of the lesion were taken. The pathological processing included staining after fixation, decalcification, and paraffin embedding. Hard-cut sections were also prepared. The individual was female. The age at death was between 30 and 50 years. There is an intensely calcified bone proliferation at the right side of the os frontalis. Plain X-ray and CT imaging showed a large sclerotic lesion in the area of the right temple with a partly bulging appearance. The inner boundary of the lesion shows multi-edged irregularities. There is a diffuse thickening of the right side. In the left skull vault, there is a mix of sclerotic areas and areas which appear to be normal with a clear differentiation between tabula interna, diploë and tabula externa. Histology showed mature organised bone tissue. Radiological and histological findings favour a benign condition. Differential diagnoses comprise osteomas which may occur, for example, in the setting of hereditary adenomatous polyposis coli related to Gardner syndrome.

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.