Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: Bi-Heyting algebras

John Baez (Mar 31 2020 at 06:31):

This is an interesting quick intro to bi-Heyting algebras and "bi-intuitionistic logic":

• A clean introduction to logic (intuitionist, bi-intutiutionist, classical).

It has a good name for the new connective that shows up when there's a left adjoint to disjunction: "unless".

Mike Shulman (Mar 31 2020 at 13:33):

I don't like "unless" for the left adjoint of disjunction. The most direct logical interpretation of "P unless Q" is $\neg Q \to P$ (or $\neg P \to Q$), which in classical logic is equivalent to $P\vee Q$ itself, not to its left adjoint. In classical logic the left adjoint of disjunction is "and not", which is very different from "unless".

(BTW, in intuitionistic logic $\neg Q \to P$ and $\neg P \to Q$ are not equivalent to each other or to $P\vee Q$, but in linear logic $\neg Q \multimap P$ and $\neg P \multimap Q$ are equivalent to each other and to the multiplicative disjunction $$P\parr Q$$. So "unless" is actually a good name for $$\parr$$. I learned this from Toby Bartels.)

Dan Doel (Mar 31 2020 at 13:51):

Oh, that's nice. I was thinking a while back that explaining par as being more like 'exclusive or' might make some sense, but it's not great as a name, and 'unless' is a nicer way of connoting the same sort of thing.

Dan Doel (Mar 31 2020 at 13:58):

It might just be a better name for 'exclusive or,' too. :)

Mike Shulman (Mar 31 2020 at 15:29):

I don't think "unless" has an exclusivity connotation. Toby did have a nice suggestion of "exclusive and" for the additive conjunction though!

Henry Story (Apr 10 2020 at 19:02):

This 2016 article "Structuring Co-Constructive Logic for Proofs and Refutations" is related to the topic of Bi-Heyting Algebras.
James Trafford argues that by combining constructive and co-constructive logics (by relating but not identifying a topos and a complement-topos), one can get to an model of a dialogue between proofs and refutations.
Some interesting concepts that come up are duals to Topoi and co-exponentials.

The author is very good at combining the logic and the philosophical sides which helps me at least understand what is at stake. His book "Meaning in Dialogue" has a huge list of references on the debate on that topic.

1. In a footnote James Trafford points out that the reviewers suggested that the phrase "bi-intuitionistic logic" may have been more appropriate.
2. In an older paper from 2015 Co-Constructive Proofs and Refutations he actually makes the parallel with bi-Heyting algebras. (he does here too, indeed he defines both heating and co-heyting algebras)

Henry Story (Apr 11 2020 at 14:36):

I guess nobody here was mislead, but Trafford does cite a few important papers and books that assume that the internal logic of any elementary topos is intuitionistic. Whereas one can have paraconsistent topoi too, he argues here https://twitter.com/bblfish/status/1248981894408044546

@DavidCorfield8 That it is possible to construct a topos whose internal logic is paraconsistent is indeed what surprised me! https://link.springer.com/article/10.1007/s11787-016-0138-z https://twitter.com/bblfish/status/1248981894408044546/photo/1

- The 🐟‍‍ BabelFish (@bblfish)

John Baez (Apr 11 2020 at 16:48):

From a brief glance at the abstract it looks like this paper just does a sort of obvious thing: turn the topos upside down.

Matteo Capucci (he/him) (Apr 11 2020 at 18:01):

Uh that's cool!

Henry Story (Apr 11 2020 at 18:10):

John Baez said:

From a brief glance at the abstract it looks like this paper just does a sort of obvious thing: turn the topos upside down.

As a amateur, from a distance, I would have expected one gets the same thing back if one turned it upside down. (I guess I was thinking of a lattice)
Dualities are weird: You turn algebras upside down and you get logics of states and observation (OO programming) and modal logic instead of equations. Here it looks like one turns Topos upside down and one gets a Popperian constructive logic of falsification (see Dual Intuitionistic Logic and a Variety of Negations: The Logic of Scientific Research. Or when combining the two one gets a way of explaining dialogical logic of proofs and refutations.
It's a helpful mind bender.

John Baez (Apr 11 2020 at 18:54):

Henry Story said:

As a amateur, from a distance, I would have expected one gets the same thing back if one turned it upside down.

The whole point of intuitionistic logic is that it doesn't look the same turned upside down! Negation does not give an isomorphism between a Heyting algebra, and its opposite, the way it is for a Boolean algebra. In other words, if you draw a Heyting algebra and turn the picture upside down, what you get is not usually a picture of a Heyting algebra. But if you do this to a Boolean algebra, you get a Boolean algebra, and in fact an identical-looking Boolean algebra.

What does this mean? It means that in classical logic saying "X is true" is exactly the same as saying "$\neg P$ is false". But intuitionistic logic these are different.

John Baez (Apr 11 2020 at 18:56):

If you turn a Heyting algebra upside down, you get a co-Heyting algebra. This describes a kind of paraconsistent logic.

Henry Story (Apr 12 2020 at 05:59):

Indeed I just finished Trafford's article.
The argument from Dual Intuitionistic Logic and a Variety of Negations: The Logic of Scientific Research by Shramko argues convincingly that intuitionism is the logic of mathematics because well maths is constructive. There is no Platonic heaven where one can go to look at the forms of mathematics. All one has is proofs. (one may wonder about geometry though, which was the mathematics Plato actually thought of). On the other hand experimental science as argued by Popper can build theories, but only disprove them. So Shramko argues that a falsificationist logic is what is needed, and that is he argues what paraconsistent logic found in co-Heyting algebras gives one.
Trafford goes into more detail as to what a proof is drawing on the founders of intuitionistic logic. In mathematics a proof is a process that leads from a conjecture to a theorem. (I hope I am using the right words) The act of building a proof and showing that it does not collapse into false ⊥, is what gives it the status of a theorem. If a proof collapses into ⊥ then one has not disproved what one set out to prove, as there may be another proof of the conjecture which works. Hence we don't have ¬¬p = p.
If one tries to find a logic that is both intuitionistic and paraconsistent one gets classical logic.
Trafford wants to apply the ideas of conjecture and theorems from intuitionistic logic to the constructive refutation space: one can by symmetry distinguish conjectures and theorems: which would be those that don't end up at ⊤ ← p, because from there one could refute anything.
He then shows how one could do proofs in a Topos and refutations a complement Topos and bring the final theorems together in a boolean logic Topos which combines elements from both.

I don't see in these papers a worked out example with real life use cases. This should be feasible here... What kind of propositions should appear on each side? If one does not have a way to falsify mathematical statements, then these could only be proved on the constructive side. I guess empirical statements would be worked out in the refutation logic side. The ~ operator allows one to bring statements from one side to the other. So mathematical theorems (proved conjectures) can be brought to the refutation logic side as statements that can never be refuted. Similarly a statement that can clearly be refuted can be given in the constructive side as statements that are false.

But I am looking for more detailed working out of this as a game.

The book Immanent Reasoning or Equality in Action gives a very clearly worked out game semantics for Constructive Type Theory with dependent types, which requires thinking of two players: one putting forward a thesis and the other trying to disprove it. But it does not give an interesting example of proofs of material statements (empirical ones), even though it discusses those. (The authors have read Trafford's work that appeared a year or so before, and discuss elements of it).

Henry Story (Apr 12 2020 at 05:59):

it would be interesting to understand what other uses for co-Heyting algebras there are.

Henry Story (Apr 12 2020 at 09:26):

I asked a question on Stack Exchange regarding co-exponentials which appear in complement Topoi, as I would like to get my head around them.
https://math.stackexchange.com/questions/3621660/example-of-co-exponential

Matteo Capucci (he/him) (Apr 12 2020 at 10:30):

This is very illuminating: theorems are not disproved by failed proofs, and theories are not confirmed by successful experiments. It puts math and science in a cool duality.
It'd be nice to see if one could combine probability and paraconsistent logic to get a 'falsifiability calculus' which lets you reason quantitatively about experiments

Morgan Rogers (he/him) (Apr 12 2020 at 10:34):

Given that the success of experiments is measured using statistics, one would hope that such a theory shouldn't be too complicated to build.

Henry Story (Apr 12 2020 at 18:34):

In Meaning in Dialogue there is an interesting comment on type theory which should be relevant to HoTT and that continues the discussion above on Bi-Heyting algebras relationship to falsificationism. I can't evaluate it for myself, but the thought that one may want to complement proof objects for types with refutation objects is in any case very interesting. P 159 of Meaning in Action

Dan Doel (Apr 12 2020 at 18:44):

Something like that is developed pretty thoroughly in Compiling with Classical Connectives. It has calculi with all the dual connectives of linear logic, but it's not actually linear (I think). Instead the duality corresponds to 'polarity' and instead of exponentials that weaken the structural rules, there are polarity shifts that mediate between evaluation strategies.

Dan Doel (Apr 12 2020 at 18:46):

I don't know if 'refutation objects' are the best way to think about the duals in that setting, though.

Dan Doel (Apr 12 2020 at 18:56):

I've been wondering if some adaptation of this would be a more appropriate than linear logic for an application like in Linear Logic for Constructive Mathematics. It seemed like that wasn't strictly interested in linearity (since the chu construction given supports a bunch of extra rules more like affine logic), but in having a richer set of connectives to make sense of stronger notions of refutation.

Henry Story (Apr 12 2020 at 19:23):

Trafford has some critique of Linear Logic in Meaning in Action (to do with some lack of symmetry), but to understand it I think one really needs to understand his book (which I have not finished) and also have a good understanding of Linear Logic.

Henry Story (Apr 13 2020 at 07:47):

Argh! In Meaning and Dialogue p165 onwards Trafford first gives a definition of a subject classifier, then of a Topos, then later p.167 of a Complement Classifier leading to a complement Topos. The definitions look identical (I can't tell if the differences are just different ways of saying the same thing). The distinction is not thematized at least. He refers to the article Complement-Topoi and Dual Intuitionistic Logic from 2010, which is very similar and also does not make the difference clear. The only difference is that in one case an arrow is labelled true and in the other false. But that is just a label right?

Henry Story (Apr 13 2020 at 08:14):

I get a feeling that one can only distinguish these two by comparing them. Something like this
1) arbitrarily choose a $true: 1 \to \Omega$ as your subobject classifier. Add that to your category with finite limits and colimits and exponentials and you get a Topos. From this you can the define $false: 1 \to \Omega$ as shown on a pullback from 0.
2) given 1) now choose $false: 1 \to \Omega$ from above, as your subobject classifier, which you now call a complement subobject classifier. Add that to your category with finite limits and colimits and exponentials and you get what you call a complement topos.
Since the choice of 1 is arbitrary, so is 2. So what is a topos and complement topos, depends on the initial choice.
A Complement Topos is thus indexical on the choice of the initial Topos.
Is that right or have I just misunderstood something?

