[Cryptography] LUKS on ATA versus on SSD

[Jerry Leichter]

> If it had been available at the time, the identification of the symbols that Gödel chose to "number" would work just as well with use of a Unicode encoding for those numbered glyphs and then using strings of Unicodes in the formations on which Gödel based his arguments.  They make perfectly good bignums 😊.
> 
> My main point is that Gödel numberings and, say, UTF-8 strings have equivalences and one would not use an argument about those UTF-8's as something special about hashing as far as I can discern.
Well … no.  This misses the reason Gödel introduced his numbering to begin with.  Gödel was “arithmatizing” the notion of proof.

Consider the formal definition of a valid proof:  An ordered collection of (1) well-formed formulae each of which is either (2) an axiom or (3) follows from one of the earlier formulae through one of the rules of derivation, (4) the last of which is the formula to be proved.  Gödel needed to show that given the number of an alleged proof of a formula, there was an arithmetic procedure to check whether or not it was valid.

Now (2) and (4) are straightforward, given a unique number for each possible formula.  But (1) and (3), not so much.  He couldn’t just wave his hands, as we do today, and say that it’s clear we can write down a FSM to do this and FSMs are clearly equivalent to arithmetic operations.  He was blazing the trail on this stuff and had to actually write out how to do it.  The arithmetic properties of the numbering - something a UTF-8 representation lacks - was very much central to this project.

Yes, given what we’ve learned in the intervening century, we know of many equivalent notions - though if you want to formally show Gödel’s result on systems sufficiently strong to contain Peano arithmetic, Gödel’s approach may still be the shortest route.

                                          -- Jerry