Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.
Concept
Admissible rule
Résumé
In logic, a rule of inference is admissible in a formal system if the set of theorems of the system does not change when that rule is added to the existing rules of the system. In other words, every formula that can be derived using that rule is already derivable without that rule, so, in a sense, it is redundant. The concept of an admissible rule was introduced by Paul Lorenzen (1955).
Admissibility has been systematically studied only in the case of structural (i.e. substitution-closed) rules in propositional non-classical logics, which we will describe next.
Let a set of basic propositional connectives be fixed (for instance, in the case of superintuitionistic logics, or in the case of monomodal logics). Well-formed formulas are built freely using these connectives from a countably infinite set of propositional variables p0, p1, .... A substitution σ is a function from formulas to formulas that commutes with applications of the connectives, i.e.,
for every connective f, and formulas A1, ... , An. (We may also apply substitutions to sets Γ of formulas, making σΓ = {σA: A ∈ Γ}.) A Tarski-style consequence relation is a relation between sets of formulas, and formulas, such that
for all formulas A, B, and sets of formulas Γ, Δ. A consequence relation such that
for all substitutions σ is called structural. (Note that the term "structural" as used here and below is unrelated to the notion of structural rules in sequent calculi.) A structural consequence relation is called a propositional logic. A formula A is a theorem of a logic if .
For example, we identify a superintuitionistic logic L with its standard consequence relation generated by modus ponens and axioms, and we identify a normal modal logic with its global consequence relation generated by modus ponens, necessitation, and (as axioms) the theorems of the logic.
A structural inference rule (or just rule for short) is given by a pair (Γ, B), usually written as
where Γ = {A1, ... , An} is a finite set of formulas, and B is a formula. An instance of the rule is
for a substitution σ.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.