Editing Constructive logic (section)

== 1. Intuitionistic logic ==
{{main|Intuitionistic logic}}
'''Founder''': [[L. E. J. Brouwer]] (1908, philosophy){{sfn|Brouwer|1908}}{{sfn|Brouwer|1913}} formalized by [[Arend Heyting|A. Heyting]] (1930){{sfn|Heyting|1930}} and [[Andrey Kolmogorov|A. N. Kolmogorov]] (1932){{sfn|Kolmogorov|1932}}

'''Key Idea''': Truth = having a proof. One cannot assert “<math>P</math> or not <math>P</math>” unless one can prove <math>P</math> or prove <math>\neg \neg P</math>.

'''Features''':
* No [[law of excluded middle]] (<math>P \lor \neg P</math> is not generally valid).
* No [[Double negation#Elimination and introduction|double negation elimination]] (<math>\neg \neg\ P \to P</math> is not valid generally).
* [[Material conditional|Implication]] is constructive: a proof of <math>P \to Q</math> is a method turning any proof of P into a proof of Q.

'''Used in''': [[type theory]], [[Constructivism (philosophy of mathematics)|constructive mathematics]].