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.

Seismic anisotropy in the Morcles nappe shear zone: Implications for seismic imaging of crustal scale shear zones

Microstructures and textures of calcite mylonites from the Morcles nappe large-scale shear zone in southwestern Switzerland develop principally as a function of 1) extrinsic physical parameters including temperature, stress, strain, strain rate and 2) intrinsic parameters, such as mineral composition. We collected rock samples at a single location from this shear zone, on which laboratory ultrasonic velocities, texture and microstructures were investigated and quantified. The samples had different concentration of secondary mineral phases (< 5 up to 40 vol.%). Measured seismic P wave anisotropy ranges from 6.5% for polyphase mylonites (~ 40 vol.%) to 18.4% in mylonites with < 5 vol.% secondary phases. Texture strength of calcite is the main factor governing the seismic P wave anisotropy. Measured S wave splitting is generally highest in the foliation plane, but its origin is more difficult to explain solely by calcite texture. Additional texture measurements were made on calcite mylonites with low concentration of secondary phases (≤ 10 vol.%) along the metamorphic gradient of the shear zone (15 km distance). A systematic increase in texture strength is observed moving from the frontal part of the shear zone (anchimetamorphism; 280 °C) to the higher temperature, basal part (greenschist facies; 350–400 °C). Calculated P wave velocities become increasingly anisotropic towards the high-strain part of the nappe, from an average of 5.8% in the frontal part to 13.2% in the root of the basal part. Secondary phases raise an additional complexity, and may act either to increase or decrease seismic anisotropy of shear zone mylonites. In light of our findings we reinterpret the origin of some seismically reflective layers in the Grône–Zweisimmen line in southwestern Switzerland (PNR20 Swiss National Research Program). We hypothesize that reflections originate in part from the lateral variation in textural and microstructural arrangement of calcite mylonites in shear zones.

Radiometric Method for Emissivity Retrieval in High Reflective Materials

High reflective materials in the microwave region play a very important role in the realization of antenna reflectors for a broad range of applications, including radiometry. These reflectors have a characteristic emissivity which needs to be characterized accurately in order to perform a correct radiometric calibration of the instrument. Such a characterization can be performed by using open resonators, waveguide cavities or by radiometric measurements. The latter consists of comparative radiometric observations of absorbers, reference mirrors and the sample under test, or using the cold sky radiation as a direct reference source. While the first two mentioned techniques are suitable for the characterization of metal plates and mirrors, the latter has the advantages to be also applicable to soft materials. This paper describes how, through this radiometric techniques, it is possible to characterize the emissivity of the sample relative to a reference mirror and how to characterize the absolute emissivity of the latter by performing measurements at different incident angles. The results presented in this paper are based on our investigations on emissivity of a multilayer insulation material (MLI) for space mission, at the frequencies of 22 and 90 GHz.