Foundations 5: Intuitionistic Logic and Type Theory
ฝัง
- เผยแพร่เมื่อ 9 ม.ค. 2021
- In this series we develop an understanding of the modern foundations of pure mathematics, starting from first principles. We start with intuitive ideas about set theory, and introduce notions from category theory, logic and type theory, until we are in a position to understand dependent type theory, and in particular, homotopy type theory, which promises to replace set theory as the foundation of modern mathematics. We also take an interest in computer science, and how to write computer programming languages to formalize mathematics.
In this video we introduce a type theoretic description of Heying algebras/ intuitionistic logic. We prove a few important results about intuitionistic logic, and then informally introduce some more ideas from type theory.
![[Intro to HoTT - OLD] Martin-Löf Type Theory: Speaking the Language](http://i.ytimg.com/vi/TeY5niDR8yE/mqdefault.jpg)
U have no idea how fucking excited I get when u upload
This is great! I was just looking for something to help me get a grasp on the book Modal Homotopy Type Theory, and it looks like this was uploaded less than 10 minutes ago!
48:50 - "I wish this was taught more in school"
I absolutely agree. Students who can abstract well enough can see the patterns, but not every student is willing to put the mental energy into understanding things if there isn't an interesting way to synthesize why one would do that math.
You are great!!!
What's less than itself?
Cyclic group elements, or cyclic probabilities?
An abstract polytopes -1 dimensional "null face"?
The surreal between 0 and 0?
Maybe infinite stuff, but I guess not.
I'm not aware of any definition of an existant thing, or 'less' where a thing is less than itself. If I said that about something in this video, it was probably a slip of the tounge and I meant to say 'less than or equal'. In a poset, any existing object x is equal to x, and also x is less than or equal to itself. I think the key point is that (at least in every sphere of mathematics I am aware of) a thing is always equal to itself.
@@RichardSouthwell "less than or equal to itself", but never less than itself. 🤷🏻♂️ So this reduces to just equal to itself.
I don’t think there is any inherent problem in defining something such that a thing is less than itself. We could for example say that x
Question:
Do you need to go through all the other levels of mathematics before doing this kind of maths?
I get this feeling that mathematics is really about exploring which subjects align with you and you can just learn it.
You can't do set theory freshman year or at a community college until you get prerequisites out the way.
Set theory and the trifecta you laid out seems intuitive to me.
I see it like mountaineering. Some subjects like euclidean geometry or elementary number theory can be tackled with no prerequisites. Other subjects like differential geometry are peaks that one needs tools from abstract algebra and calculus to climb. Others like category theory probably require excercise in handling abstractions. I think one has to find the right balance between what's easy/enjoyable and what's pragmatic and what suits their long term learning goals
@@RichardSouthwell Makes sense; thank you. I'll probably go the geometry route.
Yo mate. Honestly, you do not need to know formal ideas from logic or set theory in order to start doing 'serious' mathematics either. You need to know Zorn's Lemma I suppose, and maybe not have an aneurism when someone invokes the axiom of choice or one of its many, many equivalents. A lot of motivation for this sort of thing does come from ordinary pure mathematics of course though, so it can be helpful to know a little bit about that stuff. It absolutely is conceivable that someone could learn things like what a topos is without first knowing much commutative algebra/algebraic geometry, or (modern) differential geometry. You probably should be comfortable with the idea of a manifold or at least a topological space beforehand however. Not so much because you ABSOLUTELY need to that stuff to start understanding these ideas, but because that is where these ideas come from, and it is much easier to understand them once you have done more concrete work.
Where can I learn more about Intuitional Logic from someone who doesn't have a deep formal mathematical knowledge but wants to learn. Also what benefits could be applied for someone interested in programming?
Haha, so topos goes into this kind of stuff. Interesting. Learning as I go.
How does negation fit into all of this?
negation of x = not x = x implies false = x implies 0 = 0^x
@@RichardSouthwell so then also "x
@@warwolt 3 out of 4 de Morgan laws hold math.stackexchange.com/questions/120187/do-de-morgans-laws-hold-in-propositional-intuitionistic-logic
Is this about right?
∧ is a × and an ᴀɴᴅ that works between categories?
Where y ∈ {false, true, n | 0 ≤ n ≤ 1} then y^x ∧ x ≤ y.
bread meat bread = sandwich
bread square = sandwich
magic disappearing wedge of meat?
just needs lattice