What is the difference between Formal Logic and Proofs?

Question

I'm a graduate CS major, and am reading Social Processes and Proofs of Theorems and Programs. But I can't make any sense of it. After searching for resources on YouTube and other sites, I came here in hope that someone could help me.

Asking for explaining the core argument in this paper is too much to ask, so I'll ask questions referring to the introduction:

Many people have argued that computer program- ming should strive to become more like mathematics. Maybe so, but not in the way they seem to think. The aim of program verification, an attempt to make programming more mathematics-like, is to increase dramatically one's confidence in the correct functioning of a piece of software, and the device that verifiers use to achieve this goal is a long chain of formal, deductive logic. In mathematics, the aim is to increase one's confidence in the correctness of a theorem, and it's true that one of the devices mathematicians could in theory use to achieve this goal is a long chain of formal logic. But in fact they don't. What they use is a proof, a very different animal. Nor does the proof settle the matter; contrary to what its name suggests, a proof is only one step in the direction of confidence. We believe that, in the end, it is a social process that determines whether mathematicians feel confident about a theorem-and we believe that, because no comparable social process can take place among program verifiers, program verification is bound to fail. We can't see how it's going to be able to affect anyone's confidence about programs.

The 2 most frustrating questions I have from this excerpt are:

1. What is the difference between Formal Logic and Proof that the author is talking about? A simple example would be appreciated.
2. What does the author mean when he talks about social process?

Answer 1

The distinction the author is making is between formal proofs and informal proofs. Most of mathematics is done informally. Informal proofs are just persuasive arguments written in natural language. They are, of course, very stylized, but ultimately it's just an argument. A formal proof is written in a formal language that is in principle (and nowadays in practice) machine-checkable. And for real logics, the algorithm to check such proofs is relatively simple. It is very rare for mathematicians to produce formal proofs, but as tooling for proof assistants improves, largely driven by the needs of software engineering, it becomes more popular.

The social process referenced is presumably processes like peer review and the more amorphous reproving, alternate proofs, alternate explanations of existing proofs that happens as people study a theorem and its proofs. If a bunch of people recheck the work and don't identify any problems, then it's evidence that there aren't any problems. It's clearly not incontrovertible proof that there are no problems.

The following isn't related to your specific question. As Fabio Somenzi points out in a comment, this paper is 40 years old (published in 1979). It's hard for me to imagine someone holding the views given in the quoted introduction nowadays. The reason formal proofs aren't commonly used in software development is that it is perceived (mostly likely, correctly) as not being cost-effective. The main concern that would cause a software developer to not trust some formally verified code is specification error which is not at all helped by using a social rather than mechanical process to verify the proof. It doesn't matter if your theorem is true if your assumptions are wrong. A lot of the impetus for proof assistants (which would have been young or non-existent in 1979) is precisely because informal proofs proved inadequate for verifying software, particularly concurrent software.

Answer 2

1. After reading the paper a bit, I think the autors mean that the proof is more than just the formal logic behind it (they cite Bourbaki):

Indeed every mathematician knows that a proof has not been "understood" if one has done nothing more than verify step by step the correctness of the deductions of which it is composed and has not tried to gain a clear insight into the ideas which have led to the construction of this particular chain of deductions in preference to every other one.

I think I agree unwillingly. When I write formal proofs in Mizar (a proof checker where I do have to go into every last detail) and they become longer than a hundred lines, I feel the need to add extra commentary to give the reader an understanding how the proof works. Shorter proofs are usually self-evident. So I'm doing it myself, yes. But I disagree with the authors that using only formal logic doesn't increase the confidence.

2. If you have a proof for a theorem, but no one reads it, is the theorem really proven for the rest of the world? Mathematicians are, sadly, just humans. When Cantor originally introduced his set theory, he was often frowned upon or simply ignored by the mathematical community. A few decades later David Hilbert said

No one shall expel us from the paradise that Cantor has created.

It is still a problem today. If you prove that, e.g. P=NP, then it will take time for the community to acknowledge the existence of the proof, because from their perspective, there have been so many wrong ones, why should yours, you being an unknown mathematician, be the right one? Fat chance.

The webcomic SMBC has a nice but slightly exaggerated comic about the social process.

Answer 3

This is a huge topic.

