spent some leisure time writing a useful reference page

[juan_gandhi]

https://github.com/vpatryshev/wowiki/wiki/Logic-of-Elementary-Topos 

Comments

[sassa_nf]

Can you add something about Χ_f? It is clear from the examples it is not an arbitrary arrow B→Ω.

Well, ok, maybe this is a stupid question. Of course, it's just an arrow that makes the square commute.

[juan_gandhi]

What is Χ_f? Could not find it anywhere. (I feel I'll have to add quantifiers, eventually).

[sassa_nf]

Chi_f in the diagram for the definition.

[juan_gandhi]

Yep; thanks; added a line.

[epimorphisms_split]

картинки маленькие, можно увеличить раза в два.

[juan_gandhi]

Эх; надо бы, да. Там проблема у меня, что кегль я беру более менее стандартный, когда png изготовляю. Надо поправить будет, да.

[sassa_nf]

Also, is the arrow Ω₁→Ω⨯Ω labelled (true,true) correctly?

[juan_gandhi]

Oh, right; thanks!

[sassa_nf]

Is the introduction of Union of Subobjects necessary to define disjunction? Can we not use ∨: Ω⨯Ω→Ω = ⇒ . (¬⨯id)?

[juan_gandhi]

Good question about disjunction; let me think. Most probably not, but I have to come up with an example... probably, the ternary logic could be enough.

[juan_gandhi]

So, you could as well take ¬(¬A∧¬B), like Miles Sabin did, introducing union types in Scala. Does not work though, it produces something like a double negation. In your case, instead of A∨false, we will have ¬¬A.

[sassa_nf]

I am not sure what the problem with double-negation is, if everything is reduced to true/false anyway.

[juan_gandhi]

Of course not; it depends on the logic we are dealing with. Intuitionism. Double negation does not necessarily hold.

[sassa_nf]

Hmmm.... I thought Ω was an object with just two points.

But then if Ω can have more than two points in some logic, then the definition of ∧ does not seem complete, because it doesn't explain how to choose mappings other than (true,true)→true.

If it's only two points in Ω, there is no choice; but if it's more points, then the specified definition doesn't seem to make ∧ a unique arrow.

[juan_gandhi]

Oh no. Take Set×Set - this boolean topos has 4 points already.
Regarding conjunction, it classifies (true, true) inclusion to Ω. In Grothendieck topologies, classifying maps are built by Yoneda lemma.

[sassa_nf]

ok, but what about Heyting algebra. Does this mean Ω = {a, b, T, ⊥} ? How does ∧ know what a ∧ b is, since only T∧T is specified?

[juan_gandhi]

Ok, say, we have a four-point Ω (and ignore stuff that are not points).

We can have a variety of logics.

First, 4-valued booleans. a = (0,1), b=(1,0), T = (1,1), ⊥=(0,0), and operations are defined bitwise.

Second, numbers ⊥=0, a=1/3, b=2/3, T = 1. This linear order is a bounded distributive lattice, so everything is well-defined, conjunction is just minimum. Trying to find another four-point logic...

[sassa_nf]

Heyting algebra: a lattice of ⊥ < a < T and ⊥ < b < T. Then x ∧ y = max({c for c in Ω and c ≤ a and c ≤ b}).

But my question is how does the definition reflect this fact? It seems to only say that T ∧ T = T - nothing about a ∧ b = ⊥, and not, say, a ∧ b = a.

[juan_gandhi]

Well, because the definition comes from the classifying arrow, and this classifying arrow depends on how the topos works. If we have Set^2, that's one thing; if we have Set^[0,1,2,3], it's the other thing. In both cases Ω has 4 points.

[sassa_nf]

Sure.

Maybe I don't get something basic. What it looks like to me, since the square has arrows (true,true) and true, it defines only the behaviour of the classifying arrow for one pair, not all possible pairs.

[juan_gandhi]

Right. It classifies just one point, (true, true). But it's defined on the whole ΩxΩ. How is it defined? It maps every (generalized) arrow T → ΩxΩ to a value in Ω, and it evaluates how close is this arrow to (true, true).