Are there any systems of mathematics that permit such a wide range of ways to formulate ideas

... 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.

• Already second order theories are not recursively axiomatizable, meaning there is no algorithm deciding what is or is not an axiom. If you want non-recursive syntax just identify wffs with axioms. Oct 28, 2019 at 9:07
• "If you want non-recursive syntax just identify wffs with axioms." It seems strange that the negation of an axiom wouldn't be a wff. What if there is a conjecture known today whose negation will one day be accepted as an axiom? It would be strange if the conjecture were meaningless rather than false. Oct 28, 2019 at 9:26
• Offhand, I'm thinking of some fun sentences like "This statement is false," which generates annoying paradoxes while "This statement is true" is merely a tautology. Oct 28, 2019 at 22:42
• No true in ZF means true in every model of ZF and false in ZF means false in every model of ZF. This has been standard mathematical usage for quite some time. So AC is not true and not false in ZF, it is independent of the system itself. Also "Not well-formed" is completely different from "meaningless".
– user9166
Oct 29, 2019 at 5:47
• None of this is bringing your objection to Confold any closer to making sense. Your complaint implied that in second order arithmetic everything well-formed would need to be either true, false or meaningless. But there are statements independent of any formal arithmetic the same way there are specific statements independent of existing formal set theories.
– user9166
Oct 29, 2019 at 5:51