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.

Kyzylkumite, Ti2V3+O5(OH): new structure type, modularity and revised formula

The crystal structure of kyzylkumite, ideally Ti2V3+O5(OH), from the Sludyanka complex in South Baikal, Russia was solved and refined (including the hydrogen atom position) to an agreement index, R1, of 2.34 using X-ray diffraction data collected on a twinned crystal. Kyzylkumite crystallizes in space group P21/c, with a = 8.4787(1), b = 4.5624(1), c = 10.0330(1) Å, β = 93.174(1)°, V = 387.51(1) Å3 and Z = 4. Tivanite, TiV3+O3OH, and kyzylkumite have modular structures based on hexagonal close packing of oxygen, which are made up of rutile TiO2 and montroseite V3+O(OH) slices. In tivanite the rutile:montroseite ratio is 1:1, in kyzylkumite the ratio is 2:1. The montroseite module may be replaced by the isotypic paramontroseite V4+O2 module, which produces a phase with the formula Ti2V4+O6. In the metamorphic rocks of the Sludyanka complex, vanadium can be present as V4+ and V3+ within the same mineral (e.g. in batisivite, schreyerite and berdesinskiite). Kyzylkumite has a flexible composition with respect to the M4+/M3+ ratio. The relationship between kyzylkumite and a closely related Be-bearing kyzylkumite-like mineral with an orthorhombic norbergite-type structure from Byrud mine, Norway is discussed. Both minerals have similar X-ray powder diffraction patterns.