Brouwer–Heyting–Kolmogorov interpretation

E459568

The Brouwer–Heyting–Kolmogorov interpretation is a foundational explanation of intuitionistic logic that interprets logical connectives and proofs in terms of explicit constructions and algorithms rather than classical truth values.

All labels observed (2)

How this entity was disambiguated

Statements (49)

Predicate Object
instanceOf constructive semantics ⓘ
proof interpretation ⓘ
semantics of intuitionistic logic ⓘ
aimsTo explain intuitionistic logic in constructive terms ⓘ
appliesTo conjunction in intuitionistic logic ⓘ
disjunction in intuitionistic logic ⓘ
existential quantification in intuitionistic logic ⓘ
implication in intuitionistic logic ⓘ
negation in intuitionistic logic ⓘ
universal quantification in intuitionistic logic ⓘ
basedOn intuitionism ⓘ
characterizes proofs as constructions ⓘ
truth as existence of a proof ⓘ
contrastsWith classical truth‑value semantics ⓘ
describes meaning of logical connectives in intuitionistic logic ⓘ
field constructive mathematics ⓘ
intuitionistic logic ⓘ
linked to: intuitionism

mathematical logic ⓘ
proof theory ⓘ
historicalContributor Andrey Kolmogorov ⓘ
linked to: Andrei Kolmogorov

Arend Heyting ⓘ
L. E. J. Brouwer ⓘ
influenced Curry–Howard correspondence ⓘ
interprets A → B as a method transforming any construction of A into a construction of B ⓘ
A ∧ B as a construction of A and a construction of B ⓘ
A ∨ B as a construction of either A or B together with a tag ⓘ
¬A as a method transforming any construction of A into a contradiction ⓘ
∀x A(x) as a method producing for each x a construction of A(x) ⓘ
∃x A(x) as a witness x together with a construction of A(x) ⓘ
motivatedBy Brouwer’s intuitionism ⓘ
namedAfter Andrey Kolmogorov ⓘ
linked to: Andrei Kolmogorov

Arend Heyting ⓘ
L. E. J. Brouwer ⓘ
provides operational meaning to intuitionistic proofs ⓘ
rejects law of excluded middle as generally valid ⓘ
relatedTo constructive type theory ⓘ
proofs‑as‑programs paradigm ⓘ
realizability interpretation ⓘ
type theory ⓘ
semanticsType intensional semantics ⓘ
proof‑theoretic semantics ⓘ
timePeriod 20th century ⓘ
usedIn foundations of constructive mathematics ⓘ
philosophy of mathematics ⓘ
theoretical computer science ⓘ
usesConcept algorithms ⓘ
explicit constructions ⓘ
realizers of proofs ⓘ
witnesses for existential statements ⓘ

How these facts were elicited

Referenced by (7)

Full triples — surface form annotated when it differs from this entity's canonical label.

Luitzen Egbertus Jan Brouwer → notableFor → Brouwer–Heyting–Kolmogorov interpretation ⓘ
Elements of Intuitionism → about → Brouwer–Heyting–Kolmogorov interpretation ⓘ
Brouwer–Heyting–Kolmogorov interpretation → relatedTo → realizability interpretation ⓘ
linked to: Brouwer–Heyting–Kolmogorov interpretation
Arend Heyting → contributedTo → Brouwer–Heyting–Kolmogorov interpretation ⓘ
intuitionism → associatedWith → Brouwer–Heyting–Kolmogorov interpretation ⓘ
Curry–Howard correspondence → relatedConcept → Brouwer–Heyting–Kolmogorov interpretation ⓘ
Martin-Löf type theory → formalizes → Brouwer–Heyting–Kolmogorov interpretation ⓘ