Four of my postings to the FOM mailing list are good summaries of some of my views about mathematical truth. They are included below along with links to the archived postings on the FOM site.
The consistency of a formal system is logically determined by its axioms even though we know from Gödel's work that there can be no general way to determine this. The posting, "Logically determined", explores what part of mathematics is objectively true or false in this sense.
The posting "Gödel, Darwin and creating mathematics" explains how a mind capable of developing mathematics could have evolved in light of the limitations discovered by Gödel. It speculates about the future evolution of mathematics in the short and long run.
Proposals for extending set theory usually do so by expanding both definability and provability though large cardinal axioms. There are problems of arithmetic solvable by such axioms and not by existing weaker systems. The posting "Definability and provability" suggests how mathematics might evolve as computer verification of proofs and related software evolves to a point where it becomes nearly as easy to develop a computer assisted and verified proof as it is to create a publishable proof by hand. It will be possible to work on problems with far greater combinatorial complexity than is practical today. This may lead to the definition of recursive ordinals large enough to prove the consistency of ZF plus large cardinal axioms. Such an approach may support the expansion of mathematics without expanding definability beyond "logically determined" mathematics.The Platonistic philosophy of mathematics discusses how tednology has partially vindicated the philosophy of Plato and how much of mathematics can be justified.
2+2=4 is true in all universes with cardinality of at least 4 assuming one is using those symbols to refer to standard integers. In contrast parallel lines may or may not meet in a given universe depending on the geometry of that universe. This illustrates what I mean by logically determined. Once a geometry is specified, the fate of parallel lines may become logically determined.
The consistency of a formal system is logically determined by its axioms. The axioms are either consistent or inconsistent. Gödel proved that one may not be able to decide this question from those axioms. Thus the intuitive idea of logically determined must mean something more than deducible from axioms. Gödel proved the incompleteness of logic as well as mathematics.
Gödel also pointed the way to a deeper understanding of what we mean by logically determined. The axioms of a formal system determine not only its consistency but also its omega consistency. An example of an omega inconsistent system is one that proves a particular Turing Machine (TM) halts that does not halt. The axioms of the system say something about a recursively enumerable sequence of events that is not true.
A large fragment of mathematics is composed of statements that say something about a recursively enumerable sequence of events that would seem to be objectively true or false. For example the arithmetical hierarchy can be constructed from iterating the question does a TM have an infinite number of outputs, does it have an infinite number of outputs an infinite subset of which are the Gödel numbers of TMs that themselves have an infinite number of outputs, etc. One can iterate this up to any recursive ordinal and construct the hyperarithmetical hierarchy. Even some questions that require quantification over the reals can be interpreted as referring to a recursively enumerable sequence of events. One example would be asking if a TM defines a notation system for a subset of the recursive ordinals.
I suggest that logically determined statements are those that make an objective statement about a recursively enumerable sequence of events. The catch is defining which statements (and thus which relationships between events) are objective. Since logic is provably incomplete this cannot be precisely defined. It is a philosophical idea not a mathematical assertion. It is a suggested refinement to the notion of a Platonic ideal reality. It is based on contemporary mathematics and computer science and on the old idea that infinity refers to an unlimited and thus unrealizable potential.
This approach puts some statements in ZF about uncountable set in the category of Euclidean geometry. They are not objectively true or false but have an objective interpretation relative to specific formalizations of mathematics. The provably definable objects in formal systems constructed by finite beings have definitions that are recursively enumerable as are the provable relationships between those objects.
Mathematics, as a cultural institution, is a great many things. We arrive at a deeper understanding through many divergent and even at times mutually inconsistent paths. However there seems to be an underlying ideal of irrefutable truth in an uncertain world that mathematics strives for. Thus I suggest that ideally mathematics is about formalizing which conclusions are logically determined by assumptions. This includes both choosing interesting assumptions to consider and expanding logic to decide a wider variety of interesting questions.
Gödel's Incompleteness Theorems suggests a philosophy of mathematical truth that is both objective and creative. Logically determined statements, like the consistency of a formal system, are objectively true or false even though there can be no general process for deciding this. Emil Post reached a similar conclusion over 60 years ago: "The conclusion is unescapable that even for such a fixed, well defined body of mathematical propositions [a formulation of the recursively enumerable sets], _mathematical thinking is, and must remain, essentially creative_." (from the published lecture Recursively enumerable sets of positive integers and their decision problems" www.projecteuclid.org/euclid.bams/1183505800 ).
I discussed objective mathematics in [Logically Determined] http://www.cs.nyu.edu/pipermail/fom/2010-May/014792.html This posting focuses on the creation of mathematics. My assumptions are that physical reality is always finite but could be potentially infinite and the laws of physics are recursive.
In the light of Gödel's work, these assumptions may seem to be an obstacle to the evolution of a mind capable of developing mathematics. Gödel established limits on what mathematics a recursive process can decide, but not on what it can explore. It is straight forward to write a single nondeterministic TM program to enumerate all the axiom systems definable in a formal language and to deduce all the theorems decidable in each of these systems. While this is not a practical way for us to create new mathematics, biological evolution did something a bit like this in evolving the mathematically capable mind. That process involved an immense diversity of life over billions of years.
Our sense of the innate truth of fragments of mathematics is an evolutionary legacy. It evolved because there are modes of thought that consistently lead to accurate conclusions. These modes of thought were refined and formalized through cultural evolution. This suggests two questions. How close are we to the limits of what is achievable with our evolutionary legacy? That is how far can we confidently extend our ability to decide questions about objective mathematics? The second question is what happens when we approach the limits of what is achievable from that legacy?
I suspect the answer to the first question is that we are far from those limits in part because computers have not been used as a research tool for expanding the foundations of mathematics. They are used for automated theorem proving and proof verification, but not to explore and understand the ordinal hierarchy that is essential to expanding the logical power of mathematics. There is a combinatorial explosion of complexity in developing the ordinal hierarchy at the level of the recursive and countable admissible ordinals, where it is directly connected to recursive processes and can be investigated using computer experiments. Although currently the most powerful expansions of this hierarchy come from large cardinal axioms, I suspect that, eventually, more powerful results will be obtained through a mastery of the innate complexity of the ordinal hierarchy at these lower levels. At some point it becomes impossible to manage this complexity without the aid of computers. For more about this see my page on the ordinal calculator, www.mtnmath.com/ord.
Appel and Haken pioneered using computers to manage complexity in mathematics over 30 years ago in their proof of the four color theorem. They used the computer to deal with the combinatorial explosion of special cases that had to be considered. The complexity of their proof justified a careful process of acceptance, but the use of computers should have been recognized as a powerful new technique for dealing with complexity and not seen as a possible reason for rejecting the proof.
My answer to the second question is that we will eventually need to return to the nondeterministic search of biological evolution. This will require following an ever increasing number of paths as resources become available. Unlike biological evolution, this increasingly divergent search will be guided by a deep understanding of which paths may be worth pursuing. Under my assumptions about physical reality, any approach limited to a fixed finite number of alternatives will run up against what I call a Gödel limit. Continual progress can be made defining more powerful axiom systems into an unbounded future but the entire sequence of correct results will be theorems provable from a more general axiom that will never be considered or explored.
A formal system has two measures of its strength. What questions can it define and among these what questions can it decide. As a practical matter the systems strongest in definability are usually strongest in provability, but this is not a logical necessity. Specifically large cardinal axioms are simpler and easier to deal with than axioms that assert the existence of a recursive ordinal large enough to decide the same arithmetical questions, but every arithmetical question is decidable by an axiom that asserts the existence and enumerates the structure of a sufficiently large recursive ordinal.
Richard Elwes in the New Scientist says: See: http://www.newscientist.com/article/mg20727731.300-to-infinity-and-beyond-the-struggle-to-save-arithmetic.html
The only way that Friedman's undecidable statements can be tamed, and the integrity of arithmetic restored, is to expand Peano's rule book to include "large cardinals"...
Ignoring the mistaken suggestion that the integrity of arithmetic needs restoring, large cardinal axioms are not the only way to decide the interesting problems Friedman has proposed and solved. although they appear to be the only practical way today. This can change.
On 08/14/2010 03:54 AM, Harvey Friedman wrote: (See http://cs.nyu.edu/pipermail/fom/2010-August/014986.html)
... ultimately rigorous mathematical proofs have actually been constructed - with the help of computers - for a substantial number of theorems, including rather deep ones. E.g., see http://www.ams.org/notices/200811/tx081101408p.pdf This also has a careful discussion at the end of what major advances are needed in order for the construction of ultimately rigorous mathematical proofs to become attractive for more than a few specialists.In the article Friedman references, Freek Wiedijk says,
In mathematics there have been three main revolutions:
1. The introduction of proof by the Greeks in the fourth century BC, culminating in Euclid's Elements.
2. The introduction of rigor in mathematics in the nineteenth century. During this time the nonrigorous calculus was made rigorous by Cauchy and others. This time also saw the development of mathematical logic by Frege and the development of set theory by Cantor.
3. The introduction of formal mathematics in the late twentieth and early twenty-first centuries.
Most mathematicians are not aware that this third revolution already has happened, and many probably will disagree that this revolution even is needed.
The computer will likely change the game in mathematics as it has done in other scientific fields. In a posting in January Friedman called attention to how this worked in a chess competition where computers and humans formed cooperative teams in a high stakes tournament. A team of amateurs won, beating out teams that included grand masters. (http://cs.nyu.edu/pipermail/fom/2010-January/014359.html) Presumably this was because they were best able to combine human intuition with the combinatorial power of the computer.
Once rigorous computer aided and verified proofs are nearly as easy (or easier) than hand generated publishable proofs, they will rapidly become the norm. Work will expand on creating new tools to simplify and automate the process. Mathematicians will be able to work with far more complexity than is practical today. Those who are best able to leverage this capability and to integrate human intuition into this framework will be the most successful.
Tools may become available that will allow us to directly define as iterative processes, recursive ordinals large enough to prove the consistency of ZF plus various large cardinal axioms. Using axioms that define recursive ordinals and facilities for automating and verifying complex proofs we should be able to solve some problems that currently require large cardinal axioms (or at least the assertion that these axiom systems are consistent). Will such results strengthen interest in large cardinal axioms or suggest that they are a bridge or more too far when it comes to mathematical definability? Will it perhaps do both?
Feferman said "I believe the Platonistic philosophy of mathematics that is currently claimed to justify set theory and mathematics more generally is thoroughly unsatisfactory and that some other philosophy grounded in inter-subjective human conceptions will have to be sought to explain the apparent objectivity of mathematics." (see http://math.stanford.edu/~feferman/papers/newaxioms.pdf ). This posting assumes the universe is always finite but may be unbounded. It suggests that most of mathematics is objective in and possibly relevant to such a universe. Technology has justified a limited form of Platonism that refers, not to another universe. but to physical means for idealizing part of finite mathematics. We cannot construct Plato's perfect circle, but pi has been calculated to over a trillion decimal places with a high probability that it is correct. The complexity of finite statements that can be physically simulated is continually increasing. Pi is the limit of a convergent recursively enumerable sequence of numbers defined by finite statements.
Infinity is a human conceptual creation that in some cases can be objective. A recursively enumerable sequence of finite statements may be all true or all false. There is no physical reality that corresponds to these two alternatives, but they are logically determined by events each of which is plausibly objective. This can be generalized by defining an objective statement as a logically determined statement about a recursively enumerable sequence of finite or other objective statements. This is sufficient to define the hyperarithmetic hierarchy.
Logically determined in this context is a philosophical concept that is subject to indefinite expansion. For the hyperarithmetic hierarchy it can be limited to a recursively enumerable sequence of objective statements that are all true or all false. In general it requires that all events that directly or indirectly determine the outcome are recursively enumerable and that their relationship is objective. It is the latter condition that is indefinitely expandable and correspondingly subject to error.
Consider an always finite put potentially infinite universe determined by recursive laws in which a species can in theory have an unbounded number of direct descendant species. The question will a species have an infinite chain of descendant species is determined by a recursively enumerable set of events, the history of the species and all of its direct and indirect descendant species. Yet this question requires quantification over the reals to state. Although they are not part of engineering mathematics today, I speculate that important questions about divergent creative processes like biological evolution will often involve quantification over the reals.
In the universe postulated here, Cantor's proof that the reals are not countable establishes the incompleteness of definability in any formal system. One can always use diagonalization to define more reals. Large cardinal axioms can be thought of as proposed extensions of this idea. They postulate hierarchies of yet to be defined reals, functions on reals , etc., that apply to any "correct" formal system that can be defined. Statements about uncountable sets do not necessarily have a definite truth value since the sets they refer to cannot have a definite meaning in this universe because there is no rigorous way to define the absolutely uncountable.