The first point to notice is that for decades a myth, brilliantly fostered by Bill Gates, was widely accepted: that computer software is inherently buggy, because it is so complex. That is at best a half-truth (like most myths). The real reason most software is so buggy is that there are good commercial reasons for it being buggy. Getting wide acceptance for the idea that you have to continually pay for updates/upgrades/"security enhancements" etc has generated billions for the industry. Not least because it can lead to a vast network of "officially approved" consultants who endorse your software and help to make it usable.

There are plenty of examples of cases of bug-free software being produced. For example, the "temporary supervisor" (supervisor was the old term for operating system) written for the first Cambridge University computer by Peter Swinnerton-Dyer. Or software written for JPL for space missions, or much high-speed trading software written today (there are few faster ways of losing millions that writing buggy high-speed trading software).

Of course, one could - and people have - write entire books about the problems of managing large software projects. It is certainly hard. The UK government, for example, has a long string of appalling military software messes to its discredit (torpedo guidance software so bad that submarine commanders wouldn't launch them for fear of sinking themselves, Nimrod etc).

Nonetheless, it is interesting that there has been a move towards using Haskell-type languages for programs (like high-speed trading) where there is a major financial incentive to make the software bug-free.

The second point to notice is the difficulty the math world has had over the last few decades with long proofs. Few people have understood in any detail the proof of the 4-colour theorem. Even fewer have understood the proof of the list of "exceptional" finite simple groups. Then there is the notorious case of the maybe-proof of the ABC-conjecture, which conceivably could be settled next year in the program of seminars and workshops organised by Shinichi Mochizuki and his colleagues. Note also the the messy births for the proofs of the Poincare conjecture and Fermat's last theorem.

Only a tiny number of people could prove the finite simple groups result if stranded on a desert island without comms. Rather more could prove Fermat's last theorem (and would do it rather differently from Wiles/Taylor - I remember sitting next to Gerd Faltings in a seminar at the Newton Centre and bemoaning my failure to get to grips with the proof, whereupon he offered to take me through a proof in 20 minutes). A similar number could probably manage the geometrization conjecture. A much larger number would understand the basic idea behind the 4-colour theorem and could probably scrape together an algorithm to run on a computer.

But in none of these cases can anyone put together a dozen lectures to present the proof to bright teenagers. Indeed none seem yet to have made it into the undergraduate curriculum.

So what is going on? Why are these proofs widely believed?

Part of the reason is that math is a vast structure, full of interconnecting parts. People immediately found Grisha Perelman's proof plausible because of William Thurston's widely known conjecture. Similarly people immediately found the Wiles/Taylor proof plausible because of the Taniyama-Shimura conjecture.

Another reason is that the proofs were produced by mathematicians who already had a high reputation.

But it is still somewhat strange. Why, for example, are most people still unwilling to give a verdict on Mochizuki's claimed proof? He is clearly following the hallowed Grothendieck approach, with all the hallmarks of that style of maths - endless apparently trivial lemmas, most involving hard to grasp concepts, with hard-to-prove results apparently emerging unexpectedly.

You can point to the minor mistakes in Mochizuki's work as undermining confidence. But Andrew Wiles' initial proof had mistakes, some of which were arguably not minor. Or take the case of Louis de Branges and (1) the Bieberbach conjecture, (2) the Riemann zeta hypothesis. Few people believed his proof of (1) until it was debugged and validated by the Leningrad seminar. Yet almost no one pays much attention to his claimed proof of (2). Why not? Clearly, he is prone to carelessness, but the work clearly has a respectable pedigree (eg his book on entire functions).

The last case is interesting. A major problem in maths today is that the system demands regular publication. At the junior end it is completely ridiculous. Who could possibly hope to produce anything non-trivial and novel every year? Most mathematicians produce nothing in that category in a lifetime of research. Of course, Paul Erdos produced a huge number of novel and hard-to-prove results, but he was mainly working in ill-understood areas, doing "bare hands" proofs. A classic example would be the early work on graph theory, which most mathematicians dismissed as trivial until Bela Bollobas' Modern Graph Theory showed it had a respectable body of serious results and associated techniques.

But the consequence of too much teaching, too much admin, and the requirement for too much publication, is that most mathematicians find it hard to get large blocks of uninterrupted thinking time. They are reluctant to use it to attack problems that look too hard. They are even more reluctant to spend time looking at something like Mochizuki's work, which requires ploughing through thousands of pages of material which is way outside the mainstream. What could they gain - apart from the private satisfaction of having nailed down some truth. If they show the proof is hopelessly flawed, they get no credit and it is quickly forgotten. If they show the proof is correct, almost all the credit goes to the person who originally did the work, even if the "verifier" had to make/help make substantial fixes (eg how many people give Richard Taylor much credit for the proof of Fermat's last theorem).

