0

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

Improve this question
17
  • 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.
    – Conifold
    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.
    – Ren Eh Daycart
    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.
    – Cort Ammon
    Oct 28, 2019 at 22:42
  • 2
    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
  • 2
    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

1 Answer 1

Reset to default
2

As a trivial solution to get things started, may I recommend the language consisting only of true statements? Determining whether any statement is part of the language is precisely as difficult as proving whether the statement is true or not. It'd be a very useful language!

Practically speaking, I believe we avoid such systems because they don't suit our needs as human beings. But we can speak of them. Indeed, the effort to create a sufficiently powerful language with this property is famously littered with theories beset upon by paradoxes. Instead we tend to build our mathematical foundations on languages which are weaker and explore ideas within them.

Improve this answer
6
  • In using the term "weaker" to describe a language, do you mean it has less expressive power than is possible? It seems that the demand for machine-checkable meaningfulness makes for automatic semantics, so that there should be no inquiry, beyond a trivial check, about whether or not a given mathematical wff is meaningful and what it means. In contrast, facing a poem originally written in a language you are learning, along with a translation into your first language, and notes explaining the translation, we have a task requiring assistance from human experts to help a student understand.
    – Ren Eh Daycart
    Oct 28, 2019 at 22:55
  • Are you familiar with the issues raised by Godel's Incompleteness Theorem? His work stymed a great deal of effort to create such languages because a particularly valuable class of them was impossible. Even in the Semantic Web, with languages like OWL, we avoid lots of very strong languages because they're troublesome to reason in. (which is why most reasoners target OWL-DL, when OWL-Full is capable of expressing more)
    – Cort Ammon
    Oct 28, 2019 at 23:11
  • "we avoid lots of very strong languages because they're troublesome to reason in" --> Could you clarify what you meant by "strong" in that context?
    – Ren Eh Daycart
    Oct 28, 2019 at 23:14
  • PA (Peano Arithmetic) is strong in the sense of seeming unlikely to allow contradictions to be derived from the premises, but weak in the sense that limited apparatus is available to attempt to formulate a straightforward translation of an argument that uses generally accepted resources from a variety of branches of mathematics.
    – Ren Eh Daycart
    Oct 28, 2019 at 23:17
  • I was avoiding the particular wording because I have a bad tendency of getting little bits of it wrong, so please double check this definition: the strong systems I was refereeing to were those which are capable of proving all true statements in arithmetic (i.e. "2+2=4") and could prove all true statements about its own semantics. That self-reference was the particularly troublesome bit.
    – Cort Ammon
    Oct 28, 2019 at 23:18

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .