Talk:Brouwer–Heyting–Kolmogorov interpretation

How can a function convert a thing into something that does not exist(proof of absurdity)? 2.53.1.233 (talk) 03:31, 28 January 2020 (UTC)

Yes, there seems to be some inconsistency here (section "The interpretation"):

• The formula $\neg P$ is defined as $P\to \bot$, so a proof of it is a function f that converts a proof of $P$ into a proof of $\bot$.
• There is no proof of $\bot$ (the absurdity, or bottom type (nontermination in some programming languages)).

Which would imply we can never have a proof of $\neg P$, since there are no functions $f\colon X\to \varnothing$. I'm sure this is just a matter of imprecise phrasing - perhaps someone familiar with the topic could help. --Jordan Mitchell Barrett (talk) 09:13, 28 October 2020 (UTC)

A function $f\colon X\to \varnothing$ exists precisely when $X$ itself is empty. ChurchBishop (talk) 03:35, 2 April 2021 (UTC)

I've edited this to use "construction" in place of "function", which is the language used by Heyting and Troelstra (who introduced the term "BHK interpretation"). (Kolmogorov used different language, as already noted.)

"Function" could be read as synonymous with "construction" given that we are in the realm of constructivism, but certainly not as "set-theoretic function".

This is a little tricky because $P\to Q$ is a hypothetical assertion. We would like to say that $P\to Q$ means "we have a proof of $Q$ given an assumption $P$", but BHK wants to directly define "proofs" (and only "proofs"), not "proofs-from-assumptions". The result is that that hypothetical assertion gets pushed "up" into the language we use to talk about proofs. (I've added a sentence which hopefully clarifies this to more readers.) This is certainly a subtle point that has been the source of some objections (SEP has a good discussion of that). The contemporary type-theoretic solution is the one given by Gentzen: formalize the notion of hypothesis in proof. JLLong (talk) 20:59, 18 March 2025 (UTC)

Underlinked/poorly-discoverable

This is a very interesting article; I remember binging a lot of Wikipedia articles on foundations of mathematics maybe 6-7 years ago, but I never came across this, even though this seems to be a very fundamental article. Could it be added to some navboxes/sidebars to make it more visible? – Closed Limelike Curves (talk) 03:06, 13 March 2025 (UTC)