This question was raised in another thread, and is controversial enough to warrant its own discussion. Gottlob Frege, a 19th-20th century mathematician, developed a strict definition of 'proof' which is essentially the definition that logicians still use today. "In essence, he defined a proof to be any finite sequence of well-formed statements such that each statement in the sequence either is an axiom or follows from previous members by a valid rule of inference. A proof of the statement B from the premises A1,...,An is any finite sequence of statements (with B the final statement in the sequence) such that each member of the sequence: (a) is one of the premises A1,...,An, or (b) is an axiom, or (c) follows from previous members of the sequence by a rule of inference." (see link above)

Most mathematicians can agree on this definition; it's the actual axioms or rules of inference that they can't agree on (depending on your terminology, a logical axiom could also be considered a mathematical rule of inference). There are two main schools of logic with different axioms: classical logic and intuitionist logic. Actually, classical logic could be considered an extension of intuitionist logic, since it embraces all the axioms of intuitionist logic, then adds additional axioms which intuitionists reject.

Here are the axioms of institutionist logic:

A → (B → A)

(A → B) → [(A → (B → C)) → (A → C)]

A → (B → A B)

A B → A

A B → B

A → A B

B → A B

(A → C) → ((B → C) → (A B → C))

(A → B) → [(A → ¬B) → ¬A)

¬A → (A → B)

For all x A(x) → A(t)

A(t) → x exists such that A(x)


Classical logic adds the Law of the Excluded Middle:

A ¬A

or equivalently, the law of double negation:

¬¬A → A

This axiom is extremely important because it allows proof by contradiction, in which a theorem is proven indirectly by showing its negation to be false. Mathematicians have proven many theorems by contradiction which would be very difficult or even impossible to prove by other methods.

Intuitionist logic and constructivist mathematics (which is based on intuitionist logic) still have a respectable following among mathematicians precisely because they are so intuitive. Simple theorems which have never been proven or disproven despite repeated attempts (such as the Goldbach Conjecture, which has stumped mathematicians for 260 years), defy the Law of the Excluded Middle, and support the intuitionists' cause.

So which one is right? At this point, there's no clear-cut way to decide. Classical logic has greater utility and can prove more results, but intuitionist logic assumes less, so its results are less likely to be found invalid in the future, and seem more reliable from an intuitive perspective. Also, intuitional logic is more compatible with fuzzy logic, which could play a large part in future "smart" technology.

This message has been edited. Last edited by: silenteuphony,

And, your question is?

Hmm, guess I did go into lecture mode there, must be the teacher in me. I guess the question is what do you think constitutes a valid proof? I provided a lot of background info, but I'd still be interested in hearing people's opinions on this, since it is a controversial topic (at least among mathematicians). There's plenty of area I didn't cover, which is also related to what constitutes a valid proof.

For example, what do you think about using computers in proofs? This is something that has become more of an issue in modern times. Rather than a self-contained chain of steps, some modern proofs have steps that basically say the computer tested a bunch of cases using some algorithm, and we just have to take the person's word for it, or run a similar program and see if we get the same results.

And what about the Axiom of Choice? This is another place where classical logicians and intuitionists part company. Even some mathematicians who consider themselves classical logicians will get a little uncomfortable when they have to use this in a proof, and they prefer using other methods when possible. Do you think the Axiom of Choice is valid?

Granted, these are questions that only dedicated mathematics enthusiasts would find interesting, but it was a dedicated mathematics enthusiast (Dr. Gerard) who suggested the thread. So hopefully I'm not the only person nerdy enough to enjoy this thread.

SE: Your question is a very significant one, of course. I doubt that we have scope enough here to handle it in the way it needs to be handled, though.

I was about to respond to your original post by bringing up the axiom of choice myself.

The intention of the "logicist" school, founded by Frege, and worked out in much greater detail (and independently) by Russell and Whitehead in PM, was to prove that all mathematics (and hence all proofs in mathematics) was reducible to logic, the latter being a set of self-evident axioms together with an equally self-evident set of rules of inference. The logical positivist school, which PM inspired, claims to know that all logical truths are just those which might be called tautologous.

It is evident to all but the most diehard postivist, however, that the axiom of choice is not tautologous in any meaningful sense. If it is true at all (I happen to believe it is), then it must be accepted as an instance of Kant's(horror!) synthetic apriori. So did we make a big mistake by throwing stones at Kant?

