Looking at a landscape, you don’t see the point from where you are looking. That point is part of the landscape, but to see it, together with the landscape, you have to move somewhere else, to a higher peak maybe or to a helicopter. If you shift your vantage point, you can see the place where you were standing before, together with your old vantage point, but again, you don’t see your new point of view.
Something comparable is happening in the “landscape” of formal theories.
Each formal theory or formal system can be described by a finite-length text containing all the axioms and rules of inference that make it up. There are variations in how formal systems are constructed. Some contain “axiom schemata”, some might be thought of as algorithms or programs and all kinds of different formalisms may be used. But in every case, they are describable as finite texts. From this finite set of initial information, a large and in many cases unlimited set of data or terms or statements can be derived. However, the formal theory you start with contains only a limited amount of information and everything derivable is fixed right from the beginning. From within the formal system, by applying its rules, it is not possible to change it in such a way that it can evolve. It is not possible that within a formal system, something becomes derivable that was not derivable before.
If we look at the formal system from the outside, we can look at all its axioms, rules of inference and programs contained in it. We can then apply operations from the outside, change or add something and extend or transform the formal system.
It is possible to build all the operations we apply to make those changes into the formal system. We then get a new, extended formal system that is more “powerful” than the original one. However, this extended formal system again is limited. Everything derivable or computable inside it is derivable or computable right from the beginning; it cannot change inside the new formal system. In this sense, the formal system is static; there is no time in it. It cannot evolve on its own. It can only be evolved from an outside vantage point. Building that outside vantage point into the system leads to a new system that in turn is unable to develop. The vantage point from which that new system can be changed shifts somewhere else.
We can say that a formal system cannot contain a reference to itself as a whole (see Ammon 2016), in principle. A reference to a formal system as a whole is always external to the system. Build it into the system and you only get a new formal system for which the point of total reference is again outside it.
In a previous article on this blog a proof was sketched showing the following about programs that compute total computable functions: any program that enumerates such programs, i.e. that produces such programs as its output, is necessarily incomplete. There is an operation that can be applied to it from the outside, from a meta-level, that produces another computable total function not contained in the existing enumeration we started with. This operation can be used to construct an extended, more powerful enumeration program that is an extension of the original one. But that extended enumeration program will in turn be incomplete, and so on.
The operation we apply to do the extension can itself be programmed as an algorithm. It is computable. We can build it into the original program and this would result in a new and more powerful enumeration program that produces all the programs produced by the original enumeration program, and many more, but the proof is valid for this new program again. We can apply the extension operation (what is called a “productive function”) to it again from the outside. So building the extension operation into the program has not yielded a complete program. Instead, the outside vantage point again shifted somewhere else. The program cannot contain a reference to itself in its totality so that the gap is closed. Building the reference into it changes it into just another formal system and “squeezes” the external reference somewhere else.
In (Ammon 2016, p. 11 – 16) Kurt Ammon presents a proof that is showing that in Gödels incompleteness proof, the fact that the reference to a formal theory cannot exist inside the formal theory itself is exactly what creates the incompleteness. Roughly speaking, for each formal theory in Gödels proof a formula can be constructed that is not decidable inside that theory, i.e. it cannot be derived in the theory and its negation can also not be derived. What Ammon is showing is that if the theory is extended by a symbol that represents a reference to the theory as a whole, we get a new, extended theory in which the undecidable formula is provable. However, this new theory in turn has an undecidable formula. However, a mathematician can always create such an external reference, indicating that a human being cannot be modeled completely in terms of formal systems or reasoning processes.
To come back to the landscape and vantage point metaphor, it is as if from within the original formal theory, we are unable to see the proof of the undecidable formula. If we shift our vantage point to somewhere else where we can see our original vantage point, that proof becomes visible. But there is a new blind spot again.
(The picture is from https://commons.wikimedia.org/wiki/File:GuanoPoint.jpg).