In this video we introduce the Mitchell-Benabou Language. Also known as the internal language of a topos. This language allows use to manipulate statements that look like those from set theory and logic, while actually talking about the much more general case of topos theory and topos logic (and topos logic basically looks like intuitionistic logic). In this video we introduce the formal rules behind the Mitchell-Benabou Language. We start by looking at the rules for building terms and interpreting them in the topos. We explain how terms with a type equal to the subobject classifier (formulas) have `extensions' corresponding to the subobjects they classify, and we explain how notation like that of lambda calculus can be used to discuss arrows involving exponential objects. We also discuss term interpretation. Next we apply the Mitchell-Benabou Language to topos logic. We explain how we can use the Mitchell-Benabou Language to say a formula is true, or to say that one formula implies another. We also discuss the idea of sequents (which are claims that formulas imply other formulas), and discuss how we denote chains of implication starting from a given sequent. We use this notation to describe the different term manipulation rules which are sound and complete for topos logic, and justify the rules using our understanding of topos theory. We also go through examples of proofs of statements in topos logic using the manipulation rules we have obtained within the Mitchell-Benabou Language.
Here are some videos including further proofs and discussions about particular topics:
Implications of implication 1
• Implications of implic...
Understanding False and Not
• Understanding False an...
Universal Quantification Proof
• Universal Quantificati...
False in the Mitchell-Benabou Language
• False in the Mitchell-...
Not in the Mitchell-Benabou Language
• Not in the Mitchell-Be...
The proof of Theorem 13.6 (about implication) can be found in this video:
Mclarty Topos Basics 1
• Mclarty Topos Basics 1
More information about how "there exists" works can be found here
Existential quantifier interpretation
• Existential quantifier...
The following videos give important practice in using the Mitchell-Benabou Language to formulate important notions:
Completing Equalizers with MBL
• Completing Equalizers ...
Finding all subobjects containing something
• Finding all subobjects...
Proof that the MBL OR rule works
• Proof that the MBL OR ...
Proof that the MBL EXISTS rule works
• Proof that the MBL EXI...
A proof of Theorem 13.9 can be found here
"Universal Quantification Proof"
• Universal Quantificati...
Substitution Lemma argument
• Substitution Lemma arg...
Substitution rule proof
• Substitution rule proof
Substitution and equality
• Substitution and equality
Substitution and equality 2
• Substitution and equal...
Equality, biconditionality, reasoning
• Equality, biconditiona...
(a or b) and (not a) implies b
• (a or b) and (not a) i...
Singleton and comprehension axioms
• Singleton and comprehe...
Axiom of extensionality proof
• Axiom of extensionalit...
Product axioms
• Product axioms
Correction at 6:06:39
The purple expression at the far bottom left should be the extension of (exists y.Y) phi [rather than just being the extension of phi].
Lots of good applications of MBL are in the following series on "From the MBL to the topos"
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
• From the MBL to the to...
coequalizer documents and videos
drive.google.c...
• Coequalizers for struc...
• Coequalizers for struc...
• Coequalizers for struc...
• Coequalizers for struc...
Power objects and equivalence relations
• Power objects and equi...
Негізгі бет Category Theory For Beginners: Internal Language of a Topos (Mitchell-Bénabou Language)
Пікірлер: 8