... that there is no algorithm for determining whether or not a given sequence of symbols is a wff ("well-formed formula"), but instead non-trivial proofs are required, so that some sequence of symbols thought to be meaningless could be discovered to be meaningful?
For natural language processing involving communication among people in the same language, with no machines sending their own messages, such a proof might have very little value.
For natural language processing, it may be more useful to have assistance in formulating questions designed to elicit answer messages that are more easily understood, with the combination of accumulated questions and corresponding answer messages eventually allowing the original sequence of symbols (that wasn't understood) to be edited and revised, to derive a message that is both clear and meaningful.