constructive and co-constructive logic · deprecated: logic

I wonder if those disagreements can be resolved with Category Theory by realising that constructive and co-constructive logics can be tied together to form first order logic. :-)
I found lots of papers along those lines. A recent one is Pragmatic logics for hypotheses and evidence

Henry Story (Jan 04 2021 at 06:40):

Here is how I think the argument goes. As a Category Theorist you accept that a proof in a Category

C

is also an opposite proof in the category

C^{op}

. So if a constructive proof is one that is provable in a Topoi, then any such proof is also one in the complement Topoi of co-constructive logics. And if it can be show that both of those together give first order logic, then there cannot be anything wrong with that either. Note that a lot of research recently seems to be focused on how one can avoid collapse into first order logic and have constructive and co-constructive logics work together. (I am not sure about this but I think I understood that when constructivists and co-constructivists agree - after a process of construction and attempted deconstruction - the result is a first order logic truth).

John Baez (Jan 05 2021 at 02:49):

By the way, I think "co-constructive" logic would do well to call itself "instructive logic", since that's a way of spelling "nstructive" that seems rather good for advertising purposes.

Valeria de Paiva (Jan 08 2021 at 21:40):

But Henry I don't think there is any evidence that "if it can be shown that both of those together give first order logic".
I also do not see any reason for co-constructive logic, except for an overzealous desire for symmetry. I love symmetry as much the next mathematician, but have not seen any good reason to do co-constructive logic, so far.

Peter Arndt (Jan 10 2021 at 19:10):

...and by the way a "complement topos" is not the opposite category of a topos, but it is precisely the same thing as a topos. I find it awful, but they use this expression just to emphasize that they employ the topos in question to interpret "coconstructive"/paraconsistent logic, and not intuitionistic logic.

Henry Story (Jan 10 2021 at 20:19):

It is a topos, viewed in a dual way. There are thus constructs which don't arise in a topos such as co-exponentials which I looked at about a year ago.

Henry Story (Jan 10 2021 at 20:22):

But Henry I don't think there is any evidence that "if it can be shown that both of those together give first order logic".
 I also do not see  any reason for co-constructive logic, except for an overzealous desire for symmetry. I love symmetry as much the next mathematician, but have not seen any good reason to do co-constructive logic, so far.

There are quite a lot of papers on the subject of complement topoi, and these are related to paraconsistent logics whose proponents I hear are known as "the brazilian school". One very intruiging relation is to the work of Popper https://twitter.com/bblfish/status/1248243867490672641

So here's an intriguing thesis: Where Intuitionistic Logic best describes Mathematical truths, it's dual, "falsification Logic" may be better adapted to scientific research. https://link.springer.com/article/10.1007/s11225-005-8474-7 https://twitter.com/bblfish/status/1248243867490672641/photo/1

- The 🐟‍‍ BabelFish (@bblfish)

Henry Story (Jan 10 2021 at 20:24):

Henry Story (Jan 11 2021 at 05:36):

I think one of the arguments for co-constructive logics goes back to the early topological interpretation of constructive logic in terms of open sets. Very early it was noticed that one could also interpret it in terms of closed sets. I think it was starting from that second interpretation that co-constructive logics started to emerge.

Henry Story (Jan 11 2021 at 06:05):

I don't know enough about the subject but perhaps the topological interpretation points to a way of putting this in Category Theory Terms? Interpretations in CT are usually in terms of functors. So I guess we have two functors from some Topos to a topological space, one to the open sets, the other to the closed ones?

Fawzi Hreiki (Jan 11 2021 at 09:38):

Actually, ‘co-constructive’ ie paraconsistent logic is closely related to mereology

Fawzi Hreiki (Jan 11 2021 at 09:39):

Fawzi Hreiki (Jan 11 2021 at 09:43):

The lattice of closed subsets of a topological space is a typical example of such a thing.

A more surprising example is the fact that the (big) poset of subtoposes of a topos forms a co-Heyting algebra.

Fawzi Hreiki (Jan 11 2021 at 09:44):

Since the subobject classifier contravariantly parametrises them via modal operators.

Morgan Rogers (he/him) (Jan 11 2021 at 10:40):

Subtoposes correspond to LT-topologies, which are endomorphisms of the subobject classifier, so the poset is actually conveniently small.

Fawzi Hreiki (Jan 11 2021 at 10:51):

Ah yes. Although it then depends what you mean by ‘small’ in the meta theory but you’re right

Fawzi Hreiki (Jan 11 2021 at 10:52):

I guess if you’re defining a topos in first order logic, there’s no reason a priori why it should be locally small, or what locally small even means

Matteo Capucci (he/him) (Jan 11 2021 at 10:54):

Fawzi Hreiki (Jan 11 2021 at 10:55):

I guess that’s the homotopy type theory style approach where small just means discrete

Morgan Rogers (he/him) (Jan 11 2021 at 10:57):

More like in the base topos. If your topos is bounded over

\mathcal{S}

, then your topos will be

\mathcal{S}

-enriched (and so

\mathcal{S}

-locally small)

Morgan Rogers (he/him) (Jan 11 2021 at 11:00):

Arbitrary toposes are scary, so certainly there are those where the subobject classifier has too many endomorphisms, fair enough :sweat_smile:

Henry Story (Jan 11 2021 at 11:26):

Do you have some pointers on both of those? I have found mereology pop up on the Semantic Web with Context Mereology by Pat Hayes. And I had come across it earlier in a book by David Lewis on Mereology, which summarised a book "Parts and Classes" where he deals with size issues, interestingly enough.

Fawzi Hreiki (Jan 11 2021 at 12:00):

Lawvere’s (very short) paper is here. The nLab page for co-Heyting algebras also has some other references. If I recall, the book Generic Figures and their Glueings has some stuff on them too.

Fawzi Hreiki (Jan 11 2021 at 12:02):

Much of the philosophical work on mereology is quite weak in my opinion because they usually implicitly just deal with subsets of sets. Sets are Boolean so their co-Heyting structure is trivial.

Fawzi Hreiki (Jan 11 2021 at 12:07):

I haven’t seen anything on this, but I don’t see why we can’t do ‘first order mereology’ using co-Heyting hyperdoctrines.

Henry Story (Jan 11 2021 at 12:08):

are you referring to Pat Hayes' article in your last comment "I haven't see anything on this..."?

Fawzi Hreiki (Jan 11 2021 at 12:16):

Henry Story (Jan 11 2021 at 13:02):

Ah, the interesting thing about Pat Hayes' article is that by introducing contexts it moves RDF to a simple form of modal logic I believe (I need to re-read that article carefully).

Category Theory
Zulip Server
Archive

Stream: deprecated: logic

Topic: constructive and co-constructive logic

Henry Story (Jan 01 2021 at 22:08):