I spent the weekend with Kurt Gödel, reading Rebecca Goldstein's Incompleteness The Proof and Paradox of Kurt Gödel. It was Gödel, born 100 years ago in 1906, who proved the two Incompleteness Theorems, the first of which states that a formalized system capable of specifying arithmetic can be consistent, but will contain theorems which are true but which can be neither proved nor disproved within the system.
Furthermore, such a formalized system can not, within itself, prove its own consistency. To do that you have to go outside the system. This put Gödel (incompleteness) alongside Einstein (relativity) and Heisenberg (uncertainty) in architecting the scientific worldview of the 20th century.
Let's think about this again:
- you can express things arithmetically
- which you can show to be true metamathematically
- which cannot be proven/disproven arithmetically
So an arithmetic-capable system can be consistent, but not complete.
If this is a pattern, then we could restate it as:
- What is expressible in a system
- And is true in a metasystem
- May not be provable in the system
If we think about an autopoietic system - one which ongoingly generates itself, maintaining the structural coupling with its environment which is its identity - we could say that the system's call-by-future, the morphism giving rise to it, is a truth asserting functor from system1 to metasystem, following which the elements and rules of system2 are derived. There is structural coupling between the system and its metasystem (the environment of the system's existence), which is a living autopoiesis, giving rise to systemic forms. This coupling is tacit call-by-future - truth felt but not yet proven or manifested.
It may be that the following is another way to state this: syntax, and its consistency, is in fact driven by semantics. You can not actually exclude the mathematician from the arithmetic (as the Hilbert program to formalize mathematics had claimed). Or, as Gödel, who was philosophically a Platonist, might have said, without the mathematics experienced by mathematicians there is no existence to formalized mathematical systems. I myself would extend that to include Platonic form itself as only experienced in structural coupling of the human: it's real, but not independently so (just like us :-).
This is all in the interest of examining how such a process that we human beings engage in may be shared with our software, so it may care with us, be more expressive of context, system and metasystem, and be itself actively participant in creativity and truth making. I suspect such a formalization into software language cannot be made to breath without inherent human participation, built into the shared metasystem of the software.
This program is not about artificial but about symbiotic intelligence, and not so much about the semantic as about the symbiotic web.
Homage to Kurt Gödel for thinking and prompting such thoughts.