Morgan Rogers (he/him) (Apr 13 2020 at 09:46):

The generic subobject $\top: 1 \to \Omega$ isn't arbitrary; it isn't just a label in general. It just happens that in the category of sets the subobject classifier is a Boolean algebra with only two elements, so you can complement it and get an isomorphic structure.

Morgan Rogers (he/him) (Apr 13 2020 at 09:53):

For example, take the natural numbers (including 0) with addition as a one-object category. Presheaves on this form a topos, and its subobject classifier is the object of ideals of $\mathbb{N}$, which are indexed by the natural numbers with an extra element added for the empty ideal, which I'll call $\infty$; the action of $\mathbb{N}$ on this set is, perhaps surprisingly by subtraction; the only fixed points are the ideal generated by $0$ and the empty ideal $\infty$.
Morphisms $1 \to \Omega$ are precisely fixed points; the former is $\top$ and the latter is $\bot$. I'll leave you to check that these are not interchangeable.

John Baez (Apr 13 2020 at 16:48):

arbitrarily choose a $true: 1 \to \Omega$ as your subobject classifier.

You can't "arbitrarily choose" true: $1 \to \Omega$" as your subobject classifier. A subobject classifier has to classify subobjects - see the definition. A category with finite limits either has a subobject classifier or it doesn't. If it does, this subobject classifier is unique (up to isomorphism). In short, you don't get to choose it.

Henry Story (Apr 13 2020 at 18:36):

Yes, my confusion came from only thinking of the category $Set$. There I could not see how the two elements of $\Omega$ could be distinguished other than artificially, let alone ordered. The ordering is explained in the 2015 paper From (paraconsistent) topos logic to Universal (topos) Logic. It also gives a few other topoï of which the graph topos. This article, cited by "Meaning in Dialogue" numerous times, looks at 5 widely accepted slogans on Topoï, and uses complement-topos to correct some excesses of them, as I understand (having just reached p10).

Nathanael Arkor (Apr 13 2020 at 18:40):

This is obviously off-topic, but @Henry Story: why the diaeresis on "topoi"?

Henry Story (Apr 13 2020 at 18:42):

I have heard someone famous say that topoï sounds a bit pompous, but I think it sounds a lot nicer than toposes, which makes anyone pronouncing them sound like they are slurring. :cant_talk: <- that's the best emoticon for slurring I could find.

Nathanael Arkor (Apr 13 2020 at 18:50):

I mean: why "topoï" and not "topoi"?

Reid Barton (Apr 13 2020 at 19:29):

topoï is the French spelling--otherwise it'd be pronouned like "to-pwah". In English the diaresis is a bit odd.

Joachim Kock (Apr 13 2020 at 19:36):

The funny thing is that the Greek plural is pronounced 'topi'! I don't think many category-theorist would be willing to follow that. (Personally I am happy with 'toposes'.)

John Baez (Apr 13 2020 at 19:46):

Henry Story said:

Yes, my confusion came from only thinking of the category $\mathsf{Set}$. There I could not see how the two elements of $\Omega$ could be distinguished other than artificially, let alone ordered.

Even in the category $\mathsf{Set}$ (like any other topos), the subobject classifier is determined uniquely (up to canonical isomorphism) by the fact that it is the subobject classifier. The subobject classifier is not just the object $\Omega$, it's that object and the morphism $\mathrm{true} : 1 \to \Omega$.

Furthermore the partial ordering on the subobject classifier is also determined.

John Baez (Apr 13 2020 at 19:49):

Of course it doesn't matter what you call the two elements of the subobject classifier $\Omega$ for $\mathsf{Set}$; that's what "up to canonical isomorphism" entails. We could call them "true" and "false", or switch their names and call them "false" and "true". But if I start using "false" to mean "true" and vice versa, you can easily discover that fact, e.g. by asking me "is $\pi \in \mathbb{R}$ a rational number"?

Henry Story (Apr 13 2020 at 19:54):

I guess the question in $\mathsf{Set}$ is does it matter which $f: 1 \to \Omega$ I choose? There are two such functions. Can they be distinguished? $\mathsf{Set}$ may be special here, which would explain my confusion.

John Baez (Apr 13 2020 at 19:58):

Since every function from a 1-element set to a 2-element set is uniquely isomorphic to any other function from any other 1-element set to any other 2-element set - they all "look alike" - any one of them can serve as a subobject classifier in $\mathsf{Set}$.

John Baez (Apr 13 2020 at 19:58):

Here I'm acting like you know what it means for two functions to be isomorphic.

John Baez (Apr 13 2020 at 20:01):

It may freak out beginners to hear someone say "two morphisms are isomorphic", but it makes sense because morphisms in a category are objects in that category's arrow category.

John Baez (Apr 13 2020 at 20:02):

