Abstract

Consider those many-valued logic models in which the truth values are a lattice that supplies interpretations for the logical connectives of conjunction and disjunction, and which has a De Morgan involution supplying an interpretation for negation. Assume that the set of designated truth values is a prime filter in the lattice. Each of these structures determines a simple many-valued logic. We show that there is a single Smullyan-style signed tableau system appropriate for all of the logics these structures determine. Differences between the logics are confined entirely to tableau branch closure rules. Completeness, soundness, and interpolation can be proved in a uniform way for all cases. Since branch closure rules have a limited number of variations, in fact all the semantic structures determine just four different logics, all well-known ones. Asymmetric logics such as strict/tolerant, ST, also share all the same tableau rules, but differ in what constitutes an initial tableau. It is also possible to capture the notion of antivalidity using the same set of tableau rules. Thus a simple set of tableau rules serves as a unifying and classifying device for a natural and simple family of many-valued logics.