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 corresponding frame class (...) is found. The method is a synthesis of a generation of calculi with internalized relational semantics, a Tait–Schütte–Takeuti style completeness proof, and procedures to finitize the countermodel construction. Finitizations for intuitionistic propositional logic are obtained through the search for a minimal derivation, through pruning of infinite branches in search trees by means of a suitable syntactic counterpart of semantic filtration, or through a proof-theoretic embedding into an appropriate provability logic. A number of examples illustrates the method, its subtleties, challenges, and present scope. (shrink)

A propositional logic has the variable sharing property if φ → ψ is a theorem only if φ and ψ share some propositional variable. In this note, I prove that positive semilattice relevance logic and its extension with an involution negation have the variable sharing property. Typical proofs of the variable sharing property rely on ad hoc, if clever, matrices. However, in this note, I exploit the properties of rather more intuitive arithmetical structures to establish the variable sharing property for (...) the systems discussed. (shrink)

I discuss a collection of problems in relevance logic. The main problems discussed are: the decidability of the positive semilattice system, decidability of the fragments of R in a restricted number of variables, and the complexity of the decision problem for the implicational fragment of R. Some related problems are discussed along the way.

The semilattice relevant logics ∪R, ∪T, ∪RW, and ∪TW are defined by semilattice models in which conjunction and disjunction are interpreted in a natural way. For each of them, there is a cut-free labelled sequent calculus with plural succedents . We prove that these systems are equivalent, with respect to provable formulas, to the restricted systems with single succedents . Moreover, using this equivalence, we give a new Hilbert-style axiomatizations for ∪R and ∪T and prove equivalence between two semantics for (...) the contractionless logics ∪RW and ∪TW. (shrink)

This paper is a study of four subscripted Gentzen systems G u R +, G u T +, G u RW + and G u TW +. [16] shows that the first three are equivalent to the semilattice relevant logics u R +, u T + and u RW + and conjectures that G u TW + is, equivalent to u TW +. Here we prove Cut Theorems for these systems, and then show that modus ponens is admissible — which (...) is not so trivial as one normally expects. Finally, we give decision procedures for the contractionless systems, G u TW + and G u RW +. (shrink)

The most common way of proving decidability in propositional modal logic is to shew that the system in question has the finite model property. This is not however the only way. Gabbay in [4] proves the decidability of many modal systems using Rabin's result in [8] on the decidability of the second-order theory of successor functions. In particular [4, pp. 258-265] he is able to prove the decidability of a system which lacks the finite model property. Gabbay's system is however (...) complete, in the sense of being characterized by a class of frames, and the question arises whether there is a decidable modal logic which is not complete. Since no incomplete modal logic has the finite model property [9, p. 33], any proof of decidability must employ some such method as Gabbay's. In this paper I use the Gabbay/Rabin technique to prove the decidability of a finitely axiomatized normal modal propositional logic which is not characterized by any class of frames. I am grateful to the referee for suggesting improvements in substance and presentation.The terminology I am using is standard in modal logic. By aframeis understood a pair 〈W, R〉 in whichWis a class (of “possible worlds”) andR⊆W2. To avoid confusion in what follows, a frame will henceforth be referred to as aKripkeframe. By contrast, ageneral frameis a pair 〈,Π〉 in whichis a Kripke frame andΠis a collection of subsets ofWclosed under the Boolean operations and satisfying the condition that ifAis inΠthen so isR−1“A. A model on a frame (of either kind) is obtained by adding a functionVwhich assigns sets of worlds to propositional variables. In the case of a general frame we require thatV(p) ∈Π. (shrink)