About Logic interview with Giovanni Sambin

You can read notes on Martin-Löf's lecture given in Padua in 1980 here: Giovanni Sambin's notes on Per Martin-Löf's Intuitionistic Type Theory.

See Andy Pitts on Intensional Setoids for more on Minimal Foundations. 

My comment:

40:32 Thorsten "You only need the notion of a type... Then I can explain a proposition,..." I remember when you did that a few weeks ago, and you explained it, but did anybody actually understand your explanation? I know I didn't! 

And a reply:

 @CMDR_K3YN  The problem is more about how to interpret 'statements like "a predicate of booleans is a function from bool (Boole?) to prop" ' See also from 40:43 where it's a collection of all such functions. Then Giovanni says his his idea of foundations is from the ground up, starting with propositions and sets! I honestly don't know how anyone can have a sensible conversation on this basis! I thought the standard procedure was to establish a metalanguage first then discuss the object languages in that metalanguage, and if necessary, one can simplify the metalanguage and formalise the interpretation in terms of that same metalanguage but at a lower level. So I would expect to be able to do something much simpler than primitive propositions and primitive sets. I think Herbrand's insight was that that it is syntax all all the way down. Unfortunately he fell of a mountain before he could explain it any better.

30:38 On intensional and extensional theories and "running them in parallel". I wonder how far you could get by modelling functions with bijections between pairs, i.e. permutations on graphs. I did something like this once in the iterative construction I described in this post: Brady Haran interview with Terence Tao. It produced some very interesting constructions full of amazing symmetries. See also Category Theory May Actually be a Disease and Emma Tye on Martin-Löf Type Theory. What I did was construct something like a closure operator on an abstract algebra of natural transformations which automatically preserved congruences in the process. Unfortunately on February 15th, 2010 I lost all my work leading up to that and I still feel a bit sick when I think about it. 

See https://www.math.unipd.it/~sambin/ and his most recent book Positive Topology A New Practice in Constructive Mathematics:

In dynamic constructivism, mathematics is seen as the result of a dynamic process of interaction between the construction of mathematical entities, by abstraction and by idealization, and their selection according to their efficiency in applications to reality and in the organisation of mathematics itself.

The crucial benefit of this vision is its independence from dogmas and external authorities. A practical consequence is full respect for the diverse areas of mathematics - mainly computation, spatial intuition, deduction, and abstract axiomatic method - without reducing one to another. As a second consequence, a dynamic interaction between different 'epistemological levels' is always active and present, in the development of mathematics in practice, the study of its foundations and its formalisation in a computer language.

Subscribe to About Logic.