Online research in philosophy

A non-effective cut-elimination proof for modal mu-calculus has been given by G. Jäger, M. Kretz and T. Studer. Later an effective proof has been given for a subsystem M 1 with non-iterated fixpoints and positive endsequents. Using a new device we give an effective cut-elimination proof for M 1 without restriction to positive sequents.

S4C is a logic of continuous transformations of a topological space. Cut elimination for it requires new kind of rules and new kinds of reductions.

We put together several observations on constructive negation. First, Russell anticipated intuitionistic logic by clearly distinguishing propositional principles implying the law of the excluded middle from remaining valid principles. He stated what was later called Peirce’s law. This is important in connection with the method used later by Heyting for developing his axiomatization of intuitionistic logic. Second, a work by Dragalin and his students provides easy embeddings of classical arithmetic and analysis into intuitionistic negationless systems. In the last section, we (...) present in some detail a stepwise construction of negation which essentially concluded the formation of the logical base of the Russian constructivist school. Markov’s own proof of Markov’s principle (different from later proofs by Friedman and Dragalin) is described. (shrink)

We present a cut-elimination proof for simple type theory with an axiom of choice formulated in the language with an epsilon-symbol. The proof is modeled after Takahashi's proof of cut-elimination for simple type theory with extensionality. The same proof works when types are restricted, for example for second-order classical logic with an axiom of choice.

Cut reductions are defined for a Kripke-style formulation of modal logic in terms of indexed systems of sequents. A detailed proof of the normalization (cut-elimination) theorem is given. The proof is uniform for the propositional modal systems with all combinations of reflexivity, symmetry and transitivity for the accessibility relation. Some new transformations of derivations (compared to standard sequent formulations) are needed, and some additional properties are to be checked. The display formulations of the systems considered can be presented as encodings (...) of Kripke-style formulations. (shrink)

Ackermann proved termination for a special order of reductions in Hilbert's epsilon substitution method for the first order arithmetic. We establish termination for arbitrary order of reductions.

This paper presents a formulation and completeness proof of the resolution-type calculi for the first order fragment of Girard's linear logic by a general method which provides the general scheme of transforming a cutfree Gentzen-type system into a resolution type system, preserving the structure of derivations. This is a direct extension of the method introduced by Maslov for classical predicate logic. Ideas of the author and Zamov are used to avoid skolomization. Completeness of strategies is first established for the Gentzen-type (...) system, and then transferred to resolution. The propositional resolution system was implemented by T. Tammet. (shrink)

We present a survey of proof theory in the USSR beginning with the paper by Kolmogorov [1925] and ending (mostly) in 1969; the last two sections deal with work done by A. A. Markov and N. A. Shanin in the early seventies, providing a kind of effective interpretation of negative arithmetic formulas. The material is arranged in chronological order and subdivided according to topics of investigation. The exposition is more detailed when the work is little known in the West or (...) the original presentation can be improved using notions or results which appeared later. This includes such topics as Novikov's cut-elimination method (regular formulas) and Maslov's inverse method for the predicate logic. (shrink)