#formalization

personally I have never trusted any software ever so this is not a shock or cause for concern to me tbh, and is already baked into my use of lean :) If only the universe would let us prove that the typechecking algorithm never proves false... though even without that, we can definitely formally prove at least the facts that the kernel code faithfully implements the typechecking rules, which afaik is not done yet (but people are working on it)

[O]nce a distinction or a concept has been developed in formal language it can often also be expressed in non-formal language. Another way to express this is that logic is often indispensable in the contexts of discovery and justification, but dispensable in the contexts of further elaboration and dissemination.

Descriptive and Prescriptive Formalism.—A formal language can be used to describe a given state-of-affairs (describing the properties of a state-of-affairs amenable to formalization) while object-formalism can reconstruct formal analogues of a given state-of-affairs (again, reconstructing only the formal aspects of the state-of-affairs in question). Insofar as we understand formalism as the capture of that which is given in intuition, the state-of-affairs, i.e., the intuition in question, always precedes the formalization. However, a formal language can also be used to assert what state-of-affairs ought to be, and object-formalism can demonstrate how states-of-affairs ought to be structured (both, again, only in regard to the formal properties of the state-of-affairs). Arguably, while in the intuitive conception of formalization the object to be formalized is always given beforehand, the prescriptive conception of formalization is always hovering in the background, pointing onward. While prescriptive formalism is less familiar than descriptive formalism, a little thought on the matter will reveal that every state-of-affairs that strains to attain an ideal, or any concept rationally reconstructed to supersede its naïve form, are prescriptive ideals that aspire to be embodied as a state-of-affairs. All predictive science can be assimilated to prescription if we understand experiments to be a test of whether the world is as it ought to be if it is consistent with a given theory.

Incommensurable Formalizations.—Given that mathematics wears its mind on its sleeve, making its presuppositions explicit as axioms, how are the axioms to be understood in their turn? Gödel was among the few to perceive this problem, and he devoted his later life to the pursuit of principles underlying the axioms of set theory, rather than to a revision of the axioms themselves. Below the level of foundations there is a conceptual substructure that we scarcely know, and which is the basis of our understanding. These conceptual substructures could be called the regulatory principles mathematics. There are analogous principles in natural science. Indeed, with the natural sciences we have a number of explicitly formulated regulatory principles—the principle of parsimony (Ockham’s razor), the uniformity of nature, thermodynamics—many of them of long philosophical provenance. Cosmology is particularly rich with regulatory principles, such as the cosmological principle, the anthropic principle, the Copernican principle, and the principle of mediocrity. Such principles regulate our reasoning without being directly implicated in the derivation of particular results. These principles, even if disputed, are as familiar to us as the regulatory principles of mathematical thought are unfamiliar to us. It is as though natural science skipped over the stage of axiomatization and went directly to the principles underlying the axioms—if only the axioms had been formulated in the first place. This asymmetry between natural science and mathematics gives each discipline a fundamentally different relationship to formalization, and, as Hilbert noted, “Every kind of science, if it has only reached a certain degree of maturity, automatically becomes a part of mathematics.” What he meant is that a mature science is formalized, but what he did not say was that natural science and mathematics involve incommensurable forms of formalization.

Constraining History by Constraining Facts.—The instability of facts—that the world can be decomposed into facts in various different ways—is another sense in which history is infinite (in addition to the sense in which we can construct an infinitude of formal facts about the past). As the natural numbers can be decomposed into more subsets than there are natural numbers, so too the events of history can be decomposed into innumerable facts, and these facts can be assembled into more histories than there are events in history. That no type theory was ever imposed upon facts, attempting to arrange them hierarchically according to their complexity or extent, is a fundamental ambiguity of science, though an understandable ambiguity in at least a couple of ways. It is understandable insofar as rectifying this ambiguity would likely undercut the results of science in a way much like the use of a constructive logic undercuts much classical mathematics—and for similar reasons. Non-constructive thought, or what Torkel Franzén called classical eclecticism, gives a free hand in methodology, whereas all forms of constructivism—intuitionism, predicativism, finitism—involve some principled constraints on methodology, and a constraint on method will ultimately mean a constraint on results. A type theory for facts would constrain the results of science. And the absence of a type theory of facts is further understandable insofar as we don’t possess the formal framework necessary to enforce a hierarchy upon facts. All type theories have become unmanageably complex. The type theory of Principia Mathematica required work-arounds like the axiom of reducibility, which seem flagrantly unnatural. (Mathematicians don’t use type theory, they use ZF or some similar axiomatization.) Some other formalization of facts, or their elimination, seems to be in order.  

The Procrustean Bed of Logic.—Since the bulk of the problem of logic is not in the process of deduction itself, but rather lies in the formalization of the problem that precedes deduction, almost any deductive framework will serve equally well. Whether we employ Aristotelian syllogisms, Stoic propositional logic, medieval terminist logic, or contemporary mathematical logic, is largely indifferent. While our modern logic is more advanced in virtue of having incorporated into itself the logical discoveries of the past twenty-five hundred years, it is not the be-all and end-all of logic. The formalization of a problem to the point at which it can be made to fit the Procrustean bed of logic is instead where we should seek the embodiment of human reason, but that would be formalization seemingly unmoored to logic, and that would deliver us over to a kind of rational vertigo—a disequilibrium of the reason, apparently without a handhold to steady ourselves. But not quite. We formalize a body of knowledge with an eye to how exactly it can be funneled into the strictures of logic, so our choice of logic for our deduction is not indifferent in this sense. The logic we employ governs the formalization we employ, so it is our choice of logic that ought to be attended by a rational vertigo, but here we have the spirit of seriousness to guide us, which, in the case of logic, is not the self-deception of ready-made values, but rather the self-deception of ready-made calculi. Given the calculus, our problem has been preemptively defined for us, as has its formalization; we have already surrendered our logical autonomy in our implied consent to the mode of formalization entailed by our chosen logic.