Constructive logic

Constructive mathematics is distinguished from its traditional counterpart, classical mathematics, by the strict interpretation of the phrase “there exists” as “we can construct”. In order to work constructively, we need to re-interpret not only the existential quantifier but all the logical connectives and quantifiers as instructions on how to construct a proof of the statement involving these logical expressions. (…) To summarise: to prove ¬p, we may, and normally do, assume p and derive a contradiction. To prove p, it is not enough to assume ¬p and derive a contradiction.

One aspect is that the law of excluded middle is not admitted, but it is much more than that.

Another word for it is Intuitionistic, cf martin-lofIntuitionisticTypeTheory1984

Notes mentioning this note

There are no papers linking to this note.


Here are all the notes in this garden, along with their links, visualized as a graph.

Adversarial perturbation to...Can we (and should we)...Certified compilers and proof...Constructive logicCurry Howard correspondenceDuelling banjos drama in the...Equivalence checkingExporting ocaml from imandraHalf marathon afterthoughtsHow to set up a plausible...How to make a sunrise alarm...How to make a sunrise alarm...How to make a sunrise alarm...Jupyter notebook launch...Lairg to john'o'groats bike...Marabou Imandra interfacingMarkov process modelMethodologyMonte carlo processNeural network verification ...Ocaml decoder libraryProof production for neural...Reading listType theory with agdaUbuntu housekeepingUseful imandra tipsUseful git commandsUseful vim tips and tricksUsefull miscellaneous snippetsVerifying an algorithm with...On the Dangers of Stochastic...Intuitionistic Type TheorySpinoza on ModalityAttention is All you NeedFormal Monotony Analysis...