-
120Decision methods for linearly ordered Heyting algebrasArchive for Mathematical Logic 45 (4): 411-422. 2006.The decision problem for positively quantified formulae in the theory of linearly ordered Heyting algebras is known, as a special case of work of Kreisel, to be solvable; a simple solution is here presented, inspired by related ideas in Gödel-Dummett logic
-
64Admissibility of structural rules for contraction-free systems of intuitionistic logicJournal of Symbolic Logic 65 (4): 1499-1518. 2000.We give a direct proof of admissibility of cut and contraction for the contraction-free sequent calculus G4ip for intuitionistic propositional logic and for a corresponding multi-succedent calculus: this proof extends easily in the presence of quantifiers, in contrast to other, indirect, proofs. i.e., those which use induction on sequent weight or appeal to admissibility of rules in other calculi
-
56The continuum as a formal spaceArchive for Mathematical Logic 38 (7): 423-447. 1999.A constructive definition of the continuum based on formal topology is given and its basic properties studied. A natural notion of Cauchy sequence is introduced and Cauchy completeness is proved. Other results include elementary proofs of the Baire and Cantor theorems. From a classical standpoint, formal reals are seen to be equivalent to the usual reals. Lastly, the relation of real numbers as a formal space to other approaches to constructive real numbers is determined
-
63Proof Analysis: A Contribution to Hilbert's Last ProblemCambridge University Press. 2011.This book continues from where the authors' previous book, Structural Proof Theory, ended. It presents an extension of the methods of analysis of proofs in pure logic to elementary axiomatic systems and to what is known as philosophical logic. A self-contained brief introduction to the proof theory of pure logic is included that serves both the mathematically and philosophically oriented reader. The method is built up gradually, with examples drawn from theories of order, lattice theory and elem…Read more
-
57A normalizing system of natural deduction for intuitionistic linear logicArchive for Mathematical Logic 41 (8): 789-810. 2002.The main result of this paper is a normalizing system of natural deduction for the full language of intuitionistic linear logic. No explicit weakening or contraction rules for -formulas are needed. By the systematic use of general elimination rules a correspondence between normal derivations and cut-free derivations in sequent calculus is obtained. Normalization and the subformula property for normal derivations follow through translation to sequent calculus and cut-elimination
-
20University of Azores, Ponta Delgada, Azores, Portugal June 30–July 4, 2010Bulletin of Symbolic Logic 17 (3). 2011.
-
19Cut Elimination in Sequent Calculi with Implicit Contraction, with a Conjecture on the Origin of Gentzen’s Altitude Line ConstructionIn Peter Schuster & Dieter Probst (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science, De Gruyter. pp. 269-290. 2016.
-
273Sequent calculus in natural deduction styleJournal of Symbolic Logic 66 (4): 1803-1816. 2001.A sequent calculus is given in which the management of weakening and contraction is organized as in natural deduction. The latter has no explicit weakening or contraction, but vacuous and multiple discharges in rules that discharge assumptions. A comparison to natural deduction is given through translation of derivations between the two systems. It is proved that if a cut formula is never principal in a derivation leading to the right premiss of cut, it is a subformula of the conclusion. Therefo…Read more
-
46For Oiva Ketonen's 85th birthdayBulletin of Symbolic Logic 4 (4): 418-435. 1998.A way is found to add axioms to sequent calculi that maintains the eliminability of cut, through the representation of axioms as rules of inference of a suitable form. By this method, the structural analysis of proofs is extended from pure logic to free-variable theories, covering all classical theories, and a wide class of constructive theories. All results are proved for systems in which also the rules of weakening and contraction can be eliminated. Applications include a system of predicate l…Read more
-
14Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic LogicJournal of Symbolic Logic 65 (4): 1499-1518. 2000.We give a direct proof of admissibility of cut and contraction for the contraction-free sequent calculus G4ip for intuitionistic propositional logic and for a corresponding multi-succedent calculus: this proof extends easily in the presence of quantifiers, in contrast to other, indirect, proofs. i.e., those which use induction on sequent weight or appeal to admissibility of rules in other calculi.
-
70Tychonoff's theorem in the framework of formal topologiesJournal of Symbolic Logic 62 (4): 1315-1332. 1997.
-
69Proofs and Countermodels in Non-Classical LogicsLogica Universalis 8 (1): 25-60. 2014.Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the correspon…Read more
-
94Cut Elimination in the Presence of AxiomsBulletin of Symbolic Logic 4 (4): 418-435. 1998.A way is found to add axioms to sequent calculi that maintains the eliminability of cut, through the representation of axioms as rules of inference of a suitable form. By this method, the structural analysis of proofs is extended from pure logic to free-variable theories, covering all classical theories, and a wide class of constructive theories. All results are proved for systems in which also the rules of weakening and contraction can be eliminated. Applications include a system of predicate l…Read more
-
17Equality in the Presence of Apartness: An Application of Structural Proof Analysis to Intuitionistic AxiomaticsPhilosophia Scientiae 61-79. 2006.The theories of apartness, equality, and n-stable equality are presented through contraction- and cut-free sequent calculi. By methods of proof analysis, a purely proof-theoretic characterization of the equality fragment of apartness is obtained.
-
44Sequent calculus proof theory of intuitionistic apartness and order relationsArchive for Mathematical Logic 38 (8): 521-547. 1999.Contraction-free sequent calculi for intuitionistic theories of apartness and order are given and cut-elimination for the calculi proved. Among the consequences of the result is the disjunction property for these theories. Through methods of proof analysis and permutation of rules, we establish conservativity of the theory of apartness over the theory of equality defined as the negation of apartness, for sequents in which all atomic formulas appear negated. The proof extends to conservativity re…Read more
-
32Glivenko sequent classes in the light of structural proof theoryArchive for Mathematical Logic 55 (3-4): 461-473. 2016.In 1968, Orevkov presented proofs of conservativity of classical over intuitionistic and minimal predicate logic with equality for seven classes of sequents, what are known as Glivenko classes. The proofs of these results, important in the literature on the constructive content of classical theories, have remained somehow cryptic. In this paper, direct proofs for more general extensions are given for each class by exploiting the structural properties of G3 sequent calculi; for five of the seven …Read more
-
57Geometrisation of first-order logicBulletin of Symbolic Logic 21 (2): 123-163. 2015.That every first-order theory has a coherent conservative extension is regarded by some as obvious, even trivial, and by others as not at all obvious, but instead remarkable and valuable; the result is in any case neither sufficiently well-known nor easily found in the literature. Various approaches to the result are presented and discussed in detail, including one inspired by a problem in the proof theory of intermediate logics that led us to the proof of the present paper. It can be seen as a …Read more
-
17Tychonoff's Theorem in the Framework of Formal TopologiesJournal of Symbolic Logic 62 (4): 1315-1332. 1997.
-
133Proof Analysis in Modal LogicJournal of Philosophical Logic 34 (5-6): 507-544. 2005.A general method for generating contraction- and cut-free sequent calculi for a large family of normal modal logics is presented. The method covers all modal logics characterized by Kripke frames determined by universal or geometric properties and it can be extended to treat also Gödel-Löb provability logic. The calculi provide direct decision methods through terminating proof search. Syntactic proofs of modal undefinability results are obtained in the form of conservativity theorems.