What does "provably equal" mean?

[andrejbauer]

There are three occurences of the phrase "provably equal". What is that supposed to mean? They were all written by Mike and appear as follows:

1. basics-equivalences.tex: For instance, for a single function $f:A\to B$ there may be multiple inhabitants of~\eqref{eq:qinvtype} which are not provably equal.
2. basics.tex: It's not hard to show that these three elements would be (provably) \emph{equal} (see \autoref{ex:basics:concat}), but there can still be reasons to prefer a particular definition over a provably equal one.
3. introduction.tex: Type-theoretically, this means there are many paths that are \emph{provably} equal to reflexivity, but not definitionally so.

Computer scientists sometime use "provably" when they really mean "we proved it", and that is quite awful. Let us not do that (if that is what we are doing). In any case, as we are not playing games with models, I do not see how we can meaningfully say "provable" (as opposed to "true"). At best we can point out that we actually have a proof of something, bu that is "proved", not "provable".

[mikeshulman]

I think what I meant in all three cases was "propositionally" (i.e. for emphasis, not judgmentally). Feel free to change them.

[andrejbauer]

Is "propositionally equal" the official way of saying it?

[mikeshulman]

I've written that in a couple of other places, but I suppose we could argue about that too. Certainly that isn't the only phrase we use; we also say things like "equal" (if no emphasis is needed), "connected by a path to", "can be identified with". I'm not sure we should try to restrict ourselves to only one way of saying it. I suppose "propositionally equal" may be confusing because it doesn't refer to a mere proposition; perhaps that is what motivated me to write "provably" instead.

[awodey]

for a while, following PAT we were saying that Id(a,b) is the "type of proofs that a = b", so in those terms, "provably equal" meant that Id(a, b) is inhabited.
It does make sense, but it relies on the difference "provable / true" to explain the difference "propositional / judgmental" equality, which I agree is not ideal.

the current approach is to call Id(a,b) is the "type of identifications between a and b", and to talk about propositional equality "identifying" two things.

the two notions of equality are being called "propositional / judgmental" equality, the latter replacing the former term "definitional equality".
this is not ideal either, but i don't have a better solution and we've been over it so many times that I'm too weary to reconsider it.

On Mar 6, 2013, at 9:05 AM, Andrej Bauer notifications@github.com wrote:

Is "propositionally equal" the official way of saying it?

—
Reply to this email directly or view it on GitHub.

[mikeshulman]

We could probably avoid it in the three cases you mention.

1. For instance, for a single function $f:A\to B$ there may be multiple unequal inhabitants of~\eqref{eq:qinvtype}.
2. It's not hard to show that these three elements can be identified (see \autoref{ex:basics:concat}), but as they are not definitionally equal, there can still be reasons to prefer one over another.
3. Type-theoretically, this means there are many paths that can be identified with reflexivity, but are not judgmentally equal to it.

[RobertHarper]

being a computer scientist, i have to agree with andrej that saying "provably equal" really rubs me up the wrong way. there is another issue, though, which is the common misunderstanding of what is meant by a "provably" in the constructive context vs what is meant in metamathematics. in the latter case one is talking about a fixed formal system to which goedelian considerations apply, but in the former we most definitely are not. this distinction has caused a lot of confusion in my experience, so i suggest we avoid saying "provably" if at all possible.

bob

On Mar 6, 2013, at 9:02 AM, Andrej Bauer wrote:

There are three occurences of the phrase "provably equal". What is that supposed to mean? They were all written by Mike and appear as follows:

basics-equivalences.tex: For instance, for a single function $f:A\to B$ there may be multiple inhabitants of~\eqref{eq:qinvtype} which are not provably equal.
basics.tex: It's not hard to show that these three elements would be (provably) \emph{equal} (see \autoref{ex:basics:concat}), but there can still be reasons to prefer a particular definition over a provably equal one.
introduction.tex: Type-theoretically, this means there are many paths that are \emph{provably} equal to reflexivity, but not definitionally so.
Computer scientists sometime use "provably" when they really mean "we proved it", and that is quite awful. Let us not do that (if that is what we are doing). In any case, as we are not playing games with models, I do not see how we can meaningfully say "provable" (as opposed to "true"). At best we can point out that we actually have a proof of something, bu that is "proved", not "provable".

—
Reply to this email directly or view it on GitHub.

[RobertHarper]

btw, in the proof of theorem 2.8.1, it seems that "…(x)" should be "…(u)" on the left-hand side of the last displayed equation on the page on the march 6 version.

bob

[RobertHarper]

I know that I may be stirring a hornet's nest, but I want to object to the following sentence:

"We want to avoid treating as logical propositions those types for which giving an element of them gives more information than simply knowing that the type is inhabited."

There's an old joke involving Tonto and the Lone Ranger whose punch line is "What do you mean 'we' kimosabe?". I, at least, absolutely do want to treat as logical propositions types with structure, such as sum types expressing disjunction and sigma types expressing constructive existence!

Bob

[mikeshulman]

I originally wrote that sentence as "What we want to avoid are types for which giving an element of them gives more information than simply knowing that the type is inhabited", intending it to be interpreted in the context of the desire to "obtain a more classical logic" referred to in the previous paragraph. How do you feel about that?

[RobertHarper]

sounds better to me. the subsequent discussion, which i read only after my note, is very good.

btw there is a certain dissonance in calling the equality type "propositional equality" after a discussion that suggests that propositional things are -1-types.

best,
bob

On Mar 6, 2013, at 12:43 PM, Mike Shulman wrote:

I originally wrote that sentence as "What we want to avoid are types for which giving an element of them gives more information than simply knowing that the type is inhabited", intending it to be interpreted in the context of the desire to "obtain a more classical logic" referred to in the previous paragraph. How do you feel about that?

—
Reply to this email directly or view it on GitHub.

[awodey]

Sent from my iPhone

On Mar 6, 2013, at 12:50 PM, Robert Harper notifications@github.com wrote:

sounds better to me. the subsequent discussion, which i read only after my note, is very good.

btw there is a certain dissonance in calling the equality type "propositional equality" after a discussion that suggests that propositional things are -1-types.

Good point

best,
bob

On Mar 6, 2013, at 12:43 PM, Mike Shulman wrote:

I originally wrote that sentence as "What we want to avoid are types for which giving an element of them gives more information than simply knowing that the type is inhabited", intending it to be interpreted in the context of the desire to "obtain a more classical logic" referred to in the previous paragraph. How do you feel about that?

—
Reply to this email directly or view it on GitHub.

—
Reply to this email directly or view it on GitHub.