User:Marc Schroeder/sandbox4

Constructive logic, refers to systems of symbolic logic that differ from classical logic by more closely mirroring the notion of constructive proof. Constructive logics do not assume the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.

There exists a variety of constructive logics, the most prominent of which is intuitionistic logic, based on L.E.J. Brouwer's intuitionism, formalized by Arend Heyting.

Other logics have also been said to be constructive, like, for instance,

• the minimal logic of Ingebrigt Johansson,
• the logics of David Nelsons.

Paraconsistent logic

Intuitionistic logic is related by duality to a paraconsistent logic known as Brazilian, anti-intuitionistic or dual-intuitionistic logic. The subsystem of intuitionistic logic with the FALSE axiom removed is known as minimal logic and some differences have been elaborated on above.

Intermediate logics

Any finite Heyting algebra that is not equivalent to a Boolean algebra defines (semantically) an intermediate logic. On the other hand, validity of formulae in pure intuitionistic logic is not tied to any individual Heyting algebra but relates to any and all Heyting algebras at the same time.

For a schema not involving negations, consider the classically valid $(A\to B)\lor (B\to A)$. Adopting this over intuitionistic logic gives the intermediate logic called Gödel-Dummett logic.

Many-valued logic

Kurt Gödel's work involving many-valued logic showed in 1932 that intuitionistic logic is not a finite-valued logic. (See the section titled Heyting algebra semantics above for an infinite-valued logic interpretation of intuitionistic logic.)

See also

• BHK interpretation
• Computability logic
• Constructive analysis
• Constructive proof
• Constructive set theory
• Curry–Howard correspondence
• Game semantics
• Harrop formula
• Heyting arithmetic
• Inhabited set
• Intermediate logics
• Intuitionistic type theory
• Kripke semantics
• Linear logic
• Paraconsistent logic
• Realizability
• Relevance theory
• Smooth infinitesimal analysis

References

• Van Atten, Mark (4 May 2022). "The Development of Intuitionistic Logic". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy.
• Brunner, A. B. M.; Carnielli, Walter (March 2005). "Anti-intuitionism and paraconsistency". Journal of Applied Logic. 3 (1): 161–184. doi:10.1016/j.jal.2004.07.016.
• Colacito, Almudena (2016). Minimal and Subminimal Logic of Negation (PDF). MSc Thesis (Afstudeerscriptie). Institute for Logic, Language and Computation.
• Heyting, Arend (1930). Die formalen Regeln der intuitionistischen Logik I, II, III. Sitzungsberichte der preussischen Akademie der Wissenschaften (in German). pp. 42–56, 57–71, 158–169. In three parts
• Huet, Gérard (May 1986). Formal Structures for Computation and Deduction. International Summer School on Logic of Programming and Calculi of Discrete Design. Archived from the original on 2014-07-14.
• Johansson, Ingebrigt (1937). "Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus". Compositio Mathematica (in German). 4: 119–136.
• Odintsov, Sergei P. (2008). Constructive Negations and Paraconsistency. Trends in Logic (TREN). Vol. 26. ISBN 9780444534057.
• Sørensen, Morten Heine B.; Urzyczyn, Paweł [in Polish] (May 1998). "Lectures on the Curry-Howard Isomorphism" (PDF).
• Troelstra, Anne Sjerp; Schwichtenberg, Helmut (2003) [1996]. Basic Proof Theory (2 ed.). Cambridge University Press. pp. XII, 417. ISBN 9780521779111.
• Wansing, Heinrich (2008). "Constructive negation, implication, and co-implication". Journal of Applied Non-Classical Logics. 18 (2–3): 341–364. doi:10.3166/jancl.18.341-364.
• Weber, Matthias; Simons, Martin; Lafontaine, Christine (1993). The Generic Development Language Deva: Presentation and Case Studies. Lecture Notes in Computer Science (LNCS). Vol. 738. Springer. p. 246. ISBN 3-540-57335-6.

External links

• "Constructive logic", Encyclopedia of Mathematics, EMS Press, 2001 [1994]

Category:Logic in computer science Category:Non-classical logic Category:Constructivism (mathematics) Category:Systems of formal logic Category:Intuitionism