Re: [TYPES] What's a program? (Seriously)

Thomas Streicher <streicher-H0bhvm5RIPJmTlJ5tp4iNa5Fl2EJEGXphC4ANOJQIlc@public.gmane.org> Wed, 19 May 2021 16:56:06 +0200

Newsgroups	gmane.comp.science.types
Message-ID	<[email protected]>

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

> Are there interesting or commonly used logical axioms that we know for sure
> cannot have computational interpretations?


PEM (Principle of Excluded Middle) already for equality of functions
from N to N. From this you immediately get a decider for the halting
problem.

Thomas