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: deprecated: mathematics

Topic: logical equivalence

Reid Barton (Apr 05 2023 at 10:44):

In constructive mathematics one sometimes needs to consider the relation on two sets $A$ and $B$ given by "we have a function $f : A \to B$, and a function $g : B \to A$". It is in general stronger than saying that the propositional truncations of $A$ and $B$ are equivalent.

The HoTT book introduces (but never really uses in an essential way) this notion under the name "logical equivalence". I'm not that much of a fan because I understand logic as being about propositions, and it could be okay to say that our "propositions" could have multiple inhabitants, except that in the context of HoTT the term "proposition" is well-established to mean something else, and so it seems more reasonable to say that a "logical equivalence" is something that becomes an equivalence after propositional truncation.

Does anyone have another name they prefer? e.g., I suppose this notion must come up when working with E-categories, so maybe "E-equivalence" (ugh)?

Tom de Jong (Apr 05 2023 at 10:49):

and so it seems more reasonable to say that a "logical equivalence" is something that becomes an equivalence after propositional truncation.

You might call it a (-1)-equivalence then?

Reid Barton (Apr 05 2023 at 10:50):

(More specifically, the HoTT book introduces the term "logical equivalence" for arbitrary types, but then only ever applies it to propositions.)

Reid Barton (Apr 05 2023 at 10:50):

Tom de Jong said:

and so it seems more reasonable to say that a "logical equivalence" is something that becomes an equivalence after propositional truncation.

You might call it a (-1)-equivalence then?

I'm happy to call those (-1)-equivalences, but I'm looking for a name for the other notion--where there is no truncation involved, just maps that don't have to be inverse to each other.

Tom de Jong (Apr 05 2023 at 10:52):

Oh, I misunderstood, sorry.

Reid Barton (Apr 05 2023 at 10:53):

I see how my question was unclear, but I'll just take it as more evidence that the phrase "logical equivalence" is confusing. :upside_down:

Andrew Swan (Apr 05 2023 at 10:55):

I've always used the terminology "logically equivalent" several times, although to be fair it has caused confusion sometimes. I've seen these described as "biimplications" which is maybe more descriptive.

Tom de Jong (Apr 05 2023 at 10:56):

But you want a name for having maps in both directions, right? But if you do have such maps, then they are (-1)-equivalences, as their (-1)-truncations become equivalences. What is this "other notion" you're referring to?

Reid Barton (Apr 05 2023 at 10:57):

A (-1)-equivalence might not be a, well, logical equivalence. For example there might not be any map $||A||_{-1} \to A$.

Tom de Jong (Apr 05 2023 at 11:13):

Ah, of course, thank you

Sam Speight (Apr 05 2023 at 13:17):

Andrew Swan said:

I've always used the terminology "logically equivalent" several times, although to be fair it has caused confusion sometimes. I've seen these described as "biimplications" which is maybe more descriptive.

I've also seen "biimplication", which seems reasonable. But what would you say for the relation of standing in biimplication? Maybe you'd just say A and B stand in biimplication?

Mike Shulman (Apr 05 2023 at 17:41):

Reid Barton said:

The HoTT book introduces (but never really uses in an essential way) this notion under the name "logical equivalence". I'm not that much of a fan because I understand logic as being about propositions, and it could be okay to say that our "propositions" could have multiple inhabitants, except that in the context of HoTT the term "proposition" is well-established to mean something else

In fairness, I would like to point out that that "well-established" usage did not become established until somewhat after the HoTT Book was written. The book uses "mere proposition" for a $(-1)$-truncated type.

Personally, while I'm okay with dropping the "mere", I do think it's overly limiting to say that "logic" is only about $(-1)$-truncated types, so I don't see anything wrong with "logical equivalence".

Ryan Wisnesky (Apr 05 2023 at 17:54):

this happens a lot in database theory where they call it "homomorphic equivalence"

Reid Barton (Apr 05 2023 at 18:08):

That's a good point about "mere proposition"--I think I remembered $\textsf{isProp}$, and forgot about the "mere".

Reid Barton (Apr 05 2023 at 18:10):

I'm not saying logic always has to be about (-1)-truncated types, just about whatever "propositions" means in context. For example if your mathematical framework doesn't let you form (-1)-truncations, then it would definitely be a bad idea to interpret "proposition" as (-1)-type.

Mike Shulman (Apr 05 2023 at 18:13):

I'm okay with "proposition" meaning (-1)-type but "logic" being interpreted more expansively.

Reid Barton (Apr 05 2023 at 18:14):

What makes some mathematics not logic?

Mike Shulman (Apr 05 2023 at 18:14):

Logic is the superstructure in which mathematics is written. The mathematics itself is not the same as the logic.

Reid Barton (Apr 05 2023 at 18:25):

So for example type theory is also a kind of logic, or part of logic.

Reid Barton (Apr 05 2023 at 18:25):

That seems like a reasonable usage, but then I don't see any connection to the meaning of "logical equivalence".

Mike Shulman (Apr 05 2023 at 18:27):

I guess the argument is that "logic" is a point of view on type theory that emphasizes the inhabitation of types rather than the identity of their elements.

Reid Barton (Apr 05 2023 at 20:19):

Here's a not-sure-if-serious suggestion:
equivalence relation : pseudo-equivalence relation :: logical equivalence (= (-1)-equivalence) : logical pseudo-equivalence?

Mike Shulman (Apr 05 2023 at 20:28):

I don't think it would be a good idea to use "logical equivalence" to mean (-1)-equivalence. If you don't want to use it at all, that's one thing, but using it with a similar but different definition seems to me like a recipe for confusion.

Reid Barton (Apr 05 2023 at 20:34):

I am also tempted to coin "pseudoproposition" for a set/type which we would like to treat as though it were (-1)-truncated. Basically a setoid in which every two elements are related in a unique way.

Mike Shulman (Apr 05 2023 at 20:36):

What about "propositionoid"? (-:O

Reid Barton (Apr 05 2023 at 20:46):

That would make sense too but maybe it doesn't score so highly on the "is it really a word" test.

Mike Shulman (Apr 05 2023 at 20:53):

Yeah.

Mike Shulman (Apr 05 2023 at 20:53):

I could probably live with "pseudoproposition".

Mike Shulman (Apr 05 2023 at 20:53):

It does have an unfortunate meaning in ordinary English, however.

Reid Barton (Apr 05 2023 at 20:55):

And pseudo- is sort of overloaded as it is.

Reid Barton (Apr 05 2023 at 20:56):

But the idea is that a pseudoequivalence relation is like an equivalence relation, except valued in pseudopropositions rather than propositions.

Mike Shulman (Apr 05 2023 at 21:00):

Yes. But, as you say, "pseudo" also has the meaning in category theory of "up to isomorphism", so maybe "pseudo-equivalence relation" is not the best terminology to be generalizing from.

Mike Shulman (Apr 05 2023 at 21:03):

In the terminology of my paper The derivator of setoids (which comes from the theory of derivators), a logical equivalence can be called a "$\rm Set_{pos}$-equivalence", the idea being that it becomes an equivalence in $\rm Set_{pos}$, the poset reflection of $\rm Set$.