Talk:Brouwer–Heyting–Kolmogorov interpretation
Appearance
This article is rated Start-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | |||||||||||
|
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 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)
- A function exists precisely when itself is empty. ChurchBishop (talk) 03:35, 2 April 2021 (UTC)