Being Different
In mathematics you don’t understand things. You just get used to them—John von Neumann.
Harvey Friedman is a famous mathematical logician who spent most of his career at Ohio State University. He worked not on proving new theorems as much as finding the axioms needed to prove them. Later in his career it was the axioms needed for certain large cardinal theorems. These questions can be very subtle and difficult—not unlike lower bounds in complexity theory.
Harvey was listed in the Guinness Book of World Records for being the world’s youngest professor when he taught at Stanford University at age 18 as an assistant professor of philosophy. He got his Ph.D. from Massachusetts Institute of Technology in 1967—hence the young age.
The Difference
Harvey has taken a viewpoint for most of his career that is different from other logicians. Godel’s incompleteness theorems apply to most logic systems—certainly those that are strong enough for central areas of mathematics. But the majority of mathematicians believe that incompleteness does not apply to their everyday work. In short most do not think:
I cannot prove P not equal to NP, so it must be incomplete.
Rather they feel that this means I am not smart enough to resolve P vs NP. Which of these is true?
For example, Harvey has created numerous algebraic and geometric systems that make no explicit reference to logic but which, under a suitable coding, contain a logical system to which Godel’s incompleteness theorems apply. Furthermore, these systems look similar to many systems used by mathematicians in their everyday work. Harvey uses these examples to argue that incompleteness cannot be dismissed as a phenomenon that occurs only in overly general foundational frameworks contrived by logicians. He argues that it applies often to their everyday world.
An Example
Harvey is also able to find numerous combinatorial statements with clear geometric meaning that are proved using large cardinals axioms and shown to require them. These results are famous to Harvey. Such axioms previously seemed to require statements that are not geometric.
Gill Williamson can show that this can be used to connect these problems to the assumption that subset sum is solvable in polynomial time. See the paper On The Difficulty Of Proving P Equals NP In ZFC. This curious connection between the P vs. NP problem and the theory of large cardinals seems to suggest that either P=NP is false or otherwise not provable in ZFC. This connection is surprising.
Incompleteness
Harvey does have a conjecture that shows that certain statements are not incomplete. He is interested in both sides of this coin: sometimes statements are provable and sometimes not. Concretely many mathematical theorems, such as Fermat’s Last Theorem, can be proved in very weak systems such as EFA. The Grand Conjecture says: Every theorem published in the Annals of Mathematics whose statement involves only finitary mathematical objects (i.e. what logicians call an arithmetical statement) can be proved in EFA.
EFA is the weak fragment of Peano Arithmetic based on the usual quantifier-free axioms for 
Open Problems
When Harvey was just starting to read, at age 4 or 5, he remembers pointing to a dictionary and asking his mother what it was. It’s used to find out what words mean, she explained. A few days later, he returned to her with his verdict: The volume was completely worthless. For every word he’d looked up, the dictionary had taken him in circles: from “large” to “big” to “great” and so on, until he eventually arrived back at “large” again. She just looked at me as if I were a really strange, peculiar child, Friedman laughs.
This is an insight reported in an article by Jordana Cepelewicz. I cannot imagine Harvey was four or five when he told his mom this. For more stuff—when not so young—see the book. 
In my opinion, one of Harvey Friedman’s most impressive results is reported in Martin Davis’s April 2006 article in the Notices of the American Mathematical Society, “The Incompleteness Theorem.” It takes a few minutes to absorb the definitions and the statement, but in essence, it is an elementary proposition about finite graphs that is unprovable in ZFC but provable assuming a large cardinal axiom. Moreover, the proposition is very similar to a theorem about finite graphs that does not require strong axioms to prove.
Another paper of his that you should check out is “Long Finite Sequences” in the Journal of Combinatorial Theory Series A, July 2001. Given an alphabet with 3 letters, how long a string x_1, …, x_n can you form such that no consecutive block x_i, …, x_{2i} is a subsequence of any later consecutive block x_j, …, x_{2j}? You can check that with an alphabet with 2 letters, the answer is 11. But what about 3 letters? The answer is bigger than you think.
Incidentally, the usual terminology for a statement that can be neither proved nor disproved in a given formal theory is that the statement is “undecidable” and not that the statement is “incomplete.” It is the theory that is incomplete, not the statement. There is an unfortunate clash of terminology with undecidable computational problems, but that’s life.
Definitions are, by definition, tautologies.
Could you please correct the link to the above book (Studies in Logic) if possible?
It gives: 404: Page Not Found.
Thank you