So, we can talk about two functions being isomorphic, and what you're noticing is that all functions from 1-element sets to n-element sets are isomorphic. (Here I'm fixing n.)

John Baez (Apr 13 2020 at 20:03):

Not all functions from 2-element sets to n-element sets are isomorphic!

Henry Story (Apr 13 2020 at 20:05):

I need to look a bit away from $\mathsf{Set}$ towards something that is purely intuitionistic and purely co-intutionistic. It looks like topolology is one good place to look there. (I don't think I know much about topology, though I am quite at home with modal logic, which has I believe topological models).

John Baez (Apr 13 2020 at 20:06):

I think everybody thinks the topos of graphs is the simplest example to help people break free from their set-based intuitions.

John Baez (Apr 13 2020 at 20:06):

You can draw everything.

Henry Story (Apr 13 2020 at 20:07):

That should be for me too, as RDF is also all about graphs :-) I have 15 years experience using those. The semantic web then builds a Regular Logic out of them. (see Knowledge Representation in Bicategories of Relations). Though I think there the claim is that it is a subset of first order logic, so I guess the subobject classifier will also be classical.

John Baez (Apr 13 2020 at 20:17):

I don't know what you mean by "classical", but the subobject classifier for graph is not a boolean algebra. That's why it's good for breaking one of ones boolean habits.

John Baez (Apr 13 2020 at 20:25):

A vertex can just be "in" or "out" of a subgraph, but for edges it gets more interesting.

Henry Story (Apr 13 2020 at 20:28):

yes. I was trying to find where in my experience I had used graphs a lot. The Semantic Web talks of RDF Graphs. And those really can be expressed as $s,t: A \to V$, where $A$ are triples of $Nodes = URI | Literal$ such as $(subject,relation,object)$ and $V$ are nodes. $s$ choose the first element of the triple and $t$ last element.

Henry Story (Apr 13 2020 at 20:34):

It's just that the functorial semantics that is given for those, as expressed in the bicategories of relations article is a subset of first order logic, so I'd expect to find a subobject classifier that was boolean at that level.

Henry Story (Apr 13 2020 at 20:39):

But the other place I can draw on is programming with a functional language like Scala, which has a more complex deep structure, but the type system is usually explained as being constructive. Which is why the dual of a constructive logic is intriguing.

Henry Story (Apr 13 2020 at 20:47):

It made me wonder all the various forms of testing (e.g. unit testing) developed for a program are related to co-intuitionistic logic of falsification based on co-heyting algebras. (To bring this discussion back to the topic of this thread)

Henry Story (Apr 13 2020 at 21:40):

Nice title The Evil Twin: The Basics of Complement-Toposes published 2016.

Christian Williams (Apr 13 2020 at 21:44):

Sorry, but did someone give an intuition for how to think about the left adjoint to disjunction?

Henry Story (Apr 13 2020 at 21:51):

@Christian Williams
I asked a question on Stack-Exchange on co-implication, but I have no answers yet. I have not read the mail at the top of this thread yet, as I thought I should get some background first. Perhaps if I thought of this in terms of adjunctions it would be easier...

Christian Williams (Apr 13 2020 at 21:54):

Okay, yes I've been looking at it. I think after the phrase "<<adjoint>> relations" they start making $\subset$ more concrete.

Christian Williams (Apr 13 2020 at 21:57):

In the same way
you can construct $\supset$ as a supremum: a⊃b = ⋁{C:C∧a ≤ b},
you can construct $\subset$ as an infimum a⊂b = ⋀{C:a ≤ b∨C} .

Dan Doel (Apr 13 2020 at 21:58):

It probably depends on the setting. For instance in the Compiling with Classical Connectives I mentioned earlier, I think it might have that (I'd have to check) and it's related to the fact that there are two versions of negation in the system, corresponding to two different notions of what a continuation is.

One way of conceiving of a continuation is as a function that never returns, and that is built out of the right adjoint to conjunction. Another is that it is a captured stack frame, built out of several projections, and I think that is the one that would be left adjoint to disjunction.

Dan Doel (Apr 13 2020 at 21:58):

But that all might be meaningless to you, depending on your background. :)

Christian Williams (Apr 13 2020 at 22:00):

Yes, I'm sure depends on context, until you see enough to have a more broad perspective. What's a captured stack frame?

Dan Doel (Apr 13 2020 at 22:01):

I think the hand waving programming intuition is that it is a way of encoding an early exit path. because $A-E → B$ is the same as $A → E+B$, and the latter is a model of an exceptional return.

John Baez (Apr 13 2020 at 22:03):

All that stuff is meaningless to me, thanks to my background.

John Baez (Apr 13 2020 at 22:03):

This is a lot easier for me:

Christian Williams said:

In the same way
you can construct $\supset$ as a supremum: a⊃b = ⋁{C:C∧a ≤ b},
you can construct $\subset$ as an infimum a⊂b = ⋀{C:a ≤ b∨C} .

Christian Williams (Apr 13 2020 at 22:07):

They go into lots of examples later on that post, but it looks like they leave the working out $\subset$ to the reader.

John Baez (Apr 13 2020 at 22:07):

So let me think about the boolean algebra of subsets of a set: then a⊂b is the intersection of all sets $C$ such that $b \cup C$ contains $a$.

John Baez (Apr 13 2020 at 22:08):

So $C$ has to contain everything in $a$ that $b$ doesn't.

John Baez (Apr 13 2020 at 22:08):

And that's all it needs to contain.

Dan Doel (Apr 13 2020 at 22:08):

I think in a boolean algebra $A - B = A ∧ ¬B$.

John Baez (Apr 13 2020 at 22:08):

So that's what it is: it's $a$ intersect the complement of $b$.

John Baez (Apr 13 2020 at 22:09):

Yeah, like Dan just said. But I derived it. :upside_down:

Christian Williams (Apr 13 2020 at 22:10):

Ah, of course. Thanks.

John Baez (Apr 13 2020 at 22:12):

This is why much earlier in this thread I quoted someone who called this operation "unless", reading a⊂b as "a unless b".

John Baez (Apr 13 2020 at 22:12):

Mike Shulman didn't like that.

John Baez (Apr 13 2020 at 22:13):

This way of thinking of it, as a∧¬b, is only right for boolean algebras.

Dan Doel (Apr 13 2020 at 22:13):

Is 'unless' even a good reading in a Boolean algebra? I'm unsure.

John Baez (Apr 13 2020 at 22:14):

And even in that case maybe a∧¬b should be called "a but not b", instead of "a unless b".

John Baez (Apr 13 2020 at 22:14):

I find "a unless b" to be a pretty nice shortening of "a but not b", but I guess our everyday use of "unless" is pretty flexible.

John Baez (Apr 13 2020 at 22:14):

Probably it's bad to say "unless" here!

John Baez (Apr 13 2020 at 22:15):

Yeah, I think it's misleading. "But not" or "and not" is a lot clearer.

Dan Doel (Apr 13 2020 at 22:16):

Oh, I see. I wasn't thinking of that reading.

Henry Story (Apr 13 2020 at 22:16):

Does that help make sense of the Co-exponential diagram ?
I guess $\ni_{A,B}: B \to B_A \oplus A$ we have (B -A) + A ?

John Baez (Apr 13 2020 at 22:16):

The main problem with "and not" is that it won't be correct in the nonboolean case.

Dan Doel (Apr 13 2020 at 22:16):

Like, 'b' could be a modifier of 'a', and you'll only agree to 'a' if 'b' is not involved.

Dan Doel (Apr 13 2020 at 22:16):

I'll have a slice of cake unless it has chocolate frosting.

John Baez (Apr 13 2020 at 22:17):

Right, that's what I was thinking of.

John Baez (Apr 13 2020 at 22:17):

I really want some phrase that means exactly the same thing in everyday language as "and not", but doesn't use those exact words.

