[TYPES] Meaning explanations and the invalidity of the law of excluded middle

Andrej Bauer andrej.bauer at andrej.com
Fri Oct 13 02:27:19 EDT 2017


Perhaps it helps to solve the following simpler exercise first:

Is there a term

G : (nat → nat) → nat

such that, for any closed term f : nat → nat, G f is a Gödel code of f ?

With kind regards,

Andrej


More information about the Types-list mailing list