General recursion in programs (that makes termination undecidable) requires a fix-point operator of type (a -> a) -> a The logical equivalent of this is an axi

General recursion in programs (that makes termination undecidable) requires a fix-point operator of type (a -> a) -> a The logical equivalent of this is an axiom (P -> P) -> P which lets you prove anything. So non-termination in a programming language corresponds to being able to prove anything - including False - in the logic.