Does there exist a formal language capable of expressing any mathematical proof without resorting to drawings or natural language sentences?

869 Views Asked by At

Practically everytime I read a theorem proof in a book, paper, slides, website, pdf, anywhere, the proof is written using natural language (e.g. sentences in English) and sometimes drawings (e.g. 2D drawings if it's a proof about Geometry, Graph Theory, etc.). Even if the author does her/his best at writing a very technical and formal proof, full of formal symbols, at one point or another they can't help but resort to natural language and/or drawings to get some point across. My question is: does there exist a formal language capable of expressing any mathematical proof without resorting to drawings or natural language sentences?

UPDATE: As @Noah Schweber suggested in the comments to his answer, I should make clear that a very important underlying reason for my interest in formal proofs has to do with the issue of confidence in natural language proofs. That is, if we are not using any formal language to prove most theorems, then how can we be so sure that we have proved anything at all? Because, what if we made some mistake at some point during our natural language reasoning? Since we don't have a full symbolic formal proof, how can we truthfully check that our proof is indeed correct? I think this is a very valid concern considering that natural languages are incredibly prone to ambiguities, which I guess most would agree is an undesirable property when we want to prove mathematical statements with crystal clear certainty.

1

There are 1 best solutions below

10
On BEST ANSWER

at one point or another they can't help it but resort to natural language and/or drawings to get some point across. My question is: does there exist a formal language capable of expressing any mathematical proof without resorting to drawings or natural language sentences?

I think you're misunderstanding the goal of the text: it's to explain the result to the reader. Proofs are presented using natural language and occasionally pictures in order to be better understood by the reader.

For what it's worth, I don't mean to imply that the desire for a fully formal proof is bad. You may be interested in$^*$ mathematical logic in general (and in particular the syntax of first-order logic and set theory); more specifically, I think both formal (= machine-verifiable) proof and automated theorem proving will be of interest to you. But it's important to keep in mind the fact that mathematical texts (tend to) seek to explain mathematics to the reader, and so - even if one has a purely formal proof in hand - need to make concessions to how humans actually learn.


As a historical note, you may be interested in the book Principia Mathematica by Russell and Whitehead. More modern sources you might be interested in reading, on the issue of certainty in mathematics (as you've clarified in your comments below), include the following:

And there are many others, found quickly by googling the relevant terms. It's a big and important problem!


$^*$I don't mean to imply that texts on mathematical logic will be written in the way you want - indeed, like other mathematical texts they're trying to explain something to the reader, so use natural language - but the subject itself has a lot to say about formal proofs as mathematical objects, and the formal languages developed and studied in mathematical logic are capable of faithfully expressing mathematical theorems and proofs.