Bubbles_glow

≡ Literary Systems ≡

 
Corner_fold
  • Citation
  • Extension
  • Response
  • Comment
Hopo_catalog
 
Flowchart_grey_24

Going Meta in Formal Systems

If this essay is going to be successful in convincing you that it's a useful practice to study code as literature, then we're going to have to address one of the fundamental breaks between programming languages and natural languages: their relationship to paradox. English has no difficulty with speaking of impossible things. I can simply say, "I am lying," a statement about which it is impossible to evaluate on the grounds of being true or false. If it's true, we think, then he's lying, so he's lying, which means he's telling the truth, so he can't possibly be truthful. And at about that point, we stop, satisfied at the recognition of a paradox. Novels introduce subtle paradoxes and ambiguities at many points, often in the service of character development. They range from Holden Caulfield's petty misdirections to Faulkner's truly unsettling habit of having characters mention things that they could not possibly have experienced.

With code, such inconsistencies, being logically impossible, are simply unable to be expressed by the language. Programming languages are examples of formal systems, so called because their stiff (prim, proper) rules forbid any such impossibilities. The dream of formal systems, especially for researchers at the start of the past century, was to create a complete and consistent formal system. Complete in the sense of being able to express every logical truth that exists, that there would be nothing true that the system was incapable of representing. Consistency meant that the system would have to be logically sound, keeping impossibilities and paradoxes well outside. There have even been dreams of extending the rule of formal systems to human thought: Gottfried Leibniz dreamed of assigning a number to every concept, and then resolving philosophical issues by manipulating these numbers within a formal system.

One of the most serious attempts to create such a complete and consistent system was made by the philosopher and mathematician Bertrand Russel, in his Principia Mathematica. Russell had recently come up with a major paradox in Set Theory, by proposing the existence of a set whose members were the sets that are not members of themselves. If you try to follow it's logic, it's another infinite loop: if the set does not include itself, then it must, if it must then it can't possibly. Russell (correctly) determined that the problem with paradox in formal systems is self-reference. If a system starts to talk about itself, then paradoxes come easy — note the form of the earlier English paradox, "I am lying." So Russell's Principia was specially designed to keep self-reference out of formal systems. He intended to do this by establishing a hierarchy of types (a potentially infinite one), and at each level, you were only allowed to refer to the types of the level beneath you. This theory of types turned out to be little more than a Maginot Line against self-reference.

The man who neatly side-stepped it was Kurt Gödel, and he did so at the tender age of 25 with his incompleteness theorem. Gödel attacked the Principia by proving that inside of every sufficiently powerful formal system, once can encode the equivalent of the statement: "This statement cannot be proven by use of this system!" Because of the manner in which the statement is encoded, the system must validate it as true, or else fall into inconsistency. If the statement is indeed true, then the system cannot prove it, which demonstrates that an unprovable truth exists, and that the system must necessarily be incomplete. This works on any formal system that is powerful enough to describe basic arithmetic. A beautiful result — it's not the weak systems that fall vulnerable to paradox, but the strong ones. It's the very strength of the Principia Mathematica that makes it vulnerable to the Incompleteness Theorem.

Perhaps because self-referentiality is both the official nemesis and inescapable fate of formal systems, the literary qualities of these formal texts are often wrapped in it. For the reader of proofs, theorems, and code, the meaning is less locked in the mechanical necessities of the surface math, and more in the meta-level ideas about the significance and consequences of what the code might do. As programming languages develop, an ever increasing number are beginning to use meta-programming techniques, where your explicit intent for the shape of the actual code becomes written into the meta-code itself. Naturally, as the meta-level capabilities of a programming language increase, and the text develops tangles of self-reference, the code itself becomes less tractable mathematically, less formal, less certain.




 
Why is the notion of a formal system so seductive for scientists and philosophers?
"The only certain knowledge science can give us is knowledge of the behavior of formal systems, that is, systems that are games invented my man himself."
— Joe Weizenbaum
If you're questing for absolute truth, the closest that you'll ever come is within the realm of formal systems. In comparison to them, the rest of science is estimation and guesswork.