Sun, 17 Apr 2011 13:00:00 GMT

I was just told that the equality of computable functions of type is decidable. I was a bit confused about this at first, since trivially, the equality of functions is undecidable: Let be the a complete enumeration of all proofs in our meta-theory , then define , then by Gödel's second incompleteness theorem, we cannot decide whether .

However, even though the question whether two computable functions are equal seems harder than the same question for , it is not. A first step in understanding why is maybe that every terminating algorithm is finite, and therefore can only use finitely many elements of a sequence in .

Of course, having this information without any proofs I tried to prove it myself. I noticed that this should be strongly related to the compactness theorem. And here is the outcome:

Lemma 1: Let a computable be given, and . Then there is some initial subsequence of , such that for all sequences , .

__Proof:__ A terminating turing machine can, for every given sequence , only read finitely many elements of , thus, there is an upper bound such that the program is only dependent of elements . Set and . Then for all sequences , since the program does not depend on an elements not in .

We say that a computable*depends only* on a
sequence when for every
we have , and it *depends exactly* on when it depends only on but this is not the case for subsequences .

By Lemma 1 it is trivial to proof that two functions are not equal: Just find a sequence on that both of them depend only, and for which . The more interesting part is the case when they are equal.

Using Lemma 1, we can encode such functions in the following way: Let be predicate constants, and denote by the first-order Peano arithmetic. If where depends only on , then let , where is a term constant, and can be expressed in the form as usual. Now define . Obviously, . Now, if two functions are equal, we know that is not satisfiable, and therefore, . By the completeness theorem, we therefore know that , and hence, the equality is provable.

Nice.

However, even though the question whether two computable functions are equal seems harder than the same question for , it is not. A first step in understanding why is maybe that every terminating algorithm is finite, and therefore can only use finitely many elements of a sequence in .

Of course, having this information without any proofs I tried to prove it myself. I noticed that this should be strongly related to the compactness theorem. And here is the outcome:

Lemma 1:

□

We say that a computable

By Lemma 1 it is trivial to proof that two functions are not equal: Just find a sequence on that both of them depend only, and for which . The more interesting part is the case when they are equal.

Using Lemma 1, we can encode such functions in the following way: Let be predicate constants, and denote by the first-order Peano arithmetic. If where depends only on , then let , where is a term constant, and can be expressed in the form as usual. Now define . Obviously, . Now, if two functions are equal, we know that is not satisfiable, and therefore, . By the completeness theorem, we therefore know that , and hence, the equality is provable.

Nice.