To install click the Add extension button. That's it.

The source code for the WIKI 2 extension is being checked by specialists of the Mozilla Foundation, Google, and Apple. You could also do it yourself at any point in time.

4,5
Kelly Slayton
Congratulations on this excellent venture… what a great idea!
Alexander Grigorievskiy
I use WIKI 2 every day and almost forgot how the original Wikipedia looks like.
Live Statistics
English Articles
Improved in 24 Hours
Added in 24 Hours
Languages
Recent
Show all languages
What we do. Every page goes through several hundred of perfecting techniques; in live mode. Quite the same Wikipedia. Just better.
.
Leo
Newton
Brights
Milds

Structural rule

From Wikipedia, the free encyclopedia

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

YouTube Encyclopedic

  • 1/1
    Views:
    23 206
  • Part I: Vector Arithmetic, Lec 2 | MIT Calculus Revisited: Multivariable Calculus

Transcription

Common structural rules

Three common structural rules are:

  • Weakening, where the hypotheses or conclusion of a sequence may be extended with additional members. In symbolic form weakening rules can be written as on the left of the turnstile, and on the right. Known as monotonicity of entailment in classical logic.
  • 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: and . Also known as factoring in automated theorem proving systems using resolution. Known as idempotency of entailment in classical logic.
  • Exchange, where two members on the same side of a sequent may be swapped. Symbolically: and . (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 can be considered to be multisets; and with both contraction and exchange they can be considered to be 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 page was last edited on 21 October 2023, at 06:46
Basis of this page is in Wikipedia. Text is available under the CC BY-SA 3.0 Unported License. Non-text media are available under their specified licenses. Wikipedia® is a registered trademark of the Wikimedia Foundation, Inc. WIKI 2 is an independent company and has no affiliation with Wikimedia Foundation.