Talk:Brouwer–Heyting–Kolmogorov interpretation

Latest comment: 3 years ago by ChurchBishop

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)Reply

Yes, there seems to be some inconsistency here (section "The interpretation"):
  • The formula is defined as , so a proof of it is a function f that converts a proof of into a proof of .
  • There is no proof of (the absurdity, or bottom type (nontermination in some programming languages)).
Which would imply we can never have a proof of , since there are no functions . 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)Reply
A function exists precisely when itself is empty. ChurchBishop (talk) 03:35, 2 April 2021 (UTC)Reply