Comment

Comment by kthielen

> if you want to claim "forall x in X, P(x) is true" then you need to exhibit a particular element of x for which P holds

I don’t mean to be pedantic (although it’s in keeping with constructivism) but in the case you describe, you don’t have to provide a particular x but rather you have to provide a function mapping all x in X to P(x). It may very well be that X is uninhabited but this is still a valid constructive proof (anything follows from nothing, after all).

If instead of “for all” you’d said “there exists”, then yes constructivism requires that you deliver the goods you’ve promised.

parent kthielen 2 years ago

Discussion

Live from the official Hacker News API

A modern reader for Hacker News · SvelteKit + Skeleton