Proofs and refutations getting married
In this talk I intend to discuss and promote an old idea that I proposed in my 1994 paper on “Refutation Systems in Modal Logic”, viz. the idea of developing systems of deduction that combine standard deductive systems for derivation of validities with refutations systems deriving non-validities of a given logical system. Such combined systems of deduction can employ inference rules involving both derivable and refutable premises and conclusions. Typical examples of such rules are Modus Tollens (if A -> B is a theorem 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. More examples (in modal logics) will be given in the talk, and some potential applications will be discussed.