John Baez (Apr 13 2020 at 22:17):

"But not" is halfway there.

John Baez (Apr 13 2020 at 22:18):

I'll have a slice of cake but not with chocolate frosting.

Dan Doel (Apr 13 2020 at 22:19):

This form of unless needs to be a quantifier or something, though. :slight_smile:

Christian Williams (Apr 13 2020 at 22:22):

So evaluation for a Boolean algebra $A\wedge (A\supset B) \to B$ is modus ponens.
Now for coevaluation... you get $A\to B\vee (A\subset B)$, which is $A\leq B\vee (A\wedge \neg B)$.

Christian Williams (Apr 13 2020 at 22:23):

That's what this $\ni_{A{,}B}$ is.

Christian Williams (Apr 13 2020 at 22:24):

In a Boolean algebra this isn't very illuminating... do we know an example of a category with this left adjoint, rather than a preorder? I guess they're not called bi-Heyting categories, because Heyting category has a different meaning.

Dan Doel (Apr 13 2020 at 22:26):

I have a vague recollection there's some theorem that you can only have preorders like this in classical mathematics.

Dan Doel (Apr 13 2020 at 22:28):

I don't recall the details, though. There may be size conditions or something.

Dan Doel (Apr 13 2020 at 22:29):

I would look for 'bicartesian closed'.

Dan Doel (Apr 13 2020 at 22:30):

https://ncatlab.org/nlab/show/bicartesian+closed+category

Henry Story (Apr 13 2020 at 22:33):

They are also called Brouwerian or co-Heyting Algebras. But if you put co-Heyting with Heyting together you get classical logic.

Dan Doel (Apr 13 2020 at 22:47):

I think a proof sketch may be: $C(A,B) \simeq C(A,B+0) \simeq C(A-B,0)$, but 0 must be a strict initial object in a bicartesian closed category, so $A-B$ is also an initial object.

Henry Story (Apr 13 2020 at 22:48):

Trying the Popperian falsificationist view on this.
A: Money on Account
B: Payment with Debit Card
C: Banking system working
Co-exponential diagram
so $B_A$ would be worlds where I pay with debit card but don't have money on account.

Henry Story (Apr 13 2020 at 22:52):

That example does not make sense. The problem I find is that one has to keep thinking of negating the propositions.

Henry Story (Apr 13 2020 at 23:04):

Does this example work better?
B: Money on my Account
C: Banking system working
A: Payment with debit card
Then $B_A$ is money on account but can't pay with debit card. That would make sense that I can then move up to C.

Henry Story (Apr 13 2020 at 23:09):

The idea is that one should be able to dualise the reasoning positively, I think. So that $\ni: B \to B_A \oplus A$ turns into $\epsilon: B^A \otimes A \to B$
So positively given $f: B^A$ a function from a proof of payment to a proof of money on account and $a: A$ a proof of payment I can get a proof of money on account.

Dan Doel (Apr 13 2020 at 23:15):

If this is intuitionistic logic turned backwards, one should think about judgments like $A ⊢ Σ$ right? Where $Σ$ is a disjunction of competing explanations for the single item $A$? Then you have, e.g. $A$ being 'transaction failed', $B$ being 'out of money' and $C$ being 'banking system broken', and $A ⊢ B,C$. Then moving to $A-B ⊢ C$ indicates that if you rule out $B$ as an explanation for $A$, then $C$ is the only remaining explanation.

Dan Doel (Apr 13 2020 at 23:17):

I'm sure I have money, so the banking system must be broken.

Henry Story (Apr 13 2020 at 23:21):

yes. definitely looks like we're narrowing in on the example there. Btw you need to reverse the turnstile in the co-intuitionistic reasoning :-)

sarahzrf (Apr 13 2020 at 23:22):

Dan Doel said:

I've been wondering if some adaptation of this would be a more appropriate than linear logic for an application like in Linear Logic for Constructive Mathematics. It seemed like that wasn't strictly interested in linearity (since the chu construction given supports a bunch of extra rules more like affine logic), but in having a richer set of connectives to make sense of stronger notions of refutation.

i dunno, i think linear logic definitely has a strong tie to that stuff

sarahzrf (Apr 13 2020 at 23:23):

or at least affine

sarahzrf (Apr 13 2020 at 23:24):

to be precise, i think notions of like "continuation" or "covalue" or "dual type" are extremely at home in linear logic

sarahzrf (Apr 13 2020 at 23:25):

and i think that's sort of a computational way of looking at "refutation as a positive notion"

John Baez (Apr 13 2020 at 23:25):

Henry Story: They are also called Brouwerian or co-Heyting Algebras. But if you put co-Heyting with Heyting together you get classical logic.

If by "classical logic" you mean a boolean algebra, this is not true. This thread started out with me asking for bi-Heyting algebras that aren't boolean, and people found a truckload of them! Namely:

• the poset of subobjects of any object in any presheaf category.
• any finite distributive lattice.

The term "classical logic" is rather vague, so I'd avoid using it when trying to state precise results.

sarahzrf (Apr 13 2020 at 23:26):

hmm

Dan Doel (Apr 13 2020 at 23:26):

What is the connection with 'used at most once'?

sarahzrf (Apr 13 2020 at 23:27):

give me a second, i have some reasoning for this c:

Dan Doel (Apr 13 2020 at 23:28):

It seems like limiting the structure of things induces these dual connectives, but that limitation doesn't need to be linearity of occurrence, it can be other notions.

Dan Doel (Apr 13 2020 at 23:30):

And there might be limitations that make more sense for constructive mathematics than linearity. Or maybe not, but it's a thought I've had.

sarahzrf (Apr 13 2020 at 23:30):

i mean like

Henry Story (Apr 13 2020 at 23:30):

John Baez said:

If by "classical logic" you mean a boolean algebra, this is not true. This thread started out with me asking for bi-Heyting algebras that aren't boolean, and people found a truckload of them!

Ah I wrote that because the papers I am reading seem to say there are proofs that these collapse into boolean algebras, and they speak of classical logic. I should try to find a quote...

sarahzrf (Apr 13 2020 at 23:30):

intuitionistic linear logic is a thing, and it doesnt have duality

sarahzrf (Apr 13 2020 at 23:30):

speaking of which, "intuitionistic linear logic" is such a dumb name for it 🤬

sarahzrf (Apr 13 2020 at 23:33):

anyway ugh im having trouble articulating my vague sense of the connection between single-use and continuations

sarahzrf (Apr 13 2020 at 23:33):

well, they need to go together to keep nice normalization properties anyway

John Baez (Apr 13 2020 at 23:33):

Henry Story said:

Ah I wrote that because the papers I am reading seem to say there are proofs that these collapse into boolean algebras.

They either don't really say that, or they're wrong.

• nLab, Bi-Heyting topos

gives the examples of Bi-Heyting algebras that aren't boolean algebras that I just mentioned.

sarahzrf (Apr 13 2020 at 23:34):

otherwise you get the good old Cont (P + ¬P)

Dan Doel (Apr 13 2020 at 23:34):

You haven't read Compiling with Classical Continuations, because they show how to resolve the confluence problems, if that's what you're talking about.

sarahzrf (Apr 13 2020 at 23:34):

you're right, i haven't!

Dan Doel (Apr 13 2020 at 23:34):

The choice of an evaluation order resolves the ambiguity in classical logic.

sarahzrf (Apr 13 2020 at 23:35):

i dunno if that's what i'm talking about, though

sarahzrf (Apr 13 2020 at 23:35):

i don't just mean ambiguity, i mean like

sarahzrf (Apr 13 2020 at 23:35):

the fact that you can implement LEM if you have continuations

sarahzrf (Apr 13 2020 at 23:35):

this is a blatant violation of some kind of normalization

sarahzrf (Apr 13 2020 at 23:36):

unless your opsem is uncomputable

Henry Story (Apr 13 2020 at 23:36):

