5 ms·

This question gets asked a lot, in particular by math students, and I think that the answer that is usually given, which is the same as many answers in this pag

by ot 13y ago

This question gets asked a lot, in particular by math students, and I think that the answer that is usually given, which is the same as many answers in this page, is overly simplistic: we don't care about ontological truth of our axioms (and, by the way, of the deduction scheme), we just define a set of axioms and define true as provable. This is the formalist view of mathematics, which was the dominant view at the beginning of the 20th century. This reduces math to a meaningless mind game, as acknowledged by Hilbert himself, one of the major proponents of this view: "Mathematics is a game played according to certain simple rules with meaningless marks on paper". Unfortunately, this sweeps under the rug important questions, such as "if I prove the correctness of a an algorithm, how does this increase my confidence that the algorithm will actually work?", or "if I compute the hypotenuse of a triangle with Pythagoras theorem, then cut a piece of wood and measure it, will they match?" This is why ultimately there is some belief involved. From Wikipedia [1]: "In practice, most mathematicians either do not work from axiomatic systems, or if they do, do not doubt the consistency of ZFC, generally their preferred axiomatic system" (emphasis mine). To work with with a set of axioms, we must believe that that set is both logically consistent, and that in some way its interpretation is consistent with reality. The first question cannot be answered for the interesting sets of axioms, thanks to Godel, and the second is not even well-defined. For this and many other reasons, philosophy of mathematics has mostly moved on from the logicist/formalist view [2], but as most philosophical problems, there probably will never be a conclusive answer. [1] http://en.wikipedia.org/wiki/Foundations_of_mathematics#Partial_resolution_of_the_crisis http://en.wikipedia.org/wiki/Foundations_of_mathematics#Part... [2] http://en.wikipedia.org/wiki/Philosophy_of_mathematics http://en.wikipedia.org/wiki/Philosophy_of_mathematics

yodsanklai 13y ago
"To work with a set of axioms, we must believe that that set is both logically consistent ... The first question cannot be answered for the interesting sets of axioms" Consistency of a theory may be proven or disproven in a different set of axioms. For instance, peano or presburger arithmetic are consistent in ZF. In the field of program verification for instance, people use all kinds of theories that they prove to be consistent. But I agree that at some point, one has to believe in an axiomatic system.
Dylan16807 13y ago
Completeness is overrated. Why does it matter that a system can't prove every possible statement you can write in it? It's not going to give you a wrong answer, it's just going to fail. Why is that particular lack of capability more important than the millions of statements you can't formalize in the first place? Take consistency and build something with it. P.S. Using a theory to prove its own consistency would be way more suspicious than using a more powerful theory to prove it. "The Bible is true because the Bible says so."
- deleted 13y ago
  [deleted]
- eli_gottlieb 13y ago
  >P.S. Using a theory to prove its own consistency would be way more suspicious than using a more powerful theory to prove it. "The Bible is true because the Bible says so." Which eventually leaves us either with some top-level assumptions we treat as completely axiomatic, or with infinite regress to higher and higher systems of proof logic.
- yodsanklai 13y ago
  On the other hand, consistency alone isn't really useful! Let suppose I design a new proof system to prove arithmetic propositions. Unfortunately, my system is such that it can't produce any proposition. That makes it consistent but useless.
  - Dylan16807 13y ago
    That's why you look at completeness in terms of coverage, not as a binary.
Tloewald 13y ago
It's quite common for mathematicians to consider the impact of axioms on a theorem. Mathematicians often consider whether a proof satisfies constructivist constraints, requires the axiom of choice, and consider different geometric foundations (e.g. einstein's spacetime is non-euclidean). This doesn't cause religious disputes, and indeed mathematicians are happy to jump from one set of constraints to another. I do agree that some axioms are grounded in observed reality (e.g. arithmetic, euclidean geometry) but discovering that axioms fail in unfamiliar situations is no generally a cause for soul searching or existential angst.
- Someone 13y ago
  "This doesn't cause religious disputes, and indeed mathematicians are happy to jump from one set of constraints to another." For me, that is the difference between an axiom and a belief. People with beliefs think their beliefs to be better than those of others. With axioms, that is not so. In fact, mathematicians like to doubt their axioms "do we really need the parallel postulate" was, for centuries, a subject of thought"
  - Tloewald 13y ago
    Actually for a while the parallel postulate was a matter of religious zeal. The studies of consistent geometries that had different behaviors for "parallel" lines was, for some reason, profoundly disturbing to some christians who tried to prove that the parallel postulate was not needed (i.e. That non-euclidean geometry was inconsistent). This was a matter of amusement for mathematicians, even though many mathematicians were a bit disturbed by non-euclidean geometry. Lewis Carrol, who was a mathematician and some kind of Anglican, couldn't stomach complex numbers. So religion can become confused with axioms, but it tends to start with religion, not axioms.