The third point is that it is hard to think of a significant result that has been discovered or proved by a "general purpose" (computer) algorithm. There are several cases of "book proofs" unexpectedly produced by software for theorems/lemmas in Euclidean geometry. But in general nailing down a complete proof from the axioms is a massive task. A fair amount of work goes on in that area, but its fruits have been disappointing. It has usually done no more than confirm results everyone already accepted.

A classic reference on the "social aspects" of (mathematical) proof is William Thurston's 1994 "On proof and progress in mathematics" available here

Answer 4

Formal logic, and proofs in formal logic, is a game where you encode some symbols and have rules for how you manipulate them.

There is no truth in Formal logic, except how you associate the symbols you write with concepts. Now, those symbols are often designed to align really well with truth, so the two mix relatively well.

The thing is, most uses of "formalism" is very informal. When you define a "formal" model of computation, 9999 times out of 10,000 you talk about it informally. You'll elide or hand-wave some step. Partly because those steps are boring and annoying to formalize, and partly because humans are fallible.

Today we have formal proof checkers. These let you play the formal logic game with a computer-mediated umpire, who takes your proof and makes sure you aren't breaking the rules of the game.

We also have computer proof generating assistants, who can take two assertions you believe are connected and generate a formal proof (the annoying, small steps) that one proves the other, with more or less success.

This is a small corner of mathematics. Most mathematics doesn't use this. Instead of using formal proof checking programs and assistants, they instead write relatively informal proofs. Steps are skipped -- elided -- with the understanding that the reader can convince themselves of the validity of the skipped steps.

Proofs then become a matter of writing for the audience; to consume such a proof, you need to have a certain degree of "mathematical maturity" in the areas covered, or the "A follows B" obvious steps won't be obvious to the reader and everything falls apart.

Often such proofs can be turned into formal proofs, but the process is really hard and long. And sometimes there turns out to be "technical" errors in the proof that need adjusting in order to make the proof formally provable.

In that sense, the formal proofs are stronger than the informal proofs. But in another they are sometimes not.

With the informal proofs, you are often taking the medium-informal definitions involved and a medium-informal statement of the theorem and proving it in a way that is highly convincing to a subject matter expert. What more, the proof itself may contain useful insights into why the theorem is true.

In the formal proof, you are instead taking a specific formal set of terms and definitions and proving them. If those specific formal set of terms and definitions don't align with the medium-informal definitions and statement of theorem, then you can prove something different accidentally. Reliably connecting the computer-understood formal terms to the medium-informal theory and theorem can be a matter of non-trivial effort; in fact, you will probably have to prove they are the same thing, using an informal proof.

Then, the body of the computer-checked proof could be so technical and dense that the "reasoning" could be opaque to the human reader. This is a loss, as often the structure of the proof sheds light on related problems and extensions.

I'll then relate this back to computer software. A formal proof that a program is "correct" then requires that the "correctness" of the program be what the programmer wanted. Expressing that -- what the programmer wants -- is in a sense the problem of programming in the first place!

Programmers create programs that write programs for them all the time.

Every compiler is a program that takes in a "higher level description" of a problem and outputs a lower level description of the problem.

When programmers attempt to create ridiculously high level languages, like the GUI building toolkits, what is universally found is that you lose strength and performance to a huge degree.

Going from C or C++ or similar languages to a gc+bytecode language costs 2x-3x performance; going to a scripting language costs 5x to 10x. Power -- what things you can do -- is also lost (this is typically worked around by having the parts of the program that need power be written in a lower-level language, and access it from the higher level one).

Languages like Java came out of research into writing provably correct programs. Garbage collection and lack of pointer arithmetic and similar make proving properties about the language easier; in comparison, C or C++ has piles of "if the programmer does this, the language makes zero guarantees"; you can write provably correct C or C++, but you end up highly limited in what constructs you can use.

Other languages attempt to give C or C++ levels of abstraction, but add on a proof system to prove that you aren't wandering into the lands of undefined behavior. You can see this in Rust.

But, fundamentally, the entire problem of computer languages and compilers is attempting to do exactly what the formal proof programs in mathematics are doing. They are attempting to allow the author to write a higher level description and have the lower level details handled automatically by a computer.

In short, a sufficiently accurate description of a computer program is a computer program already; saying it is "correct" then becomes checking if the description is correct, which is a problem of meaning not mathematical proof.