Jump to content

Talk:Brouwer–Heyting–Kolmogorov interpretation

Page contents not supported in other languages.
From Wikipedia, the free encyclopedia

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]