The axiomatization of Horst Wessel’s strict logical consequence relation

Abstract

In his book from 1984 Horst Wessel presents the system of strict logical consequence Fs (see also (Wessel, 1979)). The author maintained that this system axiomatized the relation |=s of strict logical consequence between formulas of Classical Propositional Calculi (CPC). Let |= be the classical consequence relation in CPC. The relation |=s is defined as follows: \phi |=s \psi iff \phi |= \psi, every variable from \psi occurs in \phi and neither \phi is a contradiction nor \psi is a tautology. Clearly, if \phi |=s \psi, then neither \phi is a tautology nor \psi is a contradiction.

Intuitions connected with the relation |=s were presented in (Wessel, 1984). The analysis of the relation |=s is also carried out in (Pietruszczak, 2004). In the present paper we will show that the system Fs is not a complete axiomatization of the relation |=s. Moreover, we will present the system VF s that is an «extension to completeness» of the Fs.