[bubblyworld]

I don't think this is really a problem. The general problem of finding a proof from some axioms to some formula is undecidable (in e.g. first order logic). But that doesn't tell you anything about specific cases, in the same way that we can easily tell whether some specific program halts, like this one:

"return 1"

[shannifin]

True, I was rather pointing out that being able to parse symbolic language deterministically doesn't imply that we could then "reason" deterministically in general; the reasoning would still need to involve some level of stochasticism. Whether or not that's a problem in practice depends on specifics.