Formal Reasoning [pdf](cs.ru.nl) |
Formal Reasoning [pdf](cs.ru.nl) |
I can understand why a hundred years ago explaining what formal is (in the context of formal languages) could have been difficult. You had to say that it means something whose form can be manipulated without "understanding", or by rules that pertain to form rather than meaning. But since the late 1930s explaining what formal means has become much simpler: it means mechanical. A formal language is one that can be precisely and accurately interpreted and manipulated by a machine.
When we talk about "formal proofs" we don't mean precise proofs, official proofs, or proofs written by a mathematician. We mean proofs written in a language, and following a procedure, that can be mechanically checked (and by a fairly basic algorithm).
While it is still a little colloquial, these days we can say that formal languages are those languages that can always be correctly interpreted by a computer. I think this captures the meaning of "formal" much more than saying these are "models of natural language".
A formal language is a set of finite-length sequences (called "words") of symbols from another set (called the "alphabet"). It's essentially a very crude approximation of some strings of letters in an alphabetic writing system forming words in a natural language, while other combinations are just nonsense.
For a given formal language, there don't necessarily have to be any rules governing the words of the language, though the languages used for writing formal proofs are typically more well-behaved.
While my explanation of "formal" is meant to be introductory and not entirely precise, that some problem tackled by an algorithm is undecidable does not mean that that problem isn't precisely interpretable by the computer. A Python interpreter doesn't terminate for all inputs (and therefore doesn't decide halting), yet it does interpret all of its inputs precisely.
Here's the first sentence of Godel's 1931 On formally undecidable propositions...
"The development of mathematics in the direction of greater exactness has—as is well known—led to large tracts of it becoming formalized, so that proofs can be carried out according to a few mechanical rules."
Leibniz had discussed calculating machines (and even thought about binary arithmetic being the most appropriate implementation), so the general idea probably goes back quite far
Edit: Oh, I guess by "late 1930s" you're referring to Turing's 1936 paper where he defines Turing machines, rather than actual electronic computers. Still, understanding "formal" as "mechanical" predates it.
Leibniz spoke of "automatons" and dreamt of some sort of "thoughtless" reasoning, but I don't know if he had the right building blocks to even think of mechanisation as we could since the 19th century. E.g. here's how Leibniz tries to justify the utility of formal reasoning: "Our thoughts are for the most part what I call ‘blind thoughts’. I mean that they are empty of perception and sensibility, and consist in the wholly unaided use of symbols... We often reason in words, with the object itself virtually absent from our mind."
So he definitely had the right concept - which is why formal logic is so old - but not the right language that most people would intuitively understand today.
Also i highly recommend everybody to read the great logician Alfred Tarski's classic book Introduction to Logic: And to the Methodology of Deductive Sciences to really understand "Logic" which is what Formal Reasoning is based on.
1) A series of excellent and detailed blog posts by Eugene Asahara Prolog in the LLM Era - https://eugeneasahara.com/category/prolog-in-the-llm-era/
2) Previous HN discussion Use Prolog to improve LLM's reasoning - https://news.ycombinator.com/item?id=41831735
3) User "bytebach" gives a nice example of using Prolog as an intermediate DSL in the prompt to an LLM so as to transform English declarative -> Imperative code - https://news.ycombinator.com/item?id=41549823
Prolog is quite popular and successful as a target for LLMs. And it's no accident considering Prolog was introduced to represent natural language statements in (predicate) logic.
Linguists in the Richard Montague tradition have indeed attempted to use tools like formal logic, lambda calculus, continuations, monads, modalities etc. to try and understand the semantics of natural language in a way that's both logical/formal and compositional - i.e. accounting at least partially for the "deep" syntax of natural language itself, such that a fragment can be said to have a semantics of its own and the global semantics of a broader construction arises from "composing" these narrower semantics in a reasonably straightforward way.
This is pretty much the same as trying to take the "let's translate natural language into formal logic" proof-of-concept exercises from a text like OP (or from your average logic textbook) seriously and extending them to natural language as a whole. It turns out that this is really, really hard, because natural language mixes multiple "modalities" together in what looks like a very ad-hoc way. We only barely have the tools in formal logic to try and replicate this, such as continuations, modalities and monads. (Linguists actually talk about many phenomena of this kind, talking about "modalities" is just one example that's both general enough to give a broad idea and happens to be straightforward enough on the logical side. You have quantification, intensionality, anaphora, scope, presupposition, modality proper, discourse-level inference, pragmatics, ellipsis, indexicals, speech acts, etc. etc. etc.)
And because the semantics of natural language is both so general and so hard to pin down, it doesn't seem useful to "reason" about the logical semantics of natural languages so directly. You can of course use logical/mathematical modeling to address all sorts of problems, but this doesn't occur via a verbatim "translation" from some specific language utterance.
Nonetheless, I concur that LLMs don't yet know how to translate a request stated in a prompt to a complete Lean4 interpretation. My practice so far has usually required me to first choose an existing reference file that is similar to my desired goals, and use this reference as "inspiration" for how the LLM should go about formalization.
I'd happily work with someone on a conversational theorem prover, if anyone's up for it.
I think the way forward, for the immediate future, is to feed AI agents with a mixture of (hand-written) natural language and formal blueprints, then use as many mechanized analysis methods as possible on the generated code (from unit/regression testing to static analysis, and possibly more powerful software verification procedures). Potentially feed the output of these analyses back to the agents.
If you accept some axiomatic assumptions about infinite sets (that are common in mathematics; I'm not sure exactly what the weakest required axiom is for this), then you can even believe that there are infinite languages that have no finite description at all, very much akin to the commonplace claim that there are real numbers that have no finite description at all. There are formulations of mathematics in which this is not true, but most mathematicians seemingly work in formulations in which it is true.
I even expect that we can probably prove this directly using the powerset operation and diagonalization, which doesn't require particularly strong assumptions about infinities.
Instead, what is taught is starting with truth tables for logical operators and thus students simply don't learn to think/understand. For example, almost everybody is thrown off by the "implication" logical operator (evaluates to True when the antecedent is False irrespective of the consequent). But if you use some actual domain examples then it becomes clear why it is so.
Alfred Tarski's classic book mentioned above does a good job of building up logic from the first principles and hence is a great companion to any standard textbook.
I think of Math Academy as ideal for efficiently mastering subjects at a level slightly deeper than a typical education in a shorter amount of time, and AoPS is for taking your time to go much deeper into the topics.
Doing them both is probably best, but doing one or the other would still work.
I've been searching hi and lo for the ultimate beginner resource and nothing comes close to AoPS for the exact reason you mentioned. I started with principia mathematica by bertrand russel because I thought math worked like a big tree all stemming from one trunk. Boy was that a bad move lol. I'd be reading some textbook and I have an infinite amount of why's that would block me on the most basic of things, tons of assumed knowledge. AoPS treats you like a caveman who first discovered fire, and then discovered their books, in that order.
I'll give MathAcademy a go too, I heard lots of great things.