Alex, There are two very different issues: (1) Syntactic translation from one notation to another; (2) Semantic interpretation of the source or target notations. For a formally defined notation, such as FOL or any notation that is defined by its mapping to FOL, there is a single very precise definition of its meaning. For a natural language, almost every word has a continuous range of meanings. The only words (or phrases) that have a precise meaning are technical terms from some branch of science or engineering. Examples: hydrogen, oxygen, volt, ampere, gram, meter... If you translate a sentence from a natural language to formal language, that might narrow down the meaning in the target language, But that very precise meaning may be very differentt from what the original author had intended. Summary: Translation is not magic. It cannot make a vague sentence precise. John _______________________________________ From: "Alex Shkotin" <alex.shkotin(a)gmail.com> John, Let me clarify what I meant by "English is HOL" by example. Sentence: "I see a blue jay drinking out of the birdbath." HOL-structure: (I see ((a (blue jay)) (drinking (out of)) (the birdbath))) where "of" is an unary operator used in postfix form, applied to "out" being an argument. As a result we get "(out of)" an expression or term. But this term is itself an unary operator used in postfix form, applied to "drinking" to create a term "(drinking (out of))", being binary operator in infix form being applied to two arguments: left one: "(a (blue jay))", and right one: "(the birdbath)". As a result we have a proposition which is a right argument for another binary operator in infix form "see", which has the left argument "I". And we are talking here not about Logic, but about Language. In every syntactically correct phrase, words are combined: one word is applied to another. The result is something like molecules, but in the World of Words. How to get this structure from a chain of words? How to work with these structures to get what? Some pictures? True|false value? This is the questions 🔬 Alex