> 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