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.

Independent variations of CH₄ emissions and isotopic composition over the past 160,000 years

During the last glacial cycle, greenhouse gas concentrations fluctuated on decadal and longer timescales. Concentrations of methane, as measured in polar ice cores, show a close connection with Northern Hemisphere temperature variability, but the contribution of the various methane sources and sinks to changes in concentration is still a matter of debate. Here we assess changes in methane cycling over the past 160,000 years by measurements of the carbon isotopic composition delta C-13 of methane in Antarctic ice cores from Dronning Maud Land and Vostok. We find that variations in the delta C-13 of methane are not generally correlated with changes in atmospheric methane concentration, but instead more closely correlated to atmospheric CO2 concentrations. We interpret this to reflect a climatic and CO2-related control on the isotopic signature of methane source material, such as ecosystem shifts in the seasonally inundated tropical wetlands that produce methane. In contrast, relatively stable delta C-13 values occurred during intervals of large changes in the atmospheric loading of methane. We suggest that most methane sources-most notably tropical wetlands-must have responded simultaneously to climate changes across these periods.