[mycall]

So basically you are arguing a Type Theory vs Set Theory problem, Foundationalism or Engineering Refinement. Since we read here of multiple use cases for LLMs in both CS divides, we can conclude an eventual convergence in these given approaches; and if not that, some formal principles should emerge of when to use what.

[Rochus]

This discussion started already in the sixties (see e.g. the 1969 publication by McCarthy and Hayes where they describe the "frame problem" as a fundamental obstacle to the attempt to model the dynamic world using First-Order Logic and monotonic reasoning). A popular attempt to "solve" this problem is the Cyc project. Monotonic logic is universally understood as a special, restricted case (a subset) of a broader non-monotonic theory.

[mycall]

I'm familiar with Cyc but never considered it a monotonic reasoning, but it definitely makes sense in retrospect. It appears Lean Machines [0] is a step head, combining both sides of the frame problem as a specific, although it likely leans towards leans (pun intended).

[0] https://github.com/lean-machines-central/lean-machines

[Rochus]

Thanks for the hint. The "LeanMachines" project literally seems to recreate Event-B constructs (contexts, machines, events, and refinement proof obligations) inside the Lean 4 proof assistant (using Lean 4 as a "host language").

[jojomodding]

Both type and set theory are formal logic, I don't see how that's what being argued. Rather that there are some things that are formal-logicy (e.g. set theory) and many other things that are not (like e.g. biology, you'll always find some weird organism breaking your assumptions).