Abstract A terminating sequent calculus for intuitionistic propositional logic is obtained by modifying the R $\supset $ rule of the labelled sequent calculus $\mathbf {G3I}$ . This is done by adding a variant of the principle of a fortiori in the left-hand side of the premiss of the rule. In the resulting calculus, called ${\mathbf {G3I}}_{\mathbf {t}}$ , derivability of any given sequent is directly decidable by root-first proof search, without any extra device such as loop-checking. In the negative case, the failed proof search gives a finite countermodel to the sequent on a reflexive, transitive, and Noetherian Kripke frame. As a byproduct, a direct proof of faithfulness of the embedding of intuitionistic logic into Grzegorcyk logic is obtained.

The Gödel-McKinsey-Tarski embedding allows to view intuitionistic logic through the lenses of modal logic. In this work, an extension of the modal embedding to infinitary intuitionistic logic is introduced. First, a neighborhood semantics for a family of axiomatically presented infinitary modal logics is given and soundness and completeness are proved via the method of canonical models. The semantics is then exploited to obtain a labelled sequent calculus with good structural properties. Next, soundness and faithfulness of the embedding are established by transfinite induction on the height of derivations: the proof is obtained directly without resorting to non-constructive principles. Finally, the modal embedding is employed in order to relate classical, intuitionistic and modal derivability in infinitary logic extended with axioms.

Abstract The preferential conditional logic $ \mathbb{PCL} $, introduced by Burgess, and its extensions are studied. First, a natural semantics based on neighbourhood models, which generalizes Lewis’ sphere models for counterfactual logics, is proposed. Soundness and completeness of $ \mathbb{PCL} $ and its extensions with respect to this class of models are proved directly. Labelled sequent calculi for all logics of the family are then introduced. The calculi are modular and have standard proof-theoretical properties, the most important of which is admissibility of cut that entails a syntactic proof of completeness of the calculi. By adopting a general strategy, root-first proof search terminates, thereby providing a decision procedure for $ \mathbb{PCL} $ and its extensions. Finally, semantic completeness of the calculi is established: from a finite branch in a failed proof attempt it is possible to extract a finite countermodel of the root sequent. The latter result gives a constructive proof of the finite model property of all the logics considered.

Abstract Neighbourhood semantics for intuitionistic logic extended with countable conjunctions and disjunctions is introduced and shown equivalent to topological semantics, with an indirect completeness proof as payoff. The new semantics is used to obtain a labelled sequent calculus with good structural properties. In particular, admissibility of weakening and contraction, invertibility with preservation of height for each rule and cut elimination are shown. Finally, a direct Tait–Schütte–Takeuti style form of completeness via the extraction of a countermodel from a failed proof search is proved.

It is well-known that intuitionistic propositional logic Int may be faithfully embedded not just into the modal logic S4 but also into the provability logics GL and Grz of Gödel-Löb and Grzegorczyk, and also that there is a similar embedding of Grz into GL . Known proofs of these faithfulness results are short but model-theoretic and thus non-constructive. Here a labelled sequent system Grz for Grzegorczyk logic is presented and shown to be complete and therefore closed with respect to Cut . The completeness proof, being constructive, yields a constructive decision procedure, i.e. both a proof procedure for derivable sequents and a countermodel construction for underivable sequents. As an application, a constructive proof of the faithfulness of the embedding of Int into Grz and hence a constructive decision procedure for Int are obtained.

A class of axiomatic theories with arbitrary quantifier alternations is identified and a conversion to normal form is provided in terms of generalized geometric implications . The class is also characterized in terms of Glivenko classes as those first-order formulas that do not contain implications or universal quantifiers in the negative part. It is shown how the methods of proof analysis can be extended to cover such axioms by means of conversion to systems of rules . The structural properties for the resulting extensions of sequent calculus are established and a generalization of the first-order Barr theorem is shown to follow as an immediate application. The method is also applied to obtain complete labelled proof systems for logics defined through their relational semantics. In particular, the method provides analytic proof systems for all the modal logics in the Sahlqvist fragment.

A novel countermodel-producing decision procedure that applies to several multi-modal logics, both intuitionistic and classical, is presented. Based on backwards search in labeled sequent calculi, the procedure employs a novel termination condition and countermodel construction. Using the procedure, it is argued that multi-modal variants of several classical and intuitionistic logics including K, T, K4, S4 and their combinations with D are decidable and have the finite model property. At least in the intuitionistic multi-modal case, the decidability results are new. It is further shown that the countermodels produced by the procedure, starting from a set of hypotheses and no goals, characterize the atomic formulas provable from the hypotheses.

A formulation of lattice theory as a system of rules added to sequent calculus is given. The analysis of proofs for the contraction-free calculus of classical predicate logic known as G3c extends to derivations with the mathematical rules of lattice theory. It is shown that minimal derivations of quantifier-free sequents enjoy a subterm property: all terms in such derivations are terms in the endsequent. An alternative formulation of lattice theory as a system of rules in natural deduction style is given, both with explicit meet and join constructions and as a relational theory with existence axioms. A subterm property for the latter extends the standard decidable classes of quantificational formulas of pure predicate calculus to lattice theory.

The connections between formal topology and domain theory are surveyed and various types of continuous domains are represented as formal spaces through locally Stone and locally Scott formal topologies.

Abstract. 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. Therefore it is sufficient to eliminate those cuts that correspond to detour and permutation conversions in natural deduction.

Abstract We give a direct proof of admissibility of cut and contraction for the contraction-free sequent calculusG4ipfor 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.

In this paper we give a constructive proof of the pointfree version of Tychonoff's theorem within formal topology, using ideas from Coquand's proof in [7]. To deal with pointfree topology Coquand uses Johnstone's coverages. Because of the representation theorem in [3], from a mathematical viewpoint these structures are equivalent to formal topologies but there is an essential difference also. Namely, formal topologies have been developed within Martin Löf's constructive type theory (cf. [16]), which thus gives a direct way of formalizing them (cf. [4]). The most important aspect of our proof is that it is based on an inductive definition of the topological product of formal topologies. This fact allows us to transform Coquand's proof into a proof by structural induction on the last rule applied in a derivation of a cover. The inductive generation of a cover, together with a modification of the inductive property proposed by Coquand, makes it possible to formulate our proof of Tychonoff s theorem in constructive type theory. There is thus a clear difference to earlier localic proofs of Tychonoff's theorem known in the literature (cf. [9, 10, 12, 14, 27]). Indeed we not only avoid to use the axiom of choice, but reach constructiveness in a very strong sense. Namely, our proof of Tychonoff's theorem supplies an algorithm which, given a cover of the product space, computes a finite subcover, provided that there exists a similar algorithm for each component space.