World Library  
Flag as Inappropriate
Email this Article

Structural rule

Article Id: WHEBN0000697666
Reproduction Date:

Title: Structural rule  
Author: World Heritage Encyclopedia
Language: English
Subject: Linear logic, Non-classical logic, Intuitionism, Idempotency of entailment, Bunched logic
Collection: Proof Theory, Rules of Inference
Publisher: World Heritage Encyclopedia

Structural rule

In proof theory, a structural rule is an inference rule that does not refer to any logical connective, but instead operates on the judgment or sequents directly. Structural rules often mimic intended meta-theoretic properties of the logic. Logics that deny one or more of the structural rules are classified as substructural logics.

Common structural rules

Three common structural rules are:

  • Weakening, where the hypotheses or conclusion of a sequent may be extended with additional members. In symbolic form weakening rules can be written as \frac{\Gamma \vdash \Sigma}{\Gamma, A \vdash \Sigma} on the left of the turnstile, and \frac{\Gamma \vdash \Sigma}{\Gamma \vdash A, \Sigma} on the right.
  • Contraction, where two equal (or unifiable) members on the same side of a sequent may be replaced by a single member (or common instance). Symbolically: \frac{\Gamma, A, A \vdash \Sigma}{\Gamma, A \vdash \Sigma} and \frac{\Gamma \vdash A, A, \Sigma}{\Gamma \vdash A, \Sigma}. Also known as factoring in automated theorem proving systems using resolution.
  • Exchange, where two members on the same side of a sequent may be swapped. Symbolically: \frac{\Gamma_1, A, \Gamma_2, B, \Gamma_3 \vdash \Sigma}{\Gamma_1, B, \Gamma_2, A, \Gamma_3 \vdash \Sigma} and \frac{\Gamma \vdash \Sigma_1, A, \Sigma_2, B, \Sigma_3}{\Gamma \vdash \Sigma_1, B, \Sigma_2, A, \Sigma_3}. (This is also known as the permutation rule.)

A logic without any of the above structural rules would interpret the sides of a sequent as pure sequences; with exchange, they are multisets; and with both contraction and exchange they are sets.

These are not the only possible structural rules. A famous structural rule is known as cut. Considerable effort is spent by proof theorists in showing that cut rules are superfluous in various logics. More precisely, what is shown is that cut is only (in a sense) a tool for abbreviating proofs, and does not add to the theorems that can be proved. The successful 'removal' of cut rules, known as cut elimination, is directly related to the philosophy of computation as normalization (see Curry–Howard correspondence); it often gives a good indication of the complexity of deciding a given logic.

See also

This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.

Copyright © World Library Foundation. All rights reserved. eBooks from National Public Library are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.