Defaults as restrictions on classical Hilbert-style proofs

Abstract

Since the earliest formalisation of default logic by Reiter many contributions to this appealing approach to nonmonotonic reasoning have been given. The different formalisations are here presented in a general framework that gathers the basic notions, concepts and constructions underlying default logic. Our view is to interpret defaults as special rules that impose a restriction on the juxtaposition of monotonic Hubert-style proofs of a given logicL. We propose to describe default logic as a logic where the juxtaposition of default proofs is subordinate to a restriction condition Ψ. Hence a default logic is a pair (L, Ψ) where properties of the logic Ψ, like compactness, can be interpreted through the restriction condition Ψ. Different default systems are then given a common characterization through a specific condition on the logicL. We also prove cumulativity for any default logic (L, Ψ) by slightly modifying the notion of default proof. We extend, in fact, the language ofL in a way close to that followed by Brewka in the formulation of his cumulative default system. Finally we show the existence of infinitely many intermediary default logics, depending on Ψ and called linear logics, which lie between Reiter's and Łukaszewicz' versions of default logic.