Maths - Internal Language of a Topos

A subobject classifier is an arrow from 1 (terminal object) to Ω.

This is an extension. It can be thought of like a comprhension where the variables are before the '|' and the classifier (which specifies a sub-object) is after it.

[x.X | χq(x) /\ χr(x) ]
[x.X,y.Y | χq(x) /\ χr(y) ]

Model Theory

• see model theory on page here.
• see universal algebra on page here.

All the flavours of model theory rest on one fundamental notion, and that is the notion of a formula φ being true under an interpretation I. (Wilfrid Hodges)

• wikipedia
• stanford

Theory

In model theory a 'theory' is a set of first-order sentences, for instance:

• xyz.(x+(y+z)=(x+y)+z)
• x.(x+0=x)
• x.(x+(−x)=0)
• xy.(x+y=y+x)

Model of Theory

There can be multiple models of any given theory

Interpretation

The variables are given values which make the sentances true.

Define a structure B using structure A.

 

Internal Logic

See ncatlab:

• internal logic
• internalization
• Model theory

large parts of mathematics can be internalized in any category with sufficient structure

The idea is to exploit the fact that all mathematics can be written in the language of logic, and seek a way to internalize logic in a category with sufficient structure.

The basic ideas of the internal logic induced by a given category C are:

The objects A of C are regarded as collections of things of a given type A:
The morphisms A->B of C are regarded as terms of type B containing a free variable of type A (i.e. in a context x:A)
A subobject A is regarded as a proposition (predicate): by thinking of it as the sub-collection of all those things of type A for which the statement φ is true the maximal subobject is hence the proposition that is always true; this is the logical object of truth A the minimal subobject is hence the proposition that is always false; this is the logical object of falsity A one proposition implies another if as subobjects of A they are connected by a morphism in the poset of subobjects: φ=>ψ means ψ
Logical operations are implemented by universal constructions on subobjects. the conjunction and is the product of subobjects (their meet) the conjunction or is the coproduct of subobjects (their join)
A dependent type over an object A of C may be interpreted as a morphism B->A whose “fibers” represent the types B(x)for x:A. This morphism might be restricted to be a display map or a fibration.

 

Alternative Version of Expression

variables -> truth value

x₁,x₂,x₃...x_n -> Ω

Mitchell-Bénabou Language

see ncatlab

A simple form of the internal language of an elementary topos E. It makes use of the fact that in the presence of a subobject classifier Ω, there is no need to treat formulas separately from terms, since a formula or proposition can be identified with a term of type Ω.

Term		Interpretation
T1	Variables free or bound	I1	Variable xi in list x=(x1,x2,x3...xn)
T2	Arrow f: x->y	I2
T3	Constant c: 1->a	I3
T4	Product For a term: s1 of type A s2 of type B there is <s1,s2> of type A×B.	I4
T5		I5

 

 

EuclideanSpace

home

Prerequisites

Topoi are introduced on the page here.

Related Subjects

• Cubical Type Theory

Venn Diagrams

Some of us, of a certain age, can remember something called 'new maths' introduced at school. This was an idea to introduce set theory at an early stage (I hope they still do it). An important part of this was Venn diagrams, they give a very intuitive way to look at sets and their intersections and unions. For me an important part of this is the way it demonstrates a deep and beautiful link between sets (union, intersection), logic (and, or) and topology.