natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In logic, the exchange rule or permutation rule states that the order of the premises is irrelevant to the validity of a deduction. Along with the weakening rule and the contraction rule, it is one of the most commonly adopted structural rules.
This rule is commonly discarded in natural language parsers, such as those built on categorial grammars or similar, such as link-grammar. This is because in most natural languages, word-order matters; the proper “deduction” or parse of a sentence depends on the order of of “premises”/words.
Exactly how this looks depends on the logic used.
…
The notion of exchange as a structural inference rule originates (under the German name Vertauschung) with:
Gerhard Gentzen, §1.2.1 in: Untersuchungen über das logische Schließen I Mathematische Zeitschrift 39 1 (1935) [doi:10.1007/BF01201353]
Gerhard Gentzen, §1.21 in: Investigations into Logical Deduction, in M. E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, Studies in Logic and the Foundations of Mathematics 55, Springer (1969) 68-131 [ISBN:978-0-444-53419-4, pdf]
On the categorical semantics:
Last revised on May 28, 2024 at 13:18:16. See the history of this page for a list of all contributions to it.