The purpose of the paper is to study syntactic refutation systems as a way of characterizing normal modal propositional logics. In particular it is shown that there is a decidable modal logic without the finite model property that has a simple finite refutation system.

In this paper we study symmetric inference systems (that is, pairs of inference systems) as refutation systems characterizing maximal logics with certain properties. In particular, the method is applied to paraconsistent logics, which are natural examples of such logics.

The idea of rejection of some sentences on the basis of others comes from Aristotle, as Jan Łukasiewicz states in his studies on Aristotle's syllogistic [1939, 1951], concerning rejection of the false syllogistic form and those on certain calculus of propositions. Short historical remarks on the origin and development of the notion of a rejected sentence, introduced into logic by Jan Łukasiewicz, are contained in the Introduction of this paper. This paper is to a considerable extent a summary of papers (...) which are not easily available, even to the Polish reader: (1) J. Słupecki, Funkcja Łukasiewicza (Łukasiewicz’s function), Zeszyty Naukowe Uniwersytetu Wrocławskiego, Seria B, nr 3 (1959), 33-40; (2) U. Wybraniec-Skardowska, Teoria zdań odrzuconych (Theory of Rejected Sentences), (doctoral dissertation under the supervision of Jerzy Słupecki, published as a monograph), Zeszyty Naukowe Wyższej Szkoły Pedagogicznej w Opolu, Studia i Monografie, Nr 22 (1969), 5-131; (3) G. Bryll, Kilka uzupełnień teorii zdań odrzuconych (Some supplements to the theory of rejcted sentences), Zeszyty Naukowe Wyższej Szkoły Pedagogicznej w Opolu, Studia i Mnografie, Nr 22 (1969), 153-154. The paper also contains a good number of results which have not been published yet. Chapter I contains results presented in the papers (1)-(3). It provides an extension of Alfred Tarski’s theory of deductive systems presented by him in the papers [1930]: Fundamentale Begriffe der Methodologie der deduktiven Wssenschaften, I and Über einige fundamentale Begriffe der Metamathematik. The enriched theory is marked with T. The most essential new concept in T is the function Cn-1, whose definition was given by Słupecki in (1) on the basis of the so-called Tarski’s general theory of deductive systems. It has the form: y e Cn-1X iff Ex e X (x e Cn {y}), where Cn is Tarski’s consequence operation. In accordance with the definition: A sentence y is rejected on the basis of the sentences of the set X iff at least one of sentences of X is a consequence of y (is deducible from y). The intuitive meaning of the rejection function Cn-1: on the basis of false sentences we can reject false sentences only (while by means of the consequence operation Cn on the basis of true sentences we can deduce true sentences only). The function Cn-1 is a generalization of the notion of rejected sentences which was introduced into logic by Łukasiewicz. The essential property of the rejection function Cn-1 is that it satisfies the axioms of general Tarski’s consequence Cn, so it is a consequence operation, called the rejection consequence. In addition, it is an additive and normal operation. In Chapter I, there are given notions analogous to those of the theory of deductive systems, but they are written down by means of the symbol ‘Cn-1’ and not ‘Cn’. There are established the properties of introduced notions and differences and analogies taking place between them and properties of respective notions of the theory T. There are also given generalizations of the notions of ‘decidable system’ and ‘consistent system’ used by Łukasiewicz. The short Chapter II contains axioms of the system T’ which is equivalent to the system T. The only difference between sets of primitive notions of these systems consists in the appearance of the function Cn-1 in the system T’ instead of the function Cn. This chapter reproduces the results given in (2), but they are partially simplified. (shrink)

Complete deductive systems are constructed for the non-valid (refutable) formulae and sequents of some propositional modal logics. Thus, complete syntactic characterizations in the sense of Lukasiewicz are established for these logics and, in particular, purely syntactic decision procedures for them are obtained. The paper also contains some historical remarks and a general discussion on refutation systems.