Good night. way too late here!

sarahzrf (Apr 13 2020 at 23:37):

if you want to get really concrete, i mean—

sarahzrf (Apr 13 2020 at 23:38):

actually wait now im thinking im mischaracterizing, hmm can't quite remember...

sarahzrf (Apr 13 2020 at 23:38):

maybe the thing you really lose is some sort of substitutivity...

Dan Doel (Apr 13 2020 at 23:40):

I mean, I agree there are good reasons for having linearity with continuations. I just don't know if those reasons translate to any benefit for constructive mathematics.

sarahzrf (Apr 13 2020 at 23:41):

...how about the traditional reasoning for why that one irrationality proof is unconstructive?

sarahzrf (Apr 13 2020 at 23:43):

wait, where did i see that reasoning

sarahzrf (Apr 13 2020 at 23:43):

maybe it isn't traditional?

sarahzrf (Apr 13 2020 at 23:46):

aha! it was in the slides for "linear logic for constructive math" http://home.sandiego.edu/~shulman/papers/lcm-bloomington-talk.pdf

sarahzrf (Apr 13 2020 at 23:46):

i thought i'd seen it associated with that paper but "irrational" doesnt appear in it...

sarahzrf (Apr 13 2020 at 23:47):

but i feel like i've seen this line of reasoning before somewhere else too...

Dan Doel (Apr 14 2020 at 00:00):

Well, that makes some sense, but it doesn't mean some other system couldn't also make sense.

Dan Doel (Apr 14 2020 at 00:01):

Like, you cannot directly compare these systems. $¬¬P$ is not something that makes sense in Compiling with Classical Connectives. It is ill formed.

Dan Doel (Apr 14 2020 at 00:02):

$P ∨ ¬P$ is also not well formed.

Dan Doel (Apr 14 2020 at 00:05):

It's possible the system isn't normalizing, though. I'm not clear on that aspect.

Dan Doel (Apr 14 2020 at 00:26):

Anyhow, I don't know. Maybe that argument makes something more like linearity make more sense for constructivity. Maybe 'evaluation order' really isn't something you want to think about. But it's possible that 'evaluation order' has some broader interpretation.

sarahzrf (Apr 14 2020 at 00:33):

augh cwcc does look very interesting but i am just not in the headspace to read it rn

Gershom (Apr 14 2020 at 00:49):

Dan Doel said:

I mean, I agree there are good reasons for having linearity with continuations. I just don't know if those reasons translate to any benefit for constructive mathematics.

well there's the stuff with krivine's "classical realizability" and more generally the whole idea of "proof mining" where you take classical proofs (traditionally topological convergency stuff) then "run them through the translation/realization with continuations" box and extract algorithms that tell you, uh... stuff..

John Baez (Apr 14 2020 at 01:12):

sarahzrf said:

...how about the traditional reasoning for why that one irrationality proof is unconstructive?

Which irrationality proof is that? Some people mistakenly think the classic proof that $\sqrt{2}$ is irrational is nonconstructive, but they're mixed up.

Hmm, even Wikipedia, which I linked to, calls this a "proof by contradiction", but it's technically not: even intuitionists allow you to prove $\neg P$ by assuming $P$ and using this to show $\neg P$.

John Baez (Apr 14 2020 at 01:18):

Probably nobody here is confused about this, but if anyone who has friends or relatives who are confused they should get them to read this:

• Andrej Bauer, Proof of negation and proof by contradiction.

sarahzrf (Apr 14 2020 at 01:20):

im thinking maybe it isnt "traditional" after all :sweat_smile:

sarahzrf (Apr 14 2020 at 01:20):

this and the next page http://home.sandiego.edu/~shulman/papers/lcm-bloomington-talk.pdf#Navigation18

sarahzrf (Apr 14 2020 at 01:23):

fun story about that link: i once started harping on roughly that point to someone, she told me that it reminded her of andrej bauer, i was like "nahhh i think it's just a pretty common point to make for people into constructive math" and then she linked me that article and i was like "oh, wait, right, i have indeed actually read this,"

Reid Barton (Apr 14 2020 at 02:46):

Just to clarify, a "complement-topos" really is just the same thing as a topos, right? I found the article I looked at rather confusing.

Dan Doel (Apr 14 2020 at 02:59):

@Gershom Just because you don't have linear continuations doesn't mean you don't have continuations. The question is whether the linearity is actually necessary, or if some other structural discipline is as good or better. There might be other ways to decompose arguments in a classical-looking way without actually being classical or linear. I am familiar with the observation that linearity makes continuations constructive because you're required to actually use them with a single value. I think I was aware of that point a while before that paper, since some folks I knew through Haskell were thinking about it.

My takeaway from classical realizability is that you can (probably) view all mathematics as having computational underpinnings, but what a classical proof is computing is not the plain reading of the theorem. A constructive proof of $∃ r:ℝ. ...$ tells you how to compute a real number. A classical proof tells you how to compute a way of winning an argument against anyone who says you don't have a real number, or something like that. Sometimes you can do that by actually computing a number, but it's not necessary.

Some of this even shows up in constructive schools, though, I think, and the realizability toposes that model them. If you follow Markov, you're in the effective topos, and $ℝ$ is the computable reals. If you follow Brouwer, you're in a different setting where the object $ℝ$ has non-computable numbers, and Brouwer uses these in his counter-examples and such. But proofs of existence must be computable, because those are like sections $1 → ℝ$, which must come with computable realizers. So, the 'creating subjects' are allowed more freedom in how they can come up with values of a type, but proofs are limited.

Then I think that classical realizability might be more like when proofs are also allowed this additional freedom, so that even a section $1 → ℝ$ is no longer required to give a method of computing a real.

sarahzrf (Apr 14 2020 at 05:31):

i have to say i have been fascinated for a while by the dynamic of an interaction between a fixed program and an indeterminate environment and/or creating subject

sarahzrf (Apr 14 2020 at 05:32):

i cant remember whether it predates that one time you posted about a brouwerian objection to markov's principle but im pretty sure it helped either way :)

Henry Story (Apr 14 2020 at 11:48):

Christian Williams said:

So evaluation for a Boolean algebra $A\wedge (A\supset B) \to B$ is modus ponens.
Now for coevaluation... you get $A\to B\vee (A\subset B)$, which is $A\leq B\vee (A\wedge \neg B)$.

I used your above remark to provide a first tentative but detailed answer to the question on StackExchange Examples of co-implication
I still don't feel comfortable about the interpretation of $B_A$.

Henry Story (Apr 14 2020 at 16:35):

In a short 2015 paper Co-Constructive logics for Proofs and Refutations starts by keeping constructive and co-constructive logics seperate. This I think makes it easier to understand what is going on.

In constructive logic we have $\Gamma \vdash \alpha$ meaning that if all formula in $\Gamma$ are accepted then we must accept $\alpha$. If we accept that sequent, yet also refute $\alpha$, then we'd be obliged to refute one of the premises in $\Gamma$. In co-constructive logic we want to have $\Gamma \dashv \alpha$ means that if $\Gamma$ is refuted then so $\alpha$ is too. Here we want to make sure that refutation is transmitted (just as in constructive logic we need to proove that all the premises are true) so we are looking for all of $\Gamma$'s formulas to be refuted (not completely sure about this yet!).

Co-constructive logic is thus a logic of refutation. Imagine you are trying to refute someone: you win if you can prove them wrong, so false is good! In both cases the formulas are to be understood as types. The witnesses to the formulas in the case of constructive logic are elements of the type, which can also be thought of as proofs. On the other hand, in the co-constructive world witnesses are refutations of the type. Perhaps one can think of them as being part of the shadow of the type?

Henry Story (Apr 14 2020 at 17:44):

