The Constructability of Artificial Intelligence - Bruce Edmonds

Appendix

In the below, L(x) is a predicate in a recursively axiomatisable first-order logic with equality.

If whenever we could compute the truth of L(x), for any given x (with a program p), we could also compute the program p from the expression of L in the logic, then if we wanted to know whether L was implementable, the mere existence of such a program, p, would be sufficient - as we would also know that we could compute that program.

If, on the other hand, there were cases where there is a program p that computes L, but there is no way to compute that program p from L, then it is clear that it is, at the very least, highly misleading to say that "L is implementable". In such a case it may be possible to come across the program p by accident, but then we would still need to check that it was the correct program.

Below we show that, given plausible limitations on our programming ability, such cases do exist. Thus the normal characterization of computability is too weak for the purposes of the arguments in this paper. Unless there is some calculating devices more powerful than a Turing machine, in order to program L, we (aided by computers etc.) must be able to find a TM to compute it. If this is not to be the result of an unverifiable accident we must be able to somehow effectively construct the TM that computes L.

We can formalise the situation in the following way. L is a statement in some recursively axiomatized logic. So the statements in this logic can be effectively enumerated . Similarly enumerate the possible TMs .

We then say, , or an implementation, if

(1)

and is realisable implementation, iff

(2)

Then define , or is an effectively realisable implementation if, in addition to condition (2),

(3)

The program represents the combined algorithm of all our ways of constructing programs from statements like , in a planned, verifiable way. Of course, this may be different for different people, and at different times, but fixed for any particular person (or calculating device) at one time.

The question then becomes, given any particular , encoding a systematic method of building a programs from statements in this language, "Are there pairs that are a realisable implementation but not a effectively realisable implementation?". In other words Is there a difference between the normal criterion of computability and such "systematically realisable computability"? The answer to this is "Yes", as I now show

Generated with CERN WebMaker