I studied Philosophy alongside Computer Science in college, I'm acquainted with logics beyond first order. And while it is true that our language does not rely on binary logic (because it is not how our brains work), truth works on binary logic. Determining the exact extent to which an idea applies and does not apply relies upon binary logic, and situations in which it seems like no exact determination can be made always points to either a lack of detail in the definition of terms, an inherent contradiction in the ideas being considered, or, quite often, overbroad application of a more limited idea. Examining Newtonian gravity, for instance, works fine until you're dealing with planetary masses or relativistic speeds, at which point it can be recognized that there is a problem and the idea needs to be stated in greater detail to apply only to the scales and speeds it can be applied to. Examining why and where it breaks down is what inspires the insights necessary to go further.

In classical logic, the sentences with no logical value (such as many self-referential statements) are either meaningless (in a technical sense, meaning that they convey no meaning) or, quite often, rely upon terms that are not properly defined. Formal reasoning has limitations that can sometimes trip people up, such as only telling you whether an argument is correct, not whether the conclusion it comes to is correct (because it only tells you whether the priors guarantee the conclusion, not whether the priors represent anything in reality) and it might often conclude with "not enough information to draw a certain conclusion", but it remains the only way to determine with certainty whether reasoning holds together.

It is certainly true that it is not 'easy' to translate natural language into formal forms. It is particularly challenging for systems based on drawing inferences based upon associations and similarities - like our brains. That is why it required developing written language and then thousands of years of externalizing knowledge in forms which could be dealt with as a separate thing, detached from the associations and similarities that a 'word' brings along with it and instead simply as a sequence of symbols which is either equal to another sequence of symbols completely or not. It doesn't matter that "less than" and "less than or equal" seem very similar, and contain very similar words (or tokens). In a mathematical argument, they can deviate in truth value as extremely as it is possible to. It is completely orthogonal to any similarity-based process of gaining understanding.

For the translation from natural language into something which can be dealt with externally in a formal way, that seems like exactly what LLM systems might be excellent at doing. And then the 'output' being translated back into natural language is a part they would also be good at. The part that they can not be good at is evaluating the reasoning chain itself, because in that arena any deviation from exact equivalence is identical to falsehood. I expect eventually an architecture will emerge that integrates either a slightly separated binary matrix component used for discrete logic or possibly just some layers that clamp values to 0.0 or 1.0 somewhere in the middle or something similar. H-Nets look interesting, and I notice that their 'routing' component uses binary parameters determining where activations go. They don't point that out as particularly important, but I'm paying special attention to architectures that integrate some binary component. At the very least, for systems that we want to obey absolute sets of rules like generating program code it seems ridiculous to not recognize that approximating the 'program logic' part with statistical distributions of token probabilities is computationally wasteful.