Two Lectures on Constructive

Mathematics

(page 2) This is how the extraction of (functional) programs of dependent types (Also called "propositions as types" or "Curry-Howard isomorphism" or "proofs as programs") is done in Agda, Coq and Nuprl proof assistants :

 

x : A ---> B(x) from intuitionistic proofs of propositions of the form forAll x : A . ThereExist y : B(x) . R(x,y).

 

(page 7) This lecture by Robert Constable, is one of few resources that I have seen that firstly understood Brouwer's intuitionistic logic and then convey it together with illuminating other related ideas in the history of type theory, calculus of constructions and combinators etc.

 

**in this section and later, I need to elaborate on connections of Brouwer's ideas of type-ability, mental constructions, acts of intuition, to the present description of function as an operation or mental construction or "mental operation" that transforms elements of type A into elements of type B.

 

I like my "conceptual equivalences" of Martin Lof's Universes as Contexts OR Environments OR somehow an "upper type"/"large type"/"foundational type"/"mother type"/Or type "a thing" (in Ontology Engineering).

 

 

(page 13) I think a better way to express the common idea behind Russell's notion of type as "the range of significance of a proposition" and Gottlob Frege's "sense of a proposition", is that both of them are deeply concerned with the ultimate goal of Logic & Mathematics, that is, to disambiguate the natural language from all (kind) and sources of disambiguations. Of-course after that step, It is no longer be called a natural language but a formal language of a "mathematical logic" kind, that is as general and abstract as classical mathematics, but also is "computationally meaningful" or in the terms of Brouwer, Heyting, Kleene and Kolmogorov, it is a "Constructive Mathematics" that is also called "intuitionistic". These properties as mentioned, namely, Generality and Abstractness of classical mathematics together with computational meaning and power that has been evolved by intuitionistic methods to be correct and (complete?) and at the same time consistent, will be a foundational base for both mathematics and computer science and its practice into important technologies for our (and future of) the civilisation. The proposed formalism is and will be a Constructive Type Theory of Per Martin Lof intuitionistic type theory with Vladimir Voevodski's Axiom of Univalence or a weaker version called "Cubical type theory".

 

Returning to Russell and Frege and even before that of Kant, and after them of the great Brouwer and his student Heyting and also other great minds like (Not to name all of them) but, Alfred North Whitehead, Schonfinkel, (Less known) Frank Ramsey, Hasskell Curry, Alonso Church, Alane Turing, Kurt Godel, Kleene, Nikolaas de Bruijn, also John von Neuman, Heyting's student Kolmogorov, and many more. This line can be stretched well to 2021 that I'm writing these notes. But there were a relative quiet time between roughly 1940 to late 1960s. After that we have many many workers in the area of Lambda Calculus (also Combinatorics), versions of constructive set theories and also importantly in the Category theory, Functional programming in general and topics and areas like Game Semantics, Domain Theory and more. Some of the names after this re-emergence of the discipline are, Dana Scott, Per Martin Lof, Gerard, Corrado Bohm, Mac Carthy, Fitch and many many more. I tend to think, the ultimate goal of these foundational works, in a fundamental sense, have been to establish "A theory of Meaning" -- To create or agree on meaning, to preserve meaning and at the same time add or combine meaning to create new meaning and all of them must be transformable to other levels of abstractions (of interoperatable languages and domain specific languages), plus one physical condition that they must be transmitable, storable by physical technologies available (or available in the future).

 

(page 13) "computations" was there from the beginning when Brouwer constructed his intuitionistic foundations of mathematics and logic. He even, by his special intuitive personality and pessimistic attitude (by observations of his few friends and disciples), predicted precisely our computational world and the fact that every aspect of our lives are influenced by for example "software as everything" or software instead of everything that consequently translates into saying that everything now (and increasing in the future) will be controlled by programs (proofs) and mathematical algorithms behind them, something that not understandable by ordinary man, in fact and in the words of philosopher of technology ... ordinary man has no choice to accept it almost as a mystical phenomenon and a fact of his world. Hence the world will be ruled by algorithms that only very few understand in totality with surrounding technologies that support its very long chain. I think its fair to say no one will be able to understand the whole thing, a gigantic network of technologies together with supporting industries (in multitudes of levels) and every bit has its own vast academic discipline (that support related industry that enables that specific part of computationally enabled chain of activities). In this sense, as Robert Constable says, computer science appears as a complete Meta-Science that augments and empower everything else.

 

One other important point is, in "mental constructions" conception of Brouwer that, there is one element that most of workers in this area tend to overlook; that is the "element of time" or sequentiality of events (steps, instructions and thoughts constructs) that "is" the "time" concept.

 

Hossein M. Bojnordi

 

 

References:

Primary -- Robert L. Constable, Two Lectures on Constructive Type Theory, 2015.

Other --

-S.C. Kleene. On the interpretation of intuitionistic number theory. Journal of Symbolic Logic, 10:109–124, 1945.

-Stuart F. Allen, Robert L. Constable, and Lori Lorigo. Using formal reference to enhance authority and integrity in online mathematical texts. Journal of Electronic Publishing, 2006.

-Per Martin-Lof. An intuitionistic theory of types: Predicative part. In Logic Colloquium 73, pages 73–118. North-Holland, Amsterdam, 1973.