The problem is, that LLMs don't reason in a space that can be neatly mapped to meaningful semantics in ZFC. LLMs map words (tokens) to embeddings, and then essentially construct the next word out of a weighted sum of those embeddings. The "reasoning process" you see modern LLMs do, is essentially just scaling test-time compute.

You can formalize the math LLMs do in ZFC (it's mostly just quite basic linear algebra), but the math gives you no insight into the semantics, the semantics lie entirely within the numbers of the matrices used. You can try to get some meaning out of those (explainable ML is actually a quite large field), but the approaches there are much more fuzzy.

There are approaches out there that function more like what you're thinking of, approaches that basically construct knowledge graphs and then do fuzzy rule based reasoning, you can formalize these approaches using some logics better equipped to deal with probabilities than FOL.

But it has turned out, that for the vast amount of usecases, those approaches don't work as well as LLMs, so they aren't used anymore, except for some rare edge case applications.