return0 13y ago
That is interesting, but probably both views have their merits. Belief involves emotional commitment which can create intellectual inertia that can be both good and bad, while formalism places a safe detaching distance from the subject.
tel 13y ago
To provide small insight into the work of people who actually do doubt ZFC I'd like to source two interesting books. First is Peter Aczel's work with the Anti-foundation Axiom which allows you to create sets with "infinite regress". Instead of blanket disallowing these kinds of set like ZFC does, he enlarges ZFC by allowing any set which is a unique solution to a group of equations that may be self-referential. I was introduced to this stuff by a book "Vicious Circles" by Barwise and Moss (http://www.amazon.com/Vicious-Circles-Center-Language-Information/dp/1575860082 http://www.amazon.com/Vicious-Circles-Center-Language-Inform...). The important point is that the Anti-Foundation Axiom lets us model infinite, streaming structures similar to those modeled in computer programs. It also motivates the somewhat unpopular idea of bisimulation which is very necessary for creating a kind of equality in an AFA world... and also for proving the equality of streaming algorithms. Second is Lawvere's introduction to thinking about the foundations of mathematics from a Category Theoretic perspective. Lawvere is a proponent of thinking of Set theory as simply one, somewhat interesting Category which can be generated by a more foundational theory and set of axioms. I'm not personally anywhere nearly well-knowing enough to say whether that works, but his book Conceptual Mathematics (http://fef.ogu.edu.tr/matbil/eilgaz/kategori.pdf http://fef.ogu.edu.tr/matbil/eilgaz/kategori.pdf) gives a very interesting POV on how to work from the Category Theoretical basis to answer some normal Set theoretic questions.
- nano_o 13y ago
  I think that the "infinite, streaming structures" that you are referring to can be modelled in ZFC or HOL using Tarski's fixed-point theorem. See for example the paper by L. C. Paulson, "A fixedpoint approach to implementing (co)inductive definitions". So the point of this anti-foundation axiom probably lies somewhere else.
  - tel 13y ago
    While I haven't yet read that paper, I wanted to point out a thing I just read in a coinduction tutorial (http://www.cs.ru.nl/~bart/PAPERS/JR.pdf http://www.cs.ru.nl/~bart/PAPERS/JR.pdf). Coalgebras are defined as an isomorphism between "sets" X==P(A*X) which allow us to unfold our seed state over non-determistic updates. Such a "set" obviously cannot exist in ZFC directly as it violates set cardinality. It can be a set that satisfies the AFA, though—in fact, that equation I just wrote is sufficient to define it I think and then AFA guarantees uniqueness.

by ot 13y ago

yodsanklai 13y ago

"To work with a set of axioms, we must believe that that set is both logically consistent ... The first question cannot be answered for the interesting sets of axioms" Consistency of a theory may be proven or disproven in a different set of axioms. For instance, peano or presburger arithmetic are consistent in ZF. In the field of program verification for instance, people use all kinds of theories that they prove to be consistent. But I agree that at some point, one has to believe in an axiomatic system.

Dylan16807 13y ago

Completeness is overrated. Why does it matter that a system can't prove every possible statement you can write in it? It's not going to give you a wrong answer, it's just going to fail. Why is that particular lack of capability more important than the millions of statements you can't formalize in the first place? Take consistency and build something with it. P.S. Using a theory to prove its own consistency would be way more suspicious than using a more powerful theory to prove it. "The Bible is true because the Bible says so."

deleted 13y ago
[deleted]
eli_gottlieb 13y ago
>P.S. Using a theory to prove its own consistency would be way more suspicious than using a more powerful theory to prove it. "The Bible is true because the Bible says so." Which eventually leaves us either with some top-level assumptions we treat as completely axiomatic, or with infinite regress to higher and higher systems of proof logic.
yodsanklai 13y ago
On the other hand, consistency alone isn't really useful! Let suppose I design a new proof system to prove arithmetic propositions. Unfortunately, my system is such that it can't produce any proposition. That makes it consistent but useless.
- Dylan16807 13y ago
  That's why you look at completeness in terms of coverage, not as a binary.

Tloewald 13y ago

It's quite common for mathematicians to consider the impact of axioms on a theorem. Mathematicians often consider whether a proof satisfies constructivist constraints, requires the axiom of choice, and consider different geometric foundations (e.g. einstein's spacetime is non-euclidean). This doesn't cause religious disputes, and indeed mathematicians are happy to jump from one set of constraints to another. I do agree that some axioms are grounded in observed reality (e.g. arithmetic, euclidean geometry) but discovering that axioms fail in unfamiliar situations is no generally a cause for soul searching or existential angst.

