Do you mean that there can be no automated proof-checkers which are sound and complete (and terminating)? Surely there can be useful sound checkers (which terminate)? The existence of Coq and other Dependently typed languages suggests that’s true.
Do you mean that there can be no automated proof-checkers which are sound and complete (and terminating)? Surely there can be useful sound checkers (which terminate)? The existence of Coq and other Dependently typed languages suggests that’s true.