There is worse. Not only the axiom of choice, but set existence axioms, usually axiom schemata, in fact, which bring in whole infinities of axioms at a stroke. Even the simplest math of the logicist sort can't get off the ground without these, either. And precisely here is the most unintuitive thing of all, the need to restrict set existence axioms so as to rule out self-contradictory ones such as the set of all sets not members of themselves (Russell's paradox). Find a way to do this without ad hoc measures, and maybe, just maybe, the result will be what might correctly be called logic.

Your question, SE, about computer generated proofs is also a good one.

In a sense, this question arose long before computers, though. Much of the foundation of mathematics rests upon proofs that are "metamathematic." They amount to proofs only if one grants that one understands perfectly what it means to iterate a certain kind of inference an indefinite (possibly infinite) number of times. Hasn't one, as in "proofs" of the principle of mathematical induction, for example, already assumed it tacitly to be true?

Relevant to your question, I think, is the one posted earlier by Professor about a report on the new "primality algorithm." This turns out to be almost entirely about computability, and has nothing essentially new to offer about primality. Still, the authors quite correctly devote much of their paper to a proof that their algorithm is valid. It's worth looking at here (you will be asked whether you want to download the original paper in pdf format). Their proof itself is a mathematical one, and doesn't depend upon computers. So it should be.

Mathematics: invented or discovered?

Sorry it took me a while to reply, I've been spending what little spare time I have in the Mathstronomy Revisited thread, where I finally managed to get a general solution (hallelujah!). Your suggested categorization of the Axiom of Choice as "a priori" knowledge raises some very interesting issues.

At the risk of oversimplification, I might call a priori principles "natural laws" in the sense that they are universally true, independent of human experience. Certain axioms are so fundamental to reality that it is easy to place them in this category: for example the reflexive (x = x), symmetric (x = y → y = x), and transitive properties (x = y and y = z  →  x = z) of equality.

In a sense, these a priori principles were not "invented" by mathematicians, but "discovered," since they existed long before humans were even capable of understanding them, since the universe began, if you take Kant's a priori concept to its ultimate conclusion.

However, even though these principles are independent of human experience, they are quite readily verified by human senses, once you impose a more concrete definition on "equality." If we take the term equal to mean "having no measurable difference in any physical characteristic," then we could theoretically find or manufacture three equal (to the degree that we could measure them) objects and verify the properties of equality.

Thus, we see a priori knowledge reflected (if not originated) in "a posteriori" knowledge, or the empirical realm of the senses. However, the Axiom of Choice is not so easily reflected in the empirical realm. Even the concept of infinity cannot be verified by the senses. One might expect a universal, natural law to be observable in the natural, empirical world.

If anything, the Axiom of Choice occupies an unnatural realm, an abstract twilight zone where spheres can be broken into pieces and reassembled into larger spheres (although the reassembled "sphere" itself has little resemblance to the globes of our empirical world). I think even an intuitionist would concede that the basic properties of equality were discovered, not invented, but they would probably consider the Axiom of Choice, and even infinity, a purely invented concept.

Personally, I would be much more comfortable placing the Axiom of Choice in a different category, not a universal principle, but an elective axiom, much like the continuum hypothesis. Just like the continuum hypothesis, it is logically consistent with set theory, but not an essential ingredient of it. Both of these axioms also deal with infinity, which may not truly belong in the realm of natural laws or in the realm of the empirical.

For these "infinite principles," it may be necessary to consider a third category besides Kant's a priori and a posteriori knowledge. A principle may be outside the realm of empirical knowledge, and even be consistent with other a priori principles, and still not be a priori knowledge itself, at least in the sense that it isn't a universal tautology. We've already seen this with the continuum hypothesis, and I'm sure there are many other axioms that fit into this category. If we include the Axiom of Choice in this abstract realm, at least it will be in good company.

This message has been edited. Last edited by: silenteuphony,

Perhaps a conversational definition is that which proves what cannot already be assumed, such as proving the Pythagorean Theorem or difference of squares. All you see in the formulae are a^2 + b^2 = c^2 and a^2 - b^2 = (a+b)(a-b). You can't just say those, cuz they're not initially known to be true.

I'd love to see a proof of the reflexive property

First of all, it must be emphasized that a proof is always a proof in a given system. In his initial post, SE outlines what amounts to a version of the first order predicate calculus (though be needs to add the rule of inference known as modus ponens, at least, to get the system running).

No proofs of identity theorems are forthcoming in such a system. To produce these, we need to define what we mean by identity in terms of some suitable extralogical predicate. In a system like that outlined by Quine in Methods of Logic, we can proceed in terms of the set-membership predicate and define identity between sets as

Df. x = y for (z)(zÎx º zÎy)

