The Entscheidungsproblem tends to rear its ugly problem Remember NP is equivalent to second order logic with existential quantified. E.g. for any X there exis

The Entscheidungsproblem tends to rear its ugly problem Remember NP is equivalent to second order logic with existential quantified. E.g. for any X there exists a Y And that only gets you to truthy Trues, co-NP is another problem. ATP is hard, and while we get lucky with some constrained problems like type inference, which is pathological in its runtime, but decidable, Pressburger arithmetic is the highest form we know is decidable. It is a large reason CS uses science and falsification vs proofs. Gödel and the difference between Symantec and syntactic completeness is another rat hole.