A propositional calculus formal deductive system SUBℒ with an involutive negation

Residuated fuzzy logic calculi are related to continuous t-norms which are used as truth functions for the conjunction connective, and their residua as truth function for the implication. In these logics, a negation is definable from the implication and the truth constant 0̅, namely ¬φ is φ→0̅. This negation behaves quite differently depending on the t-norm. For a nilpotent t-norm, it turns out that ¬ is an involutive negation. For t-norms without non-trivial zero divisors, ¬ is Gödel negation. In this paper, we investigate the propositional calculus formal system SUBL without non-trivial zero divisors and SUBL_~ extended an involutive negation, and their completeness are proved.