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