The simple substitution property provides a systematic and easy method for proving a theorem from the additional axioms of intermediate prepositional logics. There have been known only four intermediate logics that have the additional axioms with the property. In this paper, we reformulate the many valued logics S' n defined in Gödel [3] and prove the simple substitution property for them. In our former paper [9], we proved that the sets of axioms composed of one prepositional variable do not have (...) the property except two of them. Here we provide another proof for this theorem. (shrink)

This paper studies a propositional logic which is obtained by interpreting implication as formal provability. It is also the logic of finite irreflexive Kripke Models.A Kripke Model completeness theorem is given and several completeness theorems for interpretations into Provability Logic and Peano Arithmetic.

Coming fromI andCl, i.e. from intuitionistic and classical propositional calculi with the substitution rule postulated, and using the sign to add a new connective there have been considered here: Grzegorozyk's logicGrz, the proof logicG and the proof-intuitionistic logicI set up correspondingly by the calculiFor any calculus we denote by the set of all formulae of the calculus and by the lattice of all logics that are the extensions of the logic of the calculus, i.e. sets of formulae containing the axioms (...) of and closed with respect to its rules of inference. In the logiclG the sign is decoded as follows: A = (A & A). The result of placing in the formulaA before each of its subformula is denoted byTrA. The maps are defined (in the definitions of x and the decoding of is meant), by virtue of which the diagram is constructed. (shrink)

In this paper we investigate some basic semantic and syntactic conditions characterizing the equivalence connective. In particular we define three basic classes of algebras: the class of weak equivalential algebras, the class of equivalential algebras and the class of regular equivalential algebras.Weak equivalential algebras can be used to study purely equivalential fragments of relevant logics and strict equivalential fragments of some modal logics. Equivalential algebras are suitable to study purely equivalential fragment of BCI and BCK logic. A subclass of the (...) class of regular equivalential algebras is suitable to study equivalential fragments of ukasiewicz logics. Some subvarieties of the class of regular equivalential algebras provide natural semantics for equivalential fragments of the intuitionistic prepositional logic and various intermediate logics. (shrink)

The aim of this paper is to provide a decision procedure for Dummett's logic LC, such that with any given formula will be associated either a proof in a sequent calculus equivalent to LC or a finite linear Kripke countermodel.

Dummett's logic LC quantified, Q-LC, is shown to be characterized by the extended frame Q+, ,D, where Q+ is the set of non-negative rational numbers, is the numerical relation less or equal then and D is the domain function such that for all v, w Q+, Dv and if v w, then D v . D v D w . Moreover, simple completeness proofs of extensions of Q-LC are given.

The logic RM and its basic fragments (always with implication) are considered here as entire consequence relations, rather than as sets of theorems. A new observation made here is that the disjunction of RM is definable in terms of its other positive propositional connectives, unlike that of R. The basic fragments of RM therefore fall naturally into two classes, according to whether disjunction is or is not definable. In the equivalent quasivariety semantics of these fragments, which consist of subreducts of (...) Sugihara algebras, this corresponds to a distinction between strong and weak congruence properties. The distinction is explored here. A result of Avron is used to provide a local deduction-detachment theorem for the fragments without disjunction. Together with results of Sobociski, Parks and Meyer (which concern theorems only), this leads to axiomatizations of these entire fragments — not merely their theorems. These axiomatizations then form the basis of a proof that all of the basic fragments of RM with implication are finitely axiomatized consequence relations. (shrink)