Logical refutation systems are systems of formal derivations intended to derive the non-valid, i.e. semantically refutable, formulae of a given logical system. Even though the idea of formally deriving non-valid syllogisms goes back to Aristotle, it received almost no attention until the early-mid 20thcentury, when Lukasiewicz started promoting it actively and he and some of his students developed complete refutation systems for Aristotle’s syllogistic, classical and intuitionistic logics. Since then, it has been revisited and briefly entertained by several logicians (including myself), but pursued more systematically by just a few.

In this talk I will discuss and promote an old idea that I proposed (but did not pursue further until recently) in my 1994 paper on “Refutation Systems in Modal Logic”, viz. the idea of developing systems of deduction that combine standard deductive systems for deriving logical validities with refutations systems deriving non-validities of a given logical system.  Such combined systems of deduction can employ inference rules involving both provable and refutable premises and conclusions. Typical examples of such rules are Modus Tollens (if A -> B is a theorem (hence, valid) and B is refuted, then A is refuted) and the Disjunction property (e.g. in Intuitionistic logic) stated as an inference rule: if A v B is a theorem and A is refuted then B is a theorem.

After a general, mostly non-technical and historical, introduction to refutation systems I will define generic hybrid rules and systems of proofs and refutations.  Then I will present such a system for Natural Deduction of first-order logic and will make some comments on it deductive strength. Then I will discuss briefly an emerging hierarchy of higher-order hybrid rules and systems and will conclude with some open problems and potential applications.

This is a work in (veery sloow) progress.