Godel showed that it is impossible to formally prove the
consistency of a system of arithmetic WITHIN that system
of arithmetic.<p>Given a static system that is clearly true.<p>However, I claim a self-modifying system can extend itself
to "look down" on the initial system of arithmetic.<p>I'm not sure how to show this yet. My intuition is leaning
toward using the standard trick of towers of types. Is it
possible to show a system of arithmetic is consistent
using higher order types?<p>Which raises the question of self-modifying Turing machines.
This leads to the concept of a meta-Turing machine.<p>Not only must the "instructions of the machine" be "on the tape"
so they can be modified but the "structure of the hardware"
also has to be "on the tape" so that changing the "structure"
changes the way the machine operates. A simple implementation
can be created in an FPGA which generates modifications to its
own Verilog definition and reloads itself, becoming a fundamentally
different machine.