I think I am reading things the wrong way around. I should have stopped at if we refute $\alpha$ then we must also refute $\Gamma$, which means we can choose one of the elements of $\Gamma$ to refute. Otherwise the following rule from Structuring Co-constructive Logic for Proofs and Refutations would not make sense

$\dfrac{\Delta \dashv } {\Delta \dashv \alpha} \textsf{(Weak-R)}$

It would not make sense that if all of $\Delta$ is refuted that one can deduce a new arbitrary refutation. On the other hand if from nothing one can refute $\Delta$ then certainly one can refute it also given some refuted $\alpha$.
Similarly the following shows that one must interpreted the left side disjunctively.

$\dfrac{\Delta \dashv \beta} {\Delta, \alpha \dashv \beta} \textsf{(Weak-L)}$

Henry Story (Apr 14 2020 at 19:16):

Ok, I am happy with my answer for how to think of co-constructive logics on Stack Exchange: Examples of co-Implication :-)
I start very simply from a basic constructive sequent, in order to show that by falsifying the conclusion one is led straight to co-constructive logic. Then I give an example about paying with a credit card in constructive logic using exponentials and turn it around to explain co-implication (aka. co-exponentials). This actually nicely shows the advantage of falsification based thinking. It fits nicely together.

Henry Story (Apr 14 2020 at 20:33):

There is something that reminds me of probability in co-exponentials. If one reads $A \leftarrow B$ as a refutation of A that does not depend on one of B, is that not similar to thinking of A given B? Especially as in probability any number can be thought of as a probability of a refutation as much as one of truth. No idea if the rest of the structure even gets close to working on this.

Amar Hadzihasanovic (Apr 15 2020 at 09:30):

Just for fun, I was reminded of Jean-Yves Girard's comment on “co-implication”, in his signature style:

If there is a category-theoretic solution, one is liable to provide a legible category. And not to formulate the adjunction rules – say – of a professed «subtraction» – the typical connective of the category-theoretic bricoleurs – supposedly acting like implication, but on the left. Hence, one must provide a concrete category, or at least a translation into a system already having a non-degenerate category-theoretic interpretation. What the experts in «subtraction» carefully avoid doing... with good reasons.

Amar Hadzihasanovic (Apr 15 2020 at 09:32):

(This is in a section entitled Loch Ness categories)

Matteo Capucci (he/him) (Apr 15 2020 at 19:39):

Uh that's cool!

Henry Story (Apr 22 2020 at 15:45):

I think I finally feel comfortable with my answer on examples for co-exponentials on Math Stack exchange. :relieved:

Henry Story (Apr 23 2020 at 21:39):

John Baez said:

I don't know what you mean by "classical", but the subobject classifier for graph is not a boolean algebra. That's why it's good for breaking one of ones boolean habits.

I found this nice article A Guided Tour in the Topos of Graphs. Sadly it does not develop the complement intutionistic version of it. Nor does it give good clues as to what kind of logic comes from it, and where it would best be used.
It is cited by the article Complement-Topoi and Dual Intuitionistic Logic which is very nice as it starts from Topoi to get to the inference rules of intuitionistic and complement intuitionistic logic, which feels like solid very ground to start from.
It gets very confusing otherwise: Logicians seem to have decades long debates on which rules are really dual to the intuitionistic ones. I have seen philosophers and logicians unacquainted with CT getting lost in those debates. So I'll now take this as my starting point.

Pastel Raschke (Apr 24 2020 at 07:27):

Screenshot_20200424-082619_MuPDF_mini.png

Pastel Raschke (Apr 24 2020 at 07:32):

trafford, meaning in dialogue

Pastel Raschke (Apr 24 2020 at 07:35):

this seems.... very incorrect. f_T is equal to t in the first diagram, is it not? if it's not a commutative diagram, what is it?

Henry Story (Apr 24 2020 at 07:48):

This is perhaps more cleanly explained in Complement-Topoi and Dual Intuitionistic Logic by Luis Estrada-González, which is where Trafford gets it from (and cites him).
I myself (but I am not good enough to judge) feel that there has to be a relation between the true and false in the topoi and complement topoi. But Estrada-Gonzalez seems to say it's only a question of naming. Indeed he builds a whole argument on that in The Evil Twin: The Basics of Complement-Toposes. That reasoning really needs to be checked by compotent Category Theorists.

Henry Story (Apr 24 2020 at 07:52):

The process is as follows (I think). Select a morphism $true: 1 \to \Omega$ in the right category as your subject classifier. From that you can define false as a pullback, $\lnot$ and the other connectives For the complement-topos select a morphism $false: 1 \to \Omega$ and following the process you can then define true as a pullback to 0, $\lnot$ and the dual connectives

Henry Story (Apr 24 2020 at 08:03):

Each choice gives rise to clearly different but dual logics. So there must be a way to relate them. If not then the philosophical implications drawn by Gonzalez seem to follow. What does seem to follow in any case is that the same category can have more than one internal language. Do they perhaps always come in pairs? (That would not be surprising as Category Theory lends itself so well to dualities)

Henry Story (Apr 24 2020 at 08:19):

if you start with $true: 1 \to \Omega$ you get a subobject classifier that for every object gives you its subobjects that can be seen as a Heyting algebra with arrows pointing to $\top$. If you choose $false: 1 \to \Omega$ you get a subject classifier that for every object in that category gives its subobjects that form a co-Heyting algebra where the arrows are pointing to $\bot$.

Henry Story (Apr 24 2020 at 08:21):

Could it be that there is only one $\Omega$ and one $true, false: 1 \to \Omega$ up to isomorphism, and the question is which way you look at the arrows between the subobjects, creates the Heyting or co-Heyting algebra?

Henry Story (Apr 24 2020 at 08:52):

Perhaps @David Spivak who is developing the Topos Institute can help us here :-)

Pastel Raschke (Apr 24 2020 at 08:59):

you don't have a choice of mono classifier, and pullbacks are defined from the cospan, not the other way around.

i believe this is defining f_T as the classifying map of the unique map 0 -> 1 (which i believe is monic due to every X -> 0 making X initial so any parallel pair is equal), which is unique and then forms a pullback by virtue of the mono classifier.

negation is then defined as the classifying map of f_T (which i believe is monic due to every X -> 1 being unique &c).

i believe this is a consistent development.

Pastel Raschke (Apr 24 2020 at 09:09):

the problem here is that renaming is only changing your translation of syntax to the same heyting algebra, and i'm not sure that helps you figure out how to combine what you consider a subobject classifier and a 'complement classifier', or the topoi thereof, in the way that you want.

Pastel Raschke (Apr 24 2020 at 09:18):

Screenshot_20200424-101809_MuPDF_mini.png

Pastel Raschke (Apr 24 2020 at 09:23):

this is incorrect; as john baez has pointed out several times, bi-heyting algebras, categories, topoi are not boolean. for myself, i believe it does not mean anything for a topos to "also have a complement classifier", as the complement classifier is the subobject classifier.

Pastel Raschke (Apr 24 2020 at 09:38):

i believe what this proof is demonstrating is that when subobjects in a topos are complemented, the topos is boolean. what this suggests to me is that what you want to hold your interacting heyting+brouwer logic is not a topos.

Henry Story (Apr 24 2020 at 10:05):

I think he defines the subobject classifier as the function $1 \to \Omega$ that fits the characteristic morphism pullback.
Since via a pullback to 0 one can get false, then one can also get another subobject classifier that seems to fit the same diagram.
He then writes in "Complement Topoi and dual intuitionistic Logic":

Let $\phi \Vdash_\epsilon \psi$ denote that whenever the morphism $\phi$ is the same morphism as true in $\epsilon$

So for the above false one can create the dual $\Vdash_C$

Let $\phi \Vdash_C \psi$ denote that whenever the morphism $\phi$ is the same morphism as false in $C$

