Notice again that I don't think this is feasible in practice. At least not with hand-crafted FOL expressions and certainly not with existing technology.
I'm not sure what "non-leaky abstraction" means. Would formal language theory fit the bill?
https://en.m.wikipedia.org/wiki/Heterophenomenology
In this framework, utterances can be studied without taking their truth value at face value.
I mean, I don't believe that is true any more that I believe calculus, or linear algebra are the way we think. Those are just formal systems that we can use to get various results about the world- but is that how we really think inside our heads? I kind of doubt it.
I'm just talking about the expressive power of first-order predicate calculus here, not about whether it's a good model for human intelligence.
Is there any proof about an existing non-leaky abstraction between natural language and First Order Logic (or logic in general)? Afaik there is none, but I might me wrong. For example (one amongst thousands): “I don’t like you” can actually mean (and it often does) the exact opposite, and the same can be said of a simple statement like “I am ok” which also can mean the exact opposite. Natural language is a very hard problem.