Logic & Programming

Published on Apr. 19th, 2009 on https://speleologic.livejournal.com/1696.html

Some time ago I came upon a mention of Ishihara's proof technique in constructive analysis and a claim:

In [6], Ishihara introduced the following two lemmas in which, surprisingly, we can use completeness to make a decision which at first sight would seem to be impossible with purely constructive techniques (that is, with intuitionistic, rather than classical, logic). (Bridges, van Dalen, Ishihara: Ishihara’s proof technique in constructive analysis)

One does not have to be interested in mathematical analysis to appreciate it, however, it is enough to think about a sequence of computation steps and a measure of “distance” between every two consecutive computation steps. If one can prove that for a sequence the distance gets smaller and smaller as time goes on we say that the computation converges or is Cauchy. When we consider these converging processes of computation as inhabitants of some universe X we can say that X is a complete metric space.

Here I want to give a simpler (more predicative) proof of Bridges-vanDalen-Ishiharas's Proposition 1, which more obviously gives rise to a program than theirs.

Proposition 1. If X is a complete metric space, X=P∪Q, (xn) is a sequence in X that converges to x and we have ∀y:X, x#y ∨ y∉Q, then we have that (∀n. xn ∈ P) or (∃ n. x_n ∈ Q).

The role of x, y as members of X is to stand for a sequence (xn), (yn) together with a proof that the sequences make progress as time progresses, i.e. they are Cauchy/converging. The relation '#' is called apartness and it means that the two computation processes are not 'the same'.

Proof. Start with a sequence (xn). Define the binary sequence λ to be 0 as far as the elements of the sequence (xn) are in P, and to become 1 forever as soon as one of the elements of (x_n) is in Q.

Now define the sequence (yn) to be x as far as λn is 0 and to become xk as soon as λn becomes 1, where k is the smallest natural number at which λ becomes 1, i.e. the k-th element of the sequence (xn) is in Q. The sequence (yn) we defined is very similar to a constant sequence: it is either x forever, or it is x for a finite number of starting elements and then it becomes x_k forever.

In any case (yn) is Cauchy, so we can think of it as an entity y from the universe X. We now use the hypothesis given in Proposition 1 and look at two cases. if x#y then there is k, the smallest number such that λk = 1, which implies xk ∈ Q if y∉Q then we can show that ¬∃n. λn = 1 and, since λ is decidable, ∀n. λn = 0, which implies ∀n. xn ∈ P QED

Apparently, in constructive analysis they use Proposition 1 (and 2, which was not shown) as constructive instances of the general law of excluded middle. Is it useful in logic and computer science?

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net