About Logic - Analytic and Synthetic Mathematics

See About Logic Interview with Emily Riehl and Marie Durrieu - Bourbaki n’est pas un homme, ...

My comments:

11:55 I think there is evidence in Euclid's Elements that there was an analytic process which preceded the synthetic theory he presented. Aristotle makes this explicit where he talks about the process of division as making the demonstrations obvious. He mentions in particular the proof of proposition 32 "In any triangle, if one of the sides is produced, then the exterior angle equals the sum of the two interior and opposite angles, and the sum of the three interior angles of the triangle equals two right angles." This came from considering lines falling across two parallel lines and is very closely connected with the formulation of the parallel postulate. There are other places where you can clearly see that several propositions are all derived from one drawing which then reappears as you connect the separate propositions together. I don't have my notes with me right now so I can't tell you where I saw this, but I am quite sure it's not just an isolated case, and anybody who looks for this will see what I mean. One then can wonder where this analysis started,...

37:28 I don't know if he lied about this, but there are people who claim to be able to prove P v not P from the axiom of separation and the axiom of regularity, so in plain ZF. I think the implication is that in some sense the axioms of ZF with an underlying intuitionistic logic are inconsistent or at least unsound. The IZF/CZF theories use something called ∈-induction which with LEM allows you to prove regularity, so you recover ZF. The situation with AC is more subtle. The details are in the StackExchange post "ZF Set Theory and Law of the Excluded Middle". What I would like to understand are how so-called structural rules in Natural Deduction systems, rules like weakening and contraction, are incompatible with intuitionistic logic. I think it's because of the way the deduction theorem is defined, but in some systems (Church's Formulation of the Simple Theory of Types for example) the deduction theorem is a meta theorem, not a theorem you can prove in the logic itself. 

Subscribe to About Logic.

Later I got this this talk Synthetic mathematics with an excursion into computability theory by Andrej Bauer in the YouTube recommendations (on this other talk):

Subscribe to Andrej Bauer.

See also Some Talks About Type Theory and Languages and Andrej Bauer - Models of intuitionism and computability.

Comments

Post a Comment

Popular posts from this blog

Steven Johnson - So You Think You Know How to Take Derivatives?

Image
A derivative is linearisation, and differential calculus is essentially linear algebra, ...  See  Freya Holmér - Why Can't You Multiply Vectors?  and  Freya Holmér on Continuity of Splines . See also the MIT OCW page:  Matrix Calculus For Machine Learning And Beyond  (Alan Edelman, Steven G. Johnson) Subscribe to The Julia Programming Language . Alan Edelman talking about expressing mathematics as computer code. The idea is that you can use computer languages to communicate mathematical ideas precisely to other people. See my comments about functional programming languages here:  https://prooftoys.org/ian-grant/hm/ Subscribe to TEDx Talks .
Read more

FUTO FUBS

Image
I think this is the first time they've actually publicly announced anything about this project. See these posts: Eron Woolf on Why Open Source is Failing Matt Mikhailov and Vincent McKibbon on The Problem with Open Hardware Jason Kridner talking About BeagleBoard.org and Software Development .  See these places:  https://danielc.dev/rk/ https://github.com/petabyt/rk https://github.com/futo-org/ret See also  https://pine64.org/devices/pinebook_pro/ . Subscribe to  FUTO .  See  https://github.com/nir9/low-level-learning-resources/tree/master/setups/debian . Subscribe to  Nir Lichtman .  If you're looking for a cool init process, try  https://ctx.graphics/terminal/ . See  Artful Bytes - When to Use a RTOS  and  How to Create a Successful Open Source Project . 
Read more

Tensor Fields and Simplicial Complexes

Image
Listening to Freya Holmér last night I started to get glimmers of an idea I had long ago about how to represent vector spaces in computational processes using this recursive abstract type :  abstype 'a point = POINT   of {getx :  'a vector,       diff :  'a point -> 'a point,       move :  'a point -> 'a point,       scale : 'a -> 'a point,       proj :  'a point -> 'a} with    fun new i (op +) (op -) (op * ) dot =    let fun self x =  POINT       {getx = x,        move = fn (POINT pr) =>           (self (x + (#getx pr))),        diff = fn (POINT pr) =>          self (x - (#getx pr)),        scale = fn i =>          (self (x * i)),        proj = fn (POINT pr) =>     ...
Read more