Each of these subobjects classifies any objects into its subobjects, and the relations between these subobjects gives rise to a heyting-lattice in the case of true and a co-heyting lattice in the case of false. These I guess are Opposite categories (turn the arrows around and you get the other). So the two generated categories are separate, no?

I wonder why this would not be the right way to interpret the coexistence of heyting and co-heyting in a topos.

Henry Story (Apr 24 2020 at 10:10):

Trafford does not want to put those two lattices together. Just map propositions from one to the other, so that if in a dialogue Proponent asserts $A$, then Opponent can assert $A^o$ in the refutation lattice.

Henry Story (Apr 24 2020 at 10:25):

Pastel Raschke said:

i believe what this proof is demonstrating is that when subobjects in a topos are complemented, the topos is boolean. what this suggests to me is that what you want to hold your interacting heyting+brouwer logic is not a topos.

Are you saying that the counter examples of bi-heyting algebras that are not boolean put forward by @John Baez which you mention above (and which I have not yet studied) can not live in a topos?

Pastel Raschke (Apr 24 2020 at 12:08):

the mono classifier 1 -> TV of a topos selects truth in the heyting algebra of the TV, and is unique up to isomorphism. the TV of a topos is a heyting algebra, not a co-heyting algebra.

the TV of a bi-heyting topos has a co-heyting algebra, but its operations are not preserved by inverse image functor (i assume that's the appropriate notion of topos morphism).

via classifying 0 -> 1 one obtains the mono 1 -> TV that selects false, and classifying that gives the negation TV -> TV. false is not a mono classifier. it is not even a mono classifier when the topos is boolean.

in a boolean topos, every mono i into x has a complement ī, which is a mono ī such that i ∩ ī = 0 and i ∪ ī = 1. the complement is a mono, and it is classified by the mono classifier, which selects truth.

i am not sure why you would want to interpret brouwer logic into a topos. coimplication matches coexponentials/co(cartesian closure), coapplying covalues to cofunctions in covariables :^), not the exponentials of a topos. but i don't understand the idea of a quotient coclassifier in a cotopos, or if the opposite of a topos is the right category for first-order brouwer logic.

polarity and adjunctions and duploids tend to be a good framework for theories that collapse into degeneracy when you interpret them naively.

what does degenerate: a category that is cartesian closed and cocartesian coclosed
what does not degenerate: a bi-heyting algebra, which is not a boolean algebra

Henry Story (Apr 24 2020 at 13:46):

Pastel Raschke said:

i am not sure why you would want to interpret brouwer logic into a topos. coimplication matches coexponentials/co(cartesian closure), coapplying covalues to cofunctions in covariables :^), not the exponentials of a topos. but i don't understand the idea of a quotient coclassifier in a cotopos, or if the opposite of a topos is the right category for first-order brouwer logic.

Gonzalez does give a reason for this in Complement Topoi and Dual Intutionistic Logic which looks strong. He writes quoting the book Inconsistent Mathematics

Mortensen’s argument for developing an inconsistency-tolerant approach to category theory does not rest on a sophisticated philosophical position, but in that given that every topological space gives a topos (the category of pre- sheaves on the space), mathematically

(. . . ) specifying a topological space by its closed sets is as natural as specifying it by its open sets. So it would seem odd that topos theory should be associated with open sets rather than closed sets. Yet this is what would be the case if open set logic were the natural propositional logic of toposes. At any rate, there should be a simple ‘topological’ transformation of the theory of toposes, which stands to closed sets and their logic [i.e. inconsistency-tolerant], as topos theory does to open sets and intuitionism. [11, p. 102)

It looks like the heyting and co-heyting are really dual. Is it as simple as that they are just live in opposite categories. Do we have that much secured? I guess the product, sum, (co-)exponential, appear in the (co-)heyting algebra categories. I was actually wondering about that yesterday.

It can't quite tell if one is meant to find a complement topos in the same category, or of one is meant to search for a separate complement-Topos category, in which all those constructions are meant to hold. I guess if one found the category that fits the topological closed sets should tell us what is meant to be done.

Morgan Rogers (he/him) (Apr 24 2020 at 13:59):

Pastel Raschke said:

via classifying 0 -> 1 one obtains the mono 1 -> TV that selects false, and classifying that gives the negation TV -> TV. false is not a mono classifier. it is not even a mono classifier when the topos is boolean.

On the contrary, it is a mono classifier if and only if the topos is Boolean, so that negation is an isomorphism (then every mono $A \hookrightarrow B$ is the pullback of $\bot: 1 \to \Omega$ along the morphism $B \to \Omega$ classifying the complement of $A$).
If the negation (pseudo-complement) operation is a monomorphism, then the morphism "false" classifies pseudo-complements of subobjects: subobjects of $B$ of the form $\neg A$ (or $A \rightarrow 0$). I don't know just by looking if there are cases where $\neg: \Omega \to \Omega$ is a mono but not an iso; if there are then this is the context in which complements could be interesting to study.

Pastel Raschke (Apr 24 2020 at 14:13):

i was thinking about it more and came back to correct myself, thanks for the explanation

Pastel Raschke (Apr 24 2020 at 14:22):

one of the necessary and sufficient conditions on toposes to be boolean, from nlab:

The maps ⊤,⊥:1→Ω are a coproduct cone (so in particular, Ω≅1+1, and in fact this is enough, because the map [⊤,⊥]:1+1→Ω is always a monomorphism, and any monic endomorphism of Ω is an automorphism).

no idea how to derive that last statement personally.

Morgan Rogers (he/him) (Apr 24 2020 at 14:24):

The end of that quoted statement would indeed imply that there is only a pseudo-complement classifier when the topos is Boolean.

Henry Story (Apr 24 2020 at 16:36):

From the 1995 Book Inconsistent Mathematics whose chapter 11 gives a category theoretic interpretation of top and complement topoi:

An (elementary) complement-topos is a category with initial and terminal objects, pullbacks, pushouts, exponentiation, and a complement classifier. It is clear that, if E is it complement-topos and E' is the category obtained by renaming F as T and each $\overline{\chi}_f$ as $\chi_f$ then E' is a topos; since initial and terminal objects, pull- backs, pushouts and exponents are prior category-theoretic notions independent of classifiers. This enables a dualisation of all topos constructions substituting F for T and $\overline{\chi}_f$ for $\chi_f$ ...

The duality theorem states that complement topos and topos are the same other than renaming.

And in conclusion:

It hardly bears saying that a complement-topos really is a topos, it is just a matter of how one understands the notion of a subobject classifier. This can be masked by the usual terminology of $\top : 1 \to \Omega$, rather than F as we have. There are various natural paraconsistent propositional logics arising from the $\mathcal{E}$-semantics of complement-toposes, and thus from toposes. The bias toward intuitionism is at least not justified by these structural aspects of a topos, since it depends on how they are interpreted.

Henry Story (Apr 24 2020 at 16:56):

The authors end with this remark before moving on to closed set sheaves

We conclude this section by raising the question of whether there is a construction internal to topos theory (rather than dualising 'outside' the topos as we have) which also yields paraconsistent logic. This seems not unreasonable.

Morgan Rogers (he/him) (Apr 24 2020 at 16:57):

I have to be frank, it sounds like their entire argument is based on a misunderstanding of what the subobject classifier is, and notably of the fact that the subobject classifier is also a categorical notion just as initial and terminal objects etc are.
One can get co-Heyting algebras by reversing the order in the subobject lattices, but the idea that that's somehow equivalent to a renaming is a misconception. The bias towards wanting the order to coincide with the direction of the arrows in the topos seems like a perfectly natural one. One conclusion might be that a better setting for paraconsistent logic is in the co-Heyting algebras of quotient objects in a cotopos.

Henry Story (Apr 24 2020 at 16:59):

Are there other references for these concepts "co-Heyting algebras of quotient objects in a cotopos"?

Morgan Rogers (he/him) (Apr 24 2020 at 17:12):

