14
$\begingroup$

I was in a discussion today with a philosopher about the merit of the technique of "proof by contradiction." He mentioned the Law of Excluded Middle, wherein we (typically as mathematicians) assume that we either have P or Not P. That is, if we show not "Not P", then we must have P.

Further along in the conversation, he mentions Kolmogorov's tendencies toward Intuitionist Logic (where the Law of Excluded middle does not hold; i.e. we cannot infer p from not not p). I located the source material of Kolmogorov, "On the Principle of Excluded Middle," wherein he states:

...it is illegitimate to use the principle of excluded middle in the domain of transfinite arguments.

Furthermore,

Only the finitary conclusions of mathematics can have significance in applications. But the transfinite arguments are often used to provide a foundation for finitary conclusions.

Additionally,

We shall prove that all the finitary conclusions obtained by means of a transfinite use of the principle of excluded middle are correct and can be proved even without its help.

My question: What does Kolmogorov mean when he differentiates finitary conclusions from transfinite arguments? Namely, what is an example of a finite conclusion, and what is an example of a corresponding transfinite argument?

(Source material cited in Wikipedia: http://en.wikipedia.org/wiki/Andrey_Kolmogorov#Bibliography)

2 Answers 2

11

The usage of "transfinite" there is not the same as what we now call "transfinite induction". Kolmogorov essentially just means "infinite".

One example of the sort of thing that Kolmogorov calls "excluded middle" is now called the "limited principle of omniscience" (LPO). LPO says that if you have any property $P(n)$ of a natural number $n$, so that each number either does or does not have the property, then either there is a number $m$ such that $P(m)$ holds, or, for every number $m$, $P(m)$ does not hold. In other words, if $(\forall m)(P(m) \lor \lnot P(m))$ then $(\exists m)P(m) \lor (\forall m)\lnot P(m)$.

LPO is trivially true in classical logic but it is not trivial in intuitionistic systems. The best way to understand this is to know that when an intuitionist says that a number exists with some property, he or she means that he or she already has an example of a specific number with that property. So LPO claims, on this reading, that there is some way to determine whether $(\exists m)P(m)$ holds, for any decidable property $P$.

Classical mathematicians will accept that, while they believe that the sentence $(\exists m)P(m)$ is either true or false, they have no way in general to decide which is the case (in general). For intuitionists, the lack of ability to decide which is the case means that they cannot assert that the sentence is true, and the cannot assert it is false. Because of their redefinition of the word "or", this means to them that they cannot assert the sentence is true or false.

The next place to go if you're new to this area is the Brouwer-Heyting-Kolmogorov (BHK) interpretation of intuitionistic logic. That provides a way for classically-trained mathematicians to understand what intuitionists mean when they say certain things, including the way that they redefine the terms "or" and "there exists".

One example of what Kolmogorov means by "finitary conclusion" is an equation between numbers such as $2^2 = 4$ or $0=1$. He might even accept equations with free variables like $3x + 5x = 8x$ or $3^x \not = 4y$. Working in classical Peano arithmetic, it would be possible to make a proof which ends with that sort of statement, but which applies LPO along the way. Such a proof would not be acceptable in intuitionistic logic.

There are "conservation results" that show that if sentences of a certain form are provable in Peano arithmetic, then they are actually provable (possibly with a different proof) in intuitionistic Heyting arithmetic. This is what Kolmogov is referring to when he says

We shall prove that all the finitary conclusions obtained by means of a transfinite use of the principle of excluded middle are correct and can be proved even without its help.

3

I think you will find all your answers (and much more) in the very readable exposition by Thierry Coquand: Kolmogorov's contribution to intuitionistic logic, in the book Kolmogorov's Heritage in Mathematics.

  • 0
    @BillDubuque, your link "Kolmogorov's Heritage in Mathematics" --> 4042012-08-23