The probabilistic argument may form a proof suitable for empiricists.

All physical laws may be restated in Craig-conditioned language; this is a corallary of Craig's theorem.
Arbitrary physical statement S may be replaced by "censored" statement S' following rule of production k within the metalanguage L* , containing L which language contains the currently-stated mathematical templates which describe physical behavior, and L' the language which covers the same set of behaviors using mathematical notation which lacks the infinity symbol.
By Craig's theorem, L' can exist.
Therefore k denotes a correspondence between S, our arbitrary observation of physical behavior, and S' its corrected restatement freed of the poison term.

The Gödel number corresponding to k is guaranteed to be finite and unique, for it is the product of unique primes making up its linguistic elements.
This assures us that k can be produced and stated in finite time with a finite sequence of operations.
This asymptote does not assure us of practical computability, so let us introduce the parsing operator z.

To begin our consideration of language replacement, we need to understand the equivalence of machine design and symbolic logic.
This is a further consequence of Craig's theorem.
If a determinate (race-free) gate array can be built in satisfaction of a particular equation, it certainly demonstrates a solution to the corresponding logical deduction.
The electronic circuit is the physical implementation of the abstract logical statement, but it provides the further information such as accuracy, timing and entropy we need in our decision whether we should try to make our arbitrary statement about the physical world.

It is trivial to show that any logical statement can be implemented electronically with combinatorial circuitry.
The point is, the existence of a particular logic circuit represents a statement about optimization: the logical statement representing its inputs and outputs can be solved in a time not greater than the cascaded propagation delays of this circuit, as an upper bound.
This gives us the useful guage of logical efficiency.
In general, optimality cannot be assured for logical assertions of useful complexity, but the upper bounds can be given by gate-array models, each successful design showing that the minimal time needed to resolve this assertion cannot be greater than the fallthrough time of this array.

Thus logic has an efficiency criterion, which makes the principle of parsimony concrete.
The technique shows clearly the reason infinities are meaningless, for no infinity can be produced by any physical gate array.
Open-ended iteration, endless repetition, loops without exit, are quite obviously pathological states caused by poor design, so every infinity introduced into logic circuitry is clearly an error.
Introduction of race states, endless loops, and indeterminate states can be classified as preventable error if it is predictable.
Logic has no room for infinite operations.

Gödel numeration gives us an upper bound for the complexity needed to make any logical statement.
Gödel numbers are not designed for practical computability (they are much too large.)
However, they were never intended for use in computation, but merely to depict the inherent theoretical finitude of logic.
They have done so, which none can deny.
Their power is such that no one who believes in counting, that counting will exhibit consistent behavior when extended, can deny a proof properly presented with Gödel numbers.
Craig showed that complex languages can be built up of these numbers without sacrificing their innate rigor.
He proved that the general problem of language replacement can be solved in finite time.
Our task is to provide a way to trim it down below this upper bound, to show that our deduction engine is practical, not just potential.

Now we can prepare for the release of our wizards.
State the finite deduction engine as a software project: make it a translation filter for physical approximation equations, with the useful feature that it traces back the derivation to reject any encountered infinitudes.
If the engine can produce a finite proof that results in a mathematical model matching the instrumental observations, and do this within a practical time, the rationalized equation is output and the derivation retained as establishing a new upper bound of the minimal required time to prove this equation, which is observed to predict the behavior of some aspect of the natural world.
This finite deduction engine, which when combined with its database of observations of physical phenomona may be referred to as the physics engine, operates under a constant self-improvement bias to improve its own predictive efficiency.

As to the enumeration of linguistic elements, efficiency and rigor do not meet at any convenient point.
True Gödel numbers must be immediately discarded as unuseable because of their growth functions, too big meaning too slow.
In a real-world software implementation the amount of granularity in scaling could be controlled by storing a hash-collision probability tag with the hash code of a datum.
When the error probability becomes excessive, it signals that the granularity of the present scale has been exceeded, or equivalently that this hash bucket has had more insertions than its optimum.
We may choose the degree of confidence in rigor of the finite deduction engine by choosing the number of potential ambiguities we can willingly accept; this is done in the interests of reducing execution time.
Index numbers for practical use must be smaller than Gödel numbers, and they may be much smaller without practical risk of ambiguity.
No longer can they be absolutely assured of uniqueness, so rigor is lost immediately.
Probablistic arguments remain, and they have a coefficient of probable error, so we have a mathematical template which is suitable for scientific decision making.
We have introduced a new noise source, logic noise, but we have gained much in predictivity.

The use of Gödel numbers in mathematical proofs is only possible because of their guaranteed uniqueness.
No more than one well-formed formula of the language can correspond to a given Gödel number, so no ambiguity is possible.
We must show here at least the possibility that there can be a coding for grammatical indexing of mathematical statements about instrumental data, which will result in a useable predictability with specified error bounds.
By keeping tabs on the run-time estimates, heuristic optimization can result from minimizing these figures.
But in general, the reduction of run time results in simpler logic, so the engine tends to generalize, to pull theories out of raw data, as it were.
The physics engine would help us all learn, though Gödel warned us not to expect consistency and completeness both.

There may be an enumeration system less drastic than Gödel numbers while retaining full rigor; much progress has been noted in coding theory.
The finite deduction engine would be greatly aided by any shortcut which would come up with numbers short enough to be useful data tags.
In actual processing, long tags should probably be hashed, perhaps to a pointer, to reduce internal bandwidth requirements, so long as it is recoverable from somewhere within the process.
Intuitively, there would seem to be some advantage in assigning lower primes to predicates, operators.
The lowest primes should not have to bear any burden of uniqueness as significators, if that should cramp their arithmetic usefulness.
In architectures which do not cross address and data busses, the point is moot, without the possibility for ambiguity.

Assignment of modestly "large" primes as data tags could easily keep operators separate as composed of much smaller tags, which would allow syntax parsing by a sorting array for the simplest statements.

In full rigor, note that in a Craig language which disallows endless loops, no defining procedure for infinity can be generated.
That generalizes to all computer languages: infinite operators are always errors.

Whereaway?

rev 980303