A proof is a argument that a statement is true, where the argument is written in a formalized, very specific language. The concept of what a proof is can be confusing, so I want to make an extended analogy to computer programs and programming languages.
(I think that people who know computer programming are in a uniquely good position to understand mathematical logic.)
A proof language is a lot like a programming language. When you write JavaScript code, you have to follow the syntax of the language. If you don't follow the syntax rules, your JavaScript program is invalid and unacceptable.
JavaScript code is meant to be run. Could you imagine a version of
JavaScript where there was no console.log, or no way to access or
modify the DOM? You could still define functions, call them, loop,
create variables... But your program would have no way to interact with
the user.
What I'm gesturing at is this: JavaScript needs some built-in ways to
talk about and manipulate the "outside world." That is what
console.log and the DOM are. These access points to the "outside
world" are not "syntax" per se. For instance, console is a variable
that holds an object, and log is a method of console.
I would say that a JavaScript program would have no semantic meaning if it weren't able to access or manipulate the outside world.
I want to make a note. In the JavaScript manual, it says that when you
call console.log, that causes a string to be printed in the terminal.
But what if I release my own version of Node.js (Ned.js?) where
console.log tells your laser printer to print out a page with the
specified line?
Is a JavaScript program a Node.js program or a Ned.js program? I
would say neither! I would say that a JavaScript program is merely a
document written according to the syntactic rules of JavaScript.
Node.js or Ned.js are simply different ways of interpreting that
code. We could say that both Node.js and Ned.js are real-life
versions of a theoretical, ideal "JavaScript interpreter."
We call Node.js and Ned.js models of this theoretical system. If
the JavaScript manual says console.log shows the user a specified message, then I would say that they are both valid models.
Here I'm trying to indicate: the "meaning" of a program is not really about its syntax; the meaning comes from how you interpret a program.
Now that we've built out our programming language example, let's talk specifically about a proof language. Let's start by analyzing a single statement of mathematical logic. A statement is a lot like a "line" in a computer program. Here is one:
If x is a prime number, then either x is two or x is odd.
Let me analyze this statement syntactically:
IF(A, XOR(B, C))
Without knowing what A, B, or C is, we cannot say whether this statement
is "true or false" (I'll return to what true or false might mean).
Sometimes we can determine whether a statement is true or false simply
by looking at its syntax (IF(X, NOT(X))), but that is seldom the case.
Let's look at some parts which contain semantic content:
A := "x is a prime number"
B := "x is two"
C := "x is odd"
In my example, A, B, and C are expressed very informally. A typical
proof system would not have a pre-built way to say "prime number" or
even a more basic concept like "odd." When programming, we write for (i = 0; i < 3; i++) and not loop three times. So in a typical proof
system, instead of "prime", we'd probably have to say:
For every number y, if x mod y = 0, then x = y.
This statement is now more syntactically rigorous. It is of the form:
FOR_EVERY(y, IF(x mod y = 0, x = y))
And here I think we have gotten down to the lowest level. Statements like:
x mod y = 0
x = y
don't use any "logical" syntax. They only use "math" syntax, which is
the kind of syntax we attach semantic meaning to. If a statement like x = y is "true," then it is not because of syntax. It is because of what
properties x and y have been assumed or proven to have, and what kinds
of numbers "exist" with those properties. Specifically, if x = y, it
means that there is only one number that satisfies the properties x is
required to have, and only one number that satisfies the properties y is
required to have, and finally those numbers are the same.
Since statements like x = y can never be "true" as a matter of merely
syntax, where does their "truth" come from?
In addition to a vocabulary for expressing semantically meaningful statements, we also need some fundamental mathematical "truths." We call those axioms, and here are a few examples:
There exists a number x such that x = 0.
For every number x, there exists a number y where y = x + 1.
For every pair of numbers x and y, if x + 1 = y + 1, then x = y.
For every three numbers x, y, and z, if z = x * y, then (z - x) = x * (y - 1).
For every two numbers x and y, if x * y = 0, then x = 0 or y = 0.
...
We want there to be only a finite number of axioms; a small and limited set of core mathematical "truths." We want these truths to be more than "self-evident." We want these truths to be almost the very definition of the concepts of "number," "addition," "multiplication."
Our hope is that, from these simple definitional axioms, we can prove any statement that is true in mathematics. Of course, we will see that this isn't quite possible.
A proof is a series of steps. Each step is a proposition such as we have seen above. A step is a lot like a "line" in a computer program.
Each step must follow (we also say be implied) by zero or more preceding lines.
Zero lines? We are always allowed to "introduce" an axioms by just asserting it in the proof.
For instance, assume we had a proof system with the axioms:
Socrates is a human.
If x is a human, then x is mortal.
The first axiom seems pretty bedrock. There can't be any way to logically "prove" that Socrates is a human. That either is a fact of the world, or it is not. We could imagine an alternative world where Socrates is a dog. To ensure that we are talking about the real world, and not fantasy land, we want to include this axiom.
The second axiom seems a little gratuitous. If we wanted to talk about other species, perhaps it would be more general to have axioms like:
If x is a human, then x is a living thing.
If x is a living thing, then x is mortal.
Anyway, the truth of all these axioms is still not a matter of "logic." Again, these statements are true only because they are true of our reality, and we can conceive that they are false in other hypothetical realities. That's a reason to include them as axioms.
Here is my proof that Socrates is mortal:
Socrates is a human. (Introduction of Axiom #1)
If x is a human, then x is mortal. (Introduction of Axiom #2)
Socrates is mortal. (Application of Inference Rule, replacing x with Socrates)
My proof has three steps. The proof "proves" that "Socrates is mortal" precisely because that is the final line of the proof.
The first two lines are "introductions" of axioms. I do not need to justify these steps. They are always valid to state.
The last step is the only "innovation" in the proof. I apply a logical rule that says:
For any properties P and Q, if you have already proven the statement
Px, and the statement "If Px, then Qx", then you may conclude that
Qx is true.
This rule is traditionally called modus ponens. Here "Px" is a way of saying "The statement P is true of x." Notice that even though this is just one rule of inference, it is very versatile: it works for any kind of statements P or Q.
It's not necessary to have more than a few rules of inference. You need far fewer rules than axioms. In addition to modus ponens, you can typically get away with only one extra inference rule:
If you have proven "For all x, Px", then you are allowed to conclude
that "NOT(There exists an x such that NOT(Px))."
Here is the most important thing about proofs. A proof system is only useful if a fully defined procedure exists for checking a proof. That is: there should be a totally deterministic procedure for recognizing a proof as either valid or invalid. The procedure should require absolutely no semantic understanding of what the proof is about. The proof checking should not require insight or originality.
Put simply, the concept of a proof system requires that you be able to write a computer program that will output "CORRECT" if an input proof follows the rules, and "INCORRECT" if an input proof does not follow the rules.
That's why it's important to have a very formal syntax, and a very simple kind of inference rule. The inference rule is "syntactical." A program can pattern match to make sure the rule applies without knowing what the rule means.
Our goal with a proof system is to learn truths about our reality (or about numbers) that are not otherwise immediately obvious to us.
When designing a proof system, really our only choices are (1) the syntax of the base language (stuff like defining how to parse "x = y + 3") and (2) the axioms.
It is no problem to make up proof systems that describe alternative realities. We simply change the axioms. If we do that, of course we don't expect that things we prove of the alternative reality must always be true in our true reality. It can be fun or interesting to explore alternative realities; sometimes thinking about how alternative realities would work helps us develop a better intuition of our true reality.
The point is, even if the axioms are not true of our reality, that doesn't make the statements or conclusions of a proof system meaningless.
What I'm trying to point out is the difference between the notion of true and the notion of provable. A statement is true of a model (either real world, or some imagined alternative reality). A statement is provable in a proof system.
Alternative worlds are okay, but I suppose there is one kind of proof
system that I really don't like. If you can prove both P and NOT(P),
this is a contradiction. It is an inconsistency in our proof system.
Since there is no possible imagined alternative reality where both P
and NOT(P) could both be true, a proof system that can prove
contradictory statements truly describes nothing at all. Since an
inconsistent proof system describes nothing at all, it is uninteresting
to us. We'd only be studying it or using it as a mistake.
Another thing that could go wrong is if we chose some axioms in a way that wasn't self-contradictory, but merely not true of the real world. For instance, if we replaced "Socrates is a human" with "Socrates is a dog," this would not make our system inconsistent. The only problem would be if we didn't realize that we're now talking about an alternate reality. It's okay to explore alternate realities, so long as you realize that is what you are doing.
Basically: we don't want our proof system to prove things that are untrue of our intended model.
Of course, we must consider the last thing that can go wrong. It may be that you left out some axioms that are true of our real world, and that distinguish it from alternative realities. For instance, if you neither write "Socrates is a human" nor "Socrates is a dog," then your proof language could be interpreted as referring to our real world (where Socrates is indeed human), or an alternative world (where Socrates is a dog). Lacking these axioms, there are now things you can neither prove nor disprove ("Socrates like burying bones in the ground"). That's because any provable statement is supposed to be true in all worlds that satisfy the axioms.
You want your system to be complete: for every statement P, you want
to be able to prove either P, or NOT(P).
Here's an important point about logic. You never get something from nothing. If you are the ultra-skeptic, then logic can't help you.
We will assume that the core math syntax ("x = y + 3" type stuff) is syntactically unambiguous. That is, there can never be two ways of parsing the same core math syntax.
Why should you trust that the core syntax is unambiguous? Because even if our proof system is very expressive (for instance, can describe things like the real numbers, infinite sets of numbers, et cetera), you can use a much simpler proof system (one that can only talk about integers, and can only do a primitive form of recursion) to create a proof that the syntax parses unambiguously. Basically, you don't need to trust all of mathematics to accept a proof that the syntax of math is at least unambiguous.
We will assume soundness. That means that, if the proof system can prove a statement P, then in every reality that satisfies the axioms of the system, the statement P must be true. Note, I am presuming for the moment that there are realities, alternative or otherwise, where the axioms are all true. I'm not yet worried about problems with axioms. I'm saying you shouldn't be worried about problems with reasoning.
Why should you trust soundness? Because of the extremely limited set of inference rules. Can you imagine a scenario where modus ponens led you from truth to an untrue conclusion? If that's the kind of thing you worry about, then there is no hope for you. Proofs are not for you.
If you ask me for a logical argument to prove that syntactically valid logic arguments always result in true conclusions... What the hell? What do you want from me?
You are not allowed to worry whether the way we've formulated the axioms truly describes what we intend. You're not allowed to worry that we wrote down "Socrates is a dog" when we really should have written "Socrates is a human." This is less dumb than doubting the fundamental rules of inference (that is, doubting soundness). But there's no way for logic itself to detect if you've made this kind of mistake. Because the mistake isn't in logic.
Example: if you write a JavaScript program, you might wonder: "If I run this program, will it do what I intended?" How would JavaScript ever be able to check that? Your JavaScript program is already supposed to be the precise expression of your intent! Maybe that's too harsh: you can write Mocha or Jasmine tests to feel more confidence that your JavaScript program does what you intend. But ultimately, it is up to you to make those Mocha or Jasmine tests comprehensive. The test language (and logic) can't get inside your head and figure out what you want unless you speak precisely and accurately.
You are allowed to have doubts about whether your choice of axioms may be inconsistent. Even though we try to pick a very minimal set of axioms from which we then derive all mathematical concepts, some of those axioms are pretty unintuitive. Mathematicians have made very fundamental mistakes several times in the past. (Maybe more later.)
Note: if a system is inconsistent, this is a quality that you can
always detect through logic. It is simple. Find the statement P where
you can prove both P and NOT(P). Well, it may be very very hard for
you to know how to find P. No matter how hard you try, you're not
guaranteed to find an inconsistency, because you may simply be looking
in the wrong places. But it is an absolute fact that it is always
possible (at least in theory) to detect inconsistency through logic,
because that is exactly what it means to be inconsistent!
The incompleteness theorems will ask: can you always (ever?) prove that a set of axioms is consistent? We want to trust that if we rely on our proof system, we'll never be led astray.
Which brings us to our last worry. You may worry about whether you have not included enough axioms for your system to be complete. This feels a lot less bad than being inconsistent, since our proof system will never give us bad advice. But it is troubling to think that mathematicians might spend years and years trying to prove a statement X, not realizing that X can neither be proven nor disproven given our current set of axioms.
Here's an example of incompleteness in action.
There is a mathematical statement called the "axiom of choice." It doesn't matter what this is. For a long long time, mathematicians often made arguments that implicitly assumed that the axiom of choice was true, without realizing they were making that assumption.
Eventually, mathematicians did notice that they had often been assuming the axiom of choice was true. But were they lucky? Was the axiom of choice true all along? No harm, no foul?
To a lot of mathematicians, the axiom of choice seemed like an obviously true statement. That's probably why they had assumed it for so long. On the other hand, it didn't feel like a definitional statement. The axiom of choice is about set theory (which is where a lot of shit gets real). The axiom of choice says that you are allowed to assume certain kinds of sets exist. But the axiom of choice doesn't feel like it is saying anything that is at the heart of what a set is.
For that reason, mathematicians assumed/hoped that you could prove the axiom of choice from the existing set of axioms they were already using. The system of axioms without the axiom of choice is called ZF (for Zermelo-Frankel). Is the axiom of choice a theorem of ZF? That is, can it be proven in ZF?
Godel proved that, if you added the axiom of choice as an axiom of ZF (possibly redundantly), then this could not create a new contradiction. That is, any contradiction involving the axiom of choice could be translated into a contradiction that had already existed in simply ZF without the axiom of choice.
Note that Godel did not prove that either ZF or ZFC (ZF with the axiom of choice added to the set of axioms) is in fact consistent. Godel showed that the axiom of choice is simply consistent with the existing axioms of ZF, which themselves could be inconsistent.
Mathematicians were happy. They felt justified in assuming the axiom of choice all along. Nothing new could go wrong by assuming it. But proving the axiom of choice still seemed really hard. So, in the meantime, mathematicians did simply add the axiom of choice in. They started using ZFC as their proof system, instead of simply ZF.
In 1963, Cohen proved that NOT(axiom of choice) was also consistent
with the pre-existing axioms of ZF. Same thing (but a lot harder). He
proved that if adding NOT(axiom of choice) to ZF leads to a
contradiction, you can "translate" that contradiction back to a
contradiction that had existed before.
At this point, Godel and Cohen had collectively proved that the axiom of choice is independent of the existing axioms of ZF. That is, ZF is incomplete, and the axiom of choice is one of the "holes" where you can't prove it, but you can't prove its negation.
The brings us to a question: should we add the axiom of choice in? Is it "true?" Presuming that ZF has no contradictions, then there are "versions" of set theory where the axiom of choice is true, and versions where it is false. Both versions would satisfy all the original axioms of ZF.
Yeah, but which one is true "in the real world?" I would say: mathematics is not the real world. Mathematics is a concept, a product of the mind. Like, "infinity" is a concept in mathematics. Where is that in the real world?
Practically, mathematicians (maybe excepting logicians) just go ahead and use the axiom of choice, because it lets them prove what they want to prove.
We've started to talk about something pretty deep, and maybe it sort of snuck in. We'd previously been talking about proofs of mathematical statements (like "there are no even primes greater than two"). But all of a sudden we are talking about proofs about our proof system. For instance, a proof that the axiom of choice introduces no new contradictions into our system.
What? How can we ever do that?
Let me give an example. Can you write a JavaScript program that checks that an input JavaScript program is syntactically correct? Absolutely. This kind of program is called a parser. It's essential to any JavaScript interpreter.
In a way, we can interpret the parser JavaScript program as "proving" that the input JavaScript program is syntactically valid. But does the JavaScript program really know what it's doing? The code of the JavaScript parser says stuff like:
When you see an open parenthesis, increment a counter.
When you see a close parenthesis, decrement a counter.
At the end, if the counter isn't zero, then the input program must be invalid.
These rules make no reference to the concept of "JavaScript." The JavaScript program is just processing a string input. It doesn't know that the processing it's doing is "proving" a property about the input JavaScript program. It doesn't realize that this is a statement about the JavaScript programming language (that the input program is valid).
If the JavaScript program could think of itself as "proving" anything, it would think of itself as proving something about a string. That the input string has certain properties, for instance.
Of course, we could write a JavaScript program that executes an input
JavaScript program. We don't even need to use eval to do this. We'd
write our interpreter basically the same way as if we wrote the
JavaScript interpreter in C or Java or Python.
Sure, we'd still have to run our JavaScript interpreter program with yet another JavaScript interpreter program (maybe written in C or C++), because our CPU can't execute JavaScript code directly. But the point is that the JavaScript language has all the expressive power needed to describe exactly how to run an input JavaScript program.
Again, this ability comes directly from the ability to encode JavaScript programs as strings, and the ability of JavaScript to manipulate strings.
As a programmer, you should not be surprised that a statement about numbers can itself be translated into a number. One simple way: encode that statement in ASCII, which is a series of bytes, and then treat that big long array of bytes as one big long binary number.
Here's a maybe much more surprising part. You can devise an encoding scheme where, if a statement S is provable in ZF, then the number X that S encodes to will have a specific numeric property. That numeric property will only ever hold if the encoded statement is provable. And that numeric property can itself be expressed in the language of number theory.
Let me give a different example for a metaphor. The ASCII code for "A" is 65. Any string I encode using ASCII will have a 65 in its first byte if and only if the string starts with the letter "A." Thus, it is a numeric property of ASCII encoded strings, that if I do a specific series of simple numeric operations I will end up with the number 65 if and only if the string I encoded started with the letter "A."
Godel found a way to encode proofs in such a way that the proof was a valid proof if and only if the number had a certain numeric property. There was also a way to "extract" the last line (the conclusion) of the proof from its number.
Consider any statement S of number theory. Encode S to the number X. We can now write:
There exists a number Y such that
(1) Y satisfies the numeric properties of a validly encoded proof,
(2) when you apply the numerical process to "extract" the
"conclusion number" Z from Y,
(3) Z is equal to the number X.
Call this statement S2. S2, a statement in number theory, can be interpreted as a statement about what can be proven in number theory. The "higher-level" interpretation of S2 is: "S can be proven." That is, if S2 can be proven, then the number Y that S2 says exists can be decoded as a proof of the original statement S.
If S2 cannot be proven, then the system cannot prove S. In that case,
either (1) NOT(S) can be proven, or (2) our proof system is
incomplete.
This is a very important point. We do not need a "meta-system" to talk about the consistency or incompleteness of a proof system. If the proof system can talk about integers and basic concepts like addition and multiplication, then the proof system can make statements that can be interpreted as being statements about itself.
It doesn't matter at all whether the proof system was ever designed to have this capacity; it is inescapable. It doesn't matter if anyone ever thinks to interpret these number theory statements as meta-statements about number theory. It's still the case that if the statement is true under one interpretation, it is also true under the other interpretation.
I'll return to programming. If I write a JavaScript program that checks whether the first letter of a string is the letter "A", then what the JavaScript program is doing can be described as a series of numerical operations. It has to be, because the CPU can really only do operations on numbers. It's a lot like how "machine code" bears little readable relationship to the original source code. But they mean the same thing.
Aside
Quick question. In what sense did Godel "prove" that for any statement S expressed in ZF, there exists another statement S2 which is true if and only if S can be proven?
Well, Godel described a scheme to do it, just like we describe the ASCII scheme for encoding strings.
How does Godel "know" the scheme works? Well, he can prove the scheme works using a much simpler proof system than ZF. It is true that this simpler system will have to "sit outside" ZF, in the sense that it can make statements about procedures of symbolic manipulation. But just like before, we do have to start somewhere. We have to have some original faith in at least a very very simple version of logical reasoning.
My goal so far has been to explain the context of mathematical logic. But now we can start to reap the rewards.
Godel showed that every consistent proof system (with the power to
encode number theory) is incomplete. That is, there always exists a
statement S where we can't prove S and we can't prove NOT(S).
As you may have heard, Godel's special statement is a lot like:
"This statement cannot be proven in our chosen proof system."
Now hold up. Does ZF allow us to make a statement like this? We know the language of ZF doesn't let us say just anything in the world. I can't say "Picasso is the greatest painter of all time" in ZF.
We showed that statements about numbers can be interpreted as statements about what can be proven in the proof system. That was surprising. But it's a whole new trick for a statement to talk about itself!
Well, it can be done. We already know that, for any statement S in our proof system, we can first encode S as the number X, and then pose this statement S2:
There is **no number** Y such that
(1) Y satisfies the numeric properties of a validly encoded proof,
(2) when you apply the numerical process to "extract" the
"conclusion number" Z from Y,
(3) Z is equal to the number X.
More succinctly, statement S2 says: "There does not exist a proof of S."
No self-reference yet. But check it out, let's encode S2. What if S2 itself encoded to X? That is, what if S and S2 were actually the same? Then statement S2 would be saying: "There does not exist a proof of S2."
This sounds impossible. How can a statement reference itself? Like, if a statement contains a copy of itself, wouldn't the copy contain a copy of itself, which itself... Wouldn't the statement be infinitely long?
You need to check out Quines. A Quine is a clever computer program that prints its own source code out. You're not allowed to do any cheating by opening and reading the program's source code file. It needs to be entirely self-contained. Go look one up and check out the source code. It's a really clever idea, but pretty readable when you read one.
Quines are the spiritual cousins of Godel statements. A Godel statement is a statement like S/S2. A Godel statement is a statement that references itself. Specifically, it references its own provability.
So we finally ask, can you prove S/S2? Well, if you could, you would be proving something that is untrue. But we said that a system can only reach unsound conclusions like this if the axioms contain a contradiction.
So let's assume the best. We assume the system is consistent, which means there is no proof of S/S2. But in that case, S/S2 is true. When we can't prove true statements, that's incompleteness.
So we have come to the fundamental choice: we can have consistency, or we can have completeness. Any system that lets us do basic number theory inevitably allows us to create these Godel statements, so any system that lets us do basic number theory cannot be both consistent and complete.