Negation is not all that well understood even in formal settings. When PROLOG introduced negation-as-failure, many logicians (Girard) were repulsed: how can fa

Negation is not all that well understood even in formal settings. When PROLOG introduced negation-as-failure, many logicians (Girard) were repulsed: how can failure to find a proof for a proposition P be considered a proof of the negation (not P)? Yet there are theories where this just "works" because P is about some inherently finite set of observations (not (John Doe is an employee)) is very much the failure of finding a record after consulting the employee database. The different treatment of negation in intuitionistic logic and classical logic is another example. Intuitionistic logic is more precise than classical: a statement of classical logic logic can be translated into one of intuitionistic logic (eg Gödel-Gentzen) that is provable if and only if the original statement was provable. Things like identity, equality, negation in real life reasoning seem to often be "good enough"/ fuzzy rather than rigorous applications of logic.