Two-dimensional correlation analysis: Difference between revisions
en>Bibcode Bot m Adding 0 arxiv eprint(s), 5 bibcode(s) and 0 doi(s). Did it miss something? Report bugs, errors, and suggestions at User talk:Bibcode Bot |
|||
| Line 1: | Line 1: | ||
'''Minimal logic''', or '''minimal calculus''', is a [[Mathematical logic|symbolic logic]] system originally developed by [[Ingebrigt Johansson]]. It is a variant of [[intuitionistic logic]] that rejects not only the [[classical logic|classical]] [[law of excluded middle]] (as intuitionistic logic does), but also the [[principle of explosion]] (ex falso quodlibet). | |||
Just like intuitionistic logic, minimal logic can be formulated in a language using →, ∧, ∨, ⊥ ([[logical implication|implication]], [[logical conjunction|conjunction]], [[logical disjunction|disjunction]] and [[falsum]]) as the basic [[logical connective|connectives]], treating ¬A as an abbreviation for (A → ⊥). In this language it is axiomatized by the positive fragment (i.e., formulas using only →, ∧, ∨) of intuitionistic logic, with no additional axioms or rules about ⊥. Thus minimal logic is a subsystem of intuitionistic logic, and it is strictly weaker as it does not derive the ex falso quodlibet principle <math>\neg A,A\vdash B</math> (however, it derives its special case <math>\neg A,A\vdash \neg B</math>). | |||
Adding the ex falso axiom <math>\neg A\to(A\to B)</math> to minimal logic results in intuitionistic logic, and adding the double negation law <math>\neg\neg A\to A</math> to minimal logic results in classical logic. | |||
Minimal logic is closely related to [[simply typed lambda calculus]] via the [[Curry-Howard isomorphism]], i.e. the [[typing derivation]]s of simply typed lambda terms are isomorphic to [[natural deduction]] proofs in minimal logic. | |||
==References== | |||
* [[Ingebrigt Johansson|Johansson, Ingebrigt]], 1936, "[http://www.numdam.org/numdam-bin/item?id=CM_1937__4__119_0 Der Minimalkalkul, ein reduzierter intuitionistischer Formalismus]." ''Compositio Mathematica'' '''4''', 119–136. | |||
{{Logic}} | |||
{{mathlogic-stub}} | |||
[[Category:Non-classical logic]] | |||
[[Category:Constructivism (mathematics)]] | |||
[[Category:Systems of formal logic]] | |||
Revision as of 18:07, 26 December 2013
Minimal logic, or minimal calculus, is a symbolic logic system originally developed by Ingebrigt Johansson. It is a variant of intuitionistic logic that rejects not only the classical law of excluded middle (as intuitionistic logic does), but also the principle of explosion (ex falso quodlibet).
Just like intuitionistic logic, minimal logic can be formulated in a language using →, ∧, ∨, ⊥ (implication, conjunction, disjunction and falsum) as the basic connectives, treating ¬A as an abbreviation for (A → ⊥). In this language it is axiomatized by the positive fragment (i.e., formulas using only →, ∧, ∨) of intuitionistic logic, with no additional axioms or rules about ⊥. Thus minimal logic is a subsystem of intuitionistic logic, and it is strictly weaker as it does not derive the ex falso quodlibet principle (however, it derives its special case ).
Adding the ex falso axiom to minimal logic results in intuitionistic logic, and adding the double negation law to minimal logic results in classical logic.
Minimal logic is closely related to simply typed lambda calculus via the Curry-Howard isomorphism, i.e. the typing derivations of simply typed lambda terms are isomorphic to natural deduction proofs in minimal logic.
References
- Johansson, Ingebrigt, 1936, "Der Minimalkalkul, ein reduzierter intuitionistischer Formalismus." Compositio Mathematica 4, 119–136.