Now the statement
zÎx º zÎx
is an axiom by virtue of being a truth functional tautology (in Quine's approach, e.g.). Universal generalization of this statement leads to the conclusion x = x by merely applying the definition above.

Note that this is not a proof of the reflexitivity of identity in a general sense, but only for identity of sets. And even here, it is possible, perhaps, to quarrel with the adequacy of the definition which makes the trick go. Is the notion of two sets being identical completely and correctly analyzed in terms of common membership (what is sometimes called the extentionality postulate, though here it is not a postulate, but a mere definition.)

The proof of elementary theorems of arithmetic in PM and related systems is similary very much tied to definitions. It is a theorem of PM that 2+2=4. But that proof is a proof of the ordinary language theorem pronounced in much the same way only if we can agree that the analysis of natural numbers such as 2 and 4 as sets of sets with 2 or 4 members is taken to be entirely adequate. Needless to say, such an analysis can be, and has been, doubted.

To SE: I think maybe we don't have the same idea of what Kant meant by the synthetic apriori. A synthetic statement was, as I understand him, just one which is not analytic. So you and I and Kant would seem to agree, I think, that the axiom of choice and the continuum hypothesis are both of them synthetic. I didn't mean to say I thought either of these was true apriori. But for Kant, if they were not, they would simply fail to be logic or mathematics in any sense at all. Your notion of high level empirical generalizations reminds me a lot more of Quine than it does of Kant.

I'm no expert on philosophy, and after further research, I think I have to agree with you about the Axiom of Choice (along with the Continuum Hypothesis) being synthetic a priori. Besides being about infinity, the Axiom of Choice and the Continuum Hypothesis are both undecidable theorems in basic Zermelo-Fraenkel set theory. I'm starting to think that undecidable theorems may be exactly what Kant meant by synthetic a priori, but he didn't have any good examples while he was around (besides Euclid's parallel postulate, which nobody knew was undecidable yet). I'll have to do some more studying and get back to this.

[This message was edited by silenteuphony on 08-27-02 at 10:40 AM.]

Okay, I think I've got some of Kant's basic definitions ironed out. A priori judgments are those judgments which are made (or can be made) independently of empirical (sensory) experience. A posteriori, or empirical judgments, are those judgments which depend on empirical experience.

Analytic judgements are those judgments which can be made purely from analysis of the statement in question (i.e. does the subject logically imply the predicate), without making any additional assumptions or associations. Synthetic judgments are those judgments which depend on making an assumption or association which is not derivable from the statement alone.

Let's assume (as Kant did) that all judgments are either a priori or empirical, and either analytic or synthetic. By definition, all analytic judgments are a priori, since they cannot depend on anything other than internal analysis, which excludes empirical experience. This also implies that all empirical judgments are synthetic. So we know the following:

	empirical	a priori
analytic	NO	YES
synthetic	YES	??

The question remains: is there such a thing as synthetic a priori knowledge? Kant believed there is, and looked to mathematics for examples. I believe he was instinctively drawn to the right field, but he was born too early to find the evidence he needed. Since mathematics is a "pure" science, and doesn't depend on empirical experience, then mathematical knowledge is certainly a priori.

However, considered as a whole system, any mathematical system (in Kant's time) could be considered purely analytical, since all of the statements were assumed to follow from the basic axioms, and no additional assumptions or associations were required. I think Kant was ahead of his time, though, because he sensed there was something synthetic about mathematics, that there were some statements in mathematical systems that would require synthetic leaps of logic beyond the implications of the basic axioms.

Gödel would prove this 150 years later with his Incompleteness Theorem, but in Kant's time there were no clear examples. This didn't keep him from trying, but the examples he used were criticized by many philosophers, leaving the existence of synthetic a priori knowledge highly debatable and controversial.

Ironically, the example Kant needed was within his grasp, but he didn't know it. Euclid's parallel postulate was, in fact, an undecidable theorem by the other axioms of plane geometry, and therefore a prime example of synthetic a priori knowledge. However, once again, Kant was born too soon, since it was over twenty years after his death that the logical independence of the parallel postulate, and with it non-Euclidean geometry, was established.

So modern mathematics has brought us some perfect examples of synthetic a priori knowledge (which is why this thread is in mathematics and not philosophy). Three prime examples are the parallel postulate (and its non-Euclidean alternatives), the axiom of choice, and the continuum hypothesis. I'm sure there are more waiting to be identified (the Goldbach Conjecture?); number theory could be a rich source of undecidable statements. It's a shame Kant couldn't be around to see it.