Someone 13y ago
"This doesn't cause religious disputes, and indeed mathematicians are happy to jump from one set of constraints to another." For me, that is the difference between an axiom and a belief. People with beliefs think their beliefs to be better than those of others. With axioms, that is not so. In fact, mathematicians like to doubt their axioms "do we really need the parallel postulate" was, for centuries, a subject of thought"
- Tloewald 13y ago
  Actually for a while the parallel postulate was a matter of religious zeal. The studies of consistent geometries that had different behaviors for "parallel" lines was, for some reason, profoundly disturbing to some christians who tried to prove that the parallel postulate was not needed (i.e. That non-euclidean geometry was inconsistent). This was a matter of amusement for mathematicians, even though many mathematicians were a bit disturbed by non-euclidean geometry. Lewis Carrol, who was a mathematician and some kind of Anglican, couldn't stomach complex numbers. So religion can become confused with axioms, but it tends to start with religion, not axioms.

return0 13y ago

That is interesting, but probably both views have their merits. Belief involves emotional commitment which can create intellectual inertia that can be both good and bad, while formalism places a safe detaching distance from the subject.

tel 13y ago

To provide small insight into the work of people who actually do doubt ZFC I'd like to source two interesting books. First is Peter Aczel's work with the Anti-foundation Axiom which allows you to create sets with "infinite regress". Instead of blanket disallowing these kinds of set like ZFC does, he enlarges ZFC by allowing any set which is a unique solution to a group of equations that may be self-referential. I was introduced to this stuff by a book "Vicious Circles" by Barwise and Moss (http://www.amazon.com/Vicious-Circles-Center-Language-Information/dp/1575860082 http://www.amazon.com/Vicious-Circles-Center-Language-Inform...). The important point is that the Anti-Foundation Axiom lets us model infinite, streaming structures similar to those modeled in computer programs. It also motivates the somewhat unpopular idea of bisimulation which is very necessary for creating a kind of equality in an AFA world... and also for proving the equality of streaming algorithms. Second is Lawvere's introduction to thinking about the foundations of mathematics from a Category Theoretic perspective. Lawvere is a proponent of thinking of Set theory as simply one, somewhat interesting Category which can be generated by a more foundational theory and set of axioms. I'm not personally anywhere nearly well-knowing enough to say whether that works, but his book Conceptual Mathematics (http://fef.ogu.edu.tr/matbil/eilgaz/kategori.pdf http://fef.ogu.edu.tr/matbil/eilgaz/kategori.pdf) gives a very interesting POV on how to work from the Category Theoretical basis to answer some normal Set theoretic questions.

nano_o 13y ago
I think that the "infinite, streaming structures" that you are referring to can be modelled in ZFC or HOL using Tarski's fixed-point theorem. See for example the paper by L. C. Paulson, "A fixedpoint approach to implementing (co)inductive definitions". So the point of this anti-foundation axiom probably lies somewhere else.
- tel 13y ago
  While I haven't yet read that paper, I wanted to point out a thing I just read in a coinduction tutorial (http://www.cs.ru.nl/~bart/PAPERS/JR.pdf http://www.cs.ru.nl/~bart/PAPERS/JR.pdf). Coalgebras are defined as an isomorphism between "sets" X==P(A*X) which allow us to unfold our seed state over non-determistic updates. Such a "set" obviously cannot exist in ZFC directly as it violates set cardinality. It can be a set that satisfies the AFA, though—in fact, that equation I just wrote is sufficient to define it I think and then AFA guarantees uniqueness.