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
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)
Theory
In model theory a 'theory' is a set of first-order sentences, for instance:
x
y
z.(x+(y+z)=(x+y)+z)
x.(x+0=x)
x.(x+(−x)=0)
x
y.(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:
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 ![]()
|
![]() |
Logical operations are implemented by universal constructions on subobjects.
|
|
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
x1,x2,x3...xn -> Ω
Mitchell-Bénabou Language
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:
there is <s1,s2> of type A×B. |
I4 | |
T5 | I5 |