The dynamic proofs of defeasible logics

In view of the computational properties of defeasible logics, no Tarski logic characterizes their consequence relations. After devising minimally inconsistent interpretations of inconsistent theories and extensively studying the handling and eliminating of inconsistencies from theories - a typical defeasible reasoning form - I was able, with the help of collaborators, to generalize the approach to a unifying program for characterizing defeasible reasoning forms: inductive generalization, abduction, ..., and methods in general. The logics that delineate the consequence relations were called adaptive logics and a generic theory was developed. The generic theory covers the whole field, both with respect to definitions and with respect to theorems and their proofs. Thus there is a general proof, for all adaptive logics 'in standard format', that the dynamic proof theories are sound and complete with respect to the semantics. Moreover, a host of properties (stopperedness, non-monotonicity, subset relations between consequence sets,...) of the consequence relations were stated, studied and proven for the whole domain.

As consequence sets of defeasible reasoning forms are not semi-recursive, the proofs of adaptive logics, which explicate the reasoning, deserve careful attention. Dynamic proofs do not \emph{establish} statements by showing that they are unavoidable in view of the premises, as is the case for deductive logics, but explicate the conclusions of our present best insights in the present premises. Continuing the reasoning leads in general to improved insights and, essential in the non-monotonic case, to an extended premise set. In the end all knowledge, even mathematical knowledge, relies on defeasible reasoning - cf. improvements in mathematics and metamathematics. Examples: the distinction between definability and computability, Gödel's incompleteness theorem, Lob's theorem, the Löwenheim–Skolem theorem, etc.

It turns out that static proofs - proofs of deductive logics - are a special case of dynamic proofs, obtained by annulling the effect of new lines on pevious lines of the proof.