I don't know, but I can be more precise if you like!
By cotopos I mean the categorical dual of a topos, with all of the arrows reversed. This means that I still have finite limits and colimits, but I have co-exponentials (satisfying the dual property of exponentials) and a "quotient co-classifier" (an object $\mho$ equipped with an epimorphism $\bot: \mho \to 0$, where $0$ is the initial object, such that any epimorphism with domain $X$ is the pushout of $\bot$ along a unique classifying morphism $\mho \to X$).

Morgan Rogers (he/him) (Apr 24 2020 at 17:14):

Since the epimorphisms in such a cotopos correspond to monomorphisms in the dual topos, the quotient lattices in the cotopos will be exactly the subobject lattices in the topos, but with the ordering (in the direction of the arrows) reversed.

Morgan Rogers (he/him) (Apr 24 2020 at 17:18):

Cotoposes aren't much studied in their own right ("why study Set^op when I can study Set?") but they are indispensible for elementary topos theory, in the first instance due to fact that the dual of a topos is monadic over that topos, and this is used to show that the topos having finite limits also endows it with finite colimits.

Henry Story (Apr 24 2020 at 17:20):

"why study Set^op when I can study Set?"

Yes, then one finds out that co-algebras are dual of algebras but open up completely new worlds!

Henry Story (Apr 24 2020 at 17:24):

So it looks like they were onto something, but failed to see that they were working in the opposite category.

Henry Story (Apr 24 2020 at 17:27):

What is weird is that in their diagrams they use exponentials but should have needed co-exponentials.

Henry Story (Apr 24 2020 at 17:29):

It would be very interesting to find non-trivial useful dual to a topos that is not that difficult to understand (for me) where one could look at that and see if it makes sense. What would the dual to a graph topos be?

Henry Story (Apr 24 2020 at 17:48):

Is there a relation between closed set topology and a dual topos?

sarahzrf (Apr 24 2020 at 18:01):

or maybe they were just working in the opposite lattices period

sarahzrf (Apr 24 2020 at 18:02):

and not the opposite category at all

Henry Story (Apr 24 2020 at 18:13):

Indeed it seems to me that turning the Heyting lattice around seems to be the minimal step needed to get to closed set topology or co-constructive logic. I wonder why they thought that it was necessary to do so at the Topos level. I guess their point would be in return why privilege open set over closed set topology? If one starts with open sets one needs to do an dualisation to get to closed. I guess they are trying to find a way to get to closed in one step.

John Baez (Apr 24 2020 at 18:53):

Henry Story said:

Are you saying that the counter examples of bi-heyting algebras that are not boolean put forward by John Baez which you mention above (and which I have not yet studied) can not live in a topos?

A bunch of them do live in a topos: as I said, the lattice of subobjects of any presheaf topos is a bi-Heyting algebra, and rarely is it boolean. For example the lattice of subgraphs of any graph (in the category theorist's sense of graph) is bi-Heyting.

This is why there's an nLab article bi-Heyting topos.

Henry Story (Apr 24 2020 at 20:57):

It looks like I may have had an $A \to \bot$ experience reading these papers on complement topoi then.

John Baez (Apr 24 2020 at 23:44):

Pastel Raschke said:

Screenshot_20200424-101809_MuPDF_mini.png

this is incorrect; as john baez has pointed out several times, bi-heyting algebras, categories, topoi are not boolean. for myself, i believe it does not mean anything for a topos to "also have a complement classifier", as the complement classifier is the subobject classifier.

Yes, Theorem 59 here is false. Where did it come from? I wouldn't trust this paper, given such an important mistake.

(In general you should be a bit suspicious of people who state theorems but don't prove them.)

Pastel Raschke (Apr 25 2020 at 07:19):

this is james trafford's book about inferentialism, meaning in dialogue. the proof attempt was the following paragraph.

Henry Story (Apr 25 2020 at 08:44):

The picture of the attempted proof that Category that is a topos has a complement Topos is boolean (my rendition) is here.

Henry Story (Apr 25 2020 at 08:46):

IF the proof does works but clashes with the existence of bi-heyting algebras it could well be that the definition of a complement topos is wrong, and that it should be based on co-exponentials and not exponentials. (so the problem with the proof would be prior to the proof)

Henry Story (Apr 25 2020 at 09:02):

I guess that Set should have a co-exponential, so it should be possible (for me to see) what happens when one turns the diagrams of a Topos around there.

Henry Story (Apr 25 2020 at 09:36):

I''ll look to see what a complement topos looks like in $\mathsf{Set}^{op}$ the category of complete boolean algebras according to this. But that would be a completely different concept of complement topos than the one they were trying to get at. If it did manage to capture complement sets, or for the ordering to go from $\top$ to $\bot$ as in co-heyting algebras it would be interesting though.

sarahzrf (Apr 25 2020 at 14:48):

complete atomic boolean algebras i think

sarahzrf (Apr 25 2020 at 14:48):

but also iirc if a category is both cartesian closed and cocartesian coclosed then it must be a proset

sarahzrf (Apr 25 2020 at 14:49):

https://ncatlab.org/nlab/show/cocartesian+closed+category

sarahzrf (Apr 25 2020 at 14:49):

image.png

Henry Story (Apr 25 2020 at 16:01):

Morgan Rogers said:

I don't know, but I can be more precise if you like!
By cotopos I mean the categorical dual of a topos, with all of the arrows reversed. This means that I still have finite limits and colimits, but I have co-exponentials (satisfying the dual property of exponentials) and a "quotient co-classifier" (an object $\mho$ equipped with an epimorphism $\bot: \mho \to 0$, where $0$ is the initial object, such that any epimorphism with domain $X$ is the pushout of $\bot$ along a unique classifying morphism $\mho \to X$).

I drew this up in this diagram.
ComplementTopos.jpg
I also drew up a simple example on the boolean topos to show how it works.
BA-Topos.jpg

Henry Story (Apr 25 2020 at 16:05):

I have been playing with simple examples of this co-topos in $\mathsf{Set^{op}}$ and indeed it seems to classify the atomic boolean algebra lattices from larger to smaller which is what one would need to then get the co-Heyting algebra.

Henry Story (Apr 25 2020 at 21:37):

Does the terminal object in $\mathsf{BA}$ the category of atomic boolean algebras which is just $\{ \emptyset \}$ have any special properties that could explain why it can turn inverse $\top$ and $\bot$ in the following co-topos?
Top.jpg
BA-Top.jpg

Henry Story (Apr 26 2020 at 08:34):

I have been working on dualising the Conjunction classifier in a Topos
This I think gives a co-product disjunction co-classifier in a co-Topos co-product.jpg
Which I illustrated in the atomic boolean algebra category Co-product-BA.jpg
I am not yet sure if I have the 0 and 1 are well chosen (in the BA diagram) or if they should be switched.
The disjunction co-classifier should be saying that if either of the disjuncts is refuted, then the conjunct in the topos in the opposite category to which it corresponds is "false".

Henry Story (Apr 26 2020 at 21:38):

I am trying to find a use of co-exponentials in the definitions of the operators in the complement topos, which has led me to read up on Goldblatt's Topoi: the categorical analysis of Logic.

Henry Story (Apr 26 2020 at 21:41):

The idea of a complement topos as the topos as seen in the opposite category does seem to be the thing that the authors on complement topoi discussed above were getting at. But for some reason they did not look at the dual category, and so tried to speak of it from the side of the topos category. As a result their concept looked very much like a Topos, and as they admit could not be distinguished from it. The intuitions that the complement topoi is what is behind co-Heyting algebras and co-constructive logic would then be correct.

Henry Story (Apr 27 2020 at 18:58):

Mhh, the product above in CABA is not a boolean algebra. It's a bit tricky working out what products and co-products in a boolean algebra are.... I asked on Stack Exchange. Perhaps I'll be able to answer that myself with more thought.