All active users are invited to
vote in the Elections for the Board of Trustees of the Wikimedia Foundation.
Monotonicity of entailment
From Wikipedia
Monotonicity of entailment is a property of logical systems that states that the hypotheses of any derived fact may be freely extended with additional assumptions. In sequent calculi this property can be captured by an inference rule called weakening, or sometimes thinning, and in such systems one may say that entailment if monotone just in case the rule is admissible.
Weakening rule
To illustrate, starting from the natural deduction sequent: In mathematical logic, natural deduction is the name given to a class of foundational approaches for two key concepts in logic, propositions and proofs. ... In proof theory, a sequent is a formalized statement of provability that is frequently used when specifying calculi for deduction. ...
Cweakening allows one to conclude:
CNonmonotone logics
In most logics, weakening is either an inference rule or a metatheorem if the logic doesn't have an explicit rule. Notable exceptions are:
- Strict logic or relevant logic, where every hypothesis must be necessary for the conclusion.
- Linear logic which disallows arbitrary contraction in addition to arbitrary weakening.
- Bunched implications where weakening is restricted to additive composition.
Essentially synonymous with relevant logic, though it can be characterized proof-theoretically as ordinary logic without weakening, or linear logic with contraction See also Relevant logic Linear logic Substructural logic Proof theory ... Relevance logic, also called relevant logic, is any of a family of non-classical substructural logics that impose certain restrictions on implication. ... In mathematical logic, linear logic is a type of substructural logic that denies the structural rules of weakening and contraction. ... The word contraction when used alone, has several possible meanings in the English language. ... Bunched logic is a variety of substructural logic that, like linear logic, has classes of multiplicative and additive operators, but differs from usual proof calculi in having a tree-like context of hypotheses instead of a flat list-like structure; it is thus a calculus of deep inference. ...
See also
- Contraction
- Exchange Rule
- Substructural logic

