The formula, in the old way of using it, can contain symbols in order and a mixture that does not meet the criteria of correctness (i.e. arbitrary symbols do not form a well-formed formula (WFF) and do not conform to the grammar).
Also, a sentence written in a natural language could be in such a form that it cannot be transformed to the WFF. WFF, on the other hand, always reduces to the boolean true/false values and two-valued truth tables in predicate logic.
It is possible that we can never make a parser good enough to do English sentence transformation to an informal one perfectly. Peter Norvig has the following parser made in Python to give an idea of the process: https://github.com/norvig/pytudes/blob/master/ipynb/PropositionalLogic.ipynb
So, at the end, when a sentence cannot be transformed, by automation or by human manual work, to the well-formed formula, we need to categorize it by some way not fitting to the classical propositional paradigm.
I want to examine this interface where we decide if a logical formula is correctly formed so that we can call it WFF or if a naturally written sentence is transformable to the correctly formed propositional and predicate logic formula. I assume that this logical system, or maybe it us anticipating a larger theoretical framework, would at least entail the use of one additional type? This is: to decide if the sentence is transformable to the boolean reducible format, thus if the sentence reduces to the boolean type or not.
So, my question has a few parts. On the other hand, I'd like to get a clarification what kind of theoretical framework is required to axiomate a system that has propositional and predicate logic functionality, but also can determine, if the formula or the sentence is a boolean type at all? Related to that, what is needed to determine theoretical wise if a given sentence is well-formed at all?
Does this have something to do with language parsers and syntax checking? From that perspective, how does this affect the minimum logical paradigm required?
I hope these questions intertwine in such a way that they can be handled in one answer.
For example, the following paper is discussing similar topic and introduces the logic of presuppositions and the truth-relevance concepts: https://www.researchgate.net/deref/https%3A%2F%2Fphilpapers.org%2Farchive%2FNEWMPT.pdf
Logic systems that I'm talking about are introduced in: https://www.britannica.com/topic/logic#ref1049434
Possible candidate for such logical framework might be found from this document: http://homepages.inf.ed.ac.uk/gdp/publications/Framework_Def_Log.pdf where the S4 modal logic is mentioned to have both truth and validity relations.
Also this cstheory topic may relate to my question: https://cstheory.stackexchange.com/questions/30541/logical-framework-vs-type-theory
I have added these clarifications due to request by D.W. If the former forum is better for handling my question, I hope it can be forwarded there.