Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorehogle
   • CommentTimeFeb 26th 2018
   • PermaLink
   Author: ehogle
   Format: MarkdownItexI apologize in advance if this isn't the right venue for this question, but if someone could point me to the right venue, I'd appreciate it. However, on the off chance this _is_ the right venue, I'm trying to learn the basics of HoTT and I'm troubled by something I must not understand about the analogy between $A\to B$ in homotopy and $A\Rightarrow B$ in logic: Suppose I know that propositions $A$ and $B$ are true, that is I have $a:A$ and $b: B$. I can construct (introduce?) $f:A\to B$ by $\lambda x.b$. Should I therefore conclude that $A\Rightarrow B$? It seems like I've just claimed "any two true propositions imply one another." Where am I going astray?

   I apologize in advance if this isn’t the right venue for this question, but if someone could point me to the right venue, I’d appreciate it.

   However, on the off chance this is the right venue, I’m trying to learn the basics of HoTT and I’m troubled by something I must not understand about the analogy between $A\to B$ in homotopy and $A\Rightarrow B$ in logic:

   Suppose I know that propositions $A$ and $B$ are true, that is I have $a:A$ and $b: B$. I can construct (introduce?) $f:A\to B$ by $\lambda x.b$. Should I therefore conclude that $A\Rightarrow B$? It seems like I’ve just claimed “any two true propositions imply one another.”

   Where am I going astray?

2. • CommentRowNumber2.
   • CommentAuthorehogle
   • CommentTimeFeb 26th 2018
   • (edited Feb 26th 2018)
   • PermaLink
   Author: ehogle
   Format: MarkdownItexNevermind! I didn't actually use $a:A$, and I'm leaning too hard on "implies." Really, if I know $B$ is true, then "If $A$ then $B$" is valid for any $B$. Even if $A=\emptyset$, my $f$ above is just the empty function, and _ex falso quodlibet_. Is that right?

   Nevermind!

   I didn’t actually use $a:A$, and I’m leaning too hard on “implies.” Really, if I know $B$ is true, then “If $A$ then $B$” is valid for any $B$. Even if $A=\emptyset$, my $f$ above is just the empty function, and ex falso quodlibet.

   Is that right?

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 26th 2018
   • (edited Feb 26th 2018)
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexYes, that's the idea. But a dependent type theory such as HoTT offers greater riches. You may have a proposition $B(x)$, depending on some type $A$, and then an element of $\prod_{x:A}B(x)$ may detect the relevance of the truth of $A$ for the truth of $B$. You may like to see some [slides](https://ncatlab.org/davidcorfield/files/AndTalk2.pdf) (aimed more at $\sum_{x:A}B(x)$, so 'and', though it does end with 'implies').

   Yes, that’s the idea.

   But a dependent type theory such as HoTT offers greater riches. You may have a proposition $B(x)$, depending on some type $A$, and then an element of $\prod_{x:A}B(x)$ may detect the relevance of the truth of $A$ for the truth of $B$. You may like to see some slides (aimed more at $\sum_{x:A}B(x)$, so ’and’, though it does end with ’implies’).

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeFeb 26th 2018
   • (edited Feb 26th 2018)
   • PermaLink
   Author: Urs
   Format: MarkdownItexYes, type dependency makes the difference. It is a common theme that people complain that the truth table for implication in classical logic courses | $P \Rightarrow Q$ | $P = true$ | $P = false$ | |-------------------------|--------------|---------------| | $Q = true$ | true | true | | $Q = false$ | false | true | conveys nothing of the actual idea of implication. The resolution is that the actual idea of implication is secretly one in dependent type theory, and that it collapses to the above boring truth table only in the "absolute context", which is a degenerate case that is not what one typically has in mind, implicitly, when thinking of the concept of "implication".

   Yes, type dependency makes the difference.

   It is a common theme that people complain that the truth table for implication in classical logic courses

   $P \Rightarrow Q$	$P = true$	$P = false$
   $Q = true$	true	true
   $Q = false$	false	true

   conveys nothing of the actual idea of implication.

   The resolution is that the actual idea of implication is secretly one in dependent type theory, and that it collapses to the above boring truth table only in the “absolute context”, which is a degenerate case that is not what one typically has in mind, implicitly, when thinking of the concept of “implication”.

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 26th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexA problem which is *not helped* by the common practice of "implicit universal quantification" (i.e. writing "if P(x) then Q(x)" to mean "for all x, if P(x) then Q(x)") *even in "introduction to proof" textbooks*! </rant> Although there are also other approaches to this "problem" (if one consideres it a problem) such as [[relevance logic]].

   A problem which is not helped by the common practice of “implicit universal quantification” (i.e. writing “if P(x) then Q(x)” to mean “for all x, if P(x) then Q(x)”) even in “introduction to proof” textbooks! </rant>

   Although there are also other approaches to this “problem” (if one consideres it a problem) such as relevance logic.

6. • CommentRowNumber6.
   • CommentAuthorehogle
   • CommentTimeFeb 27th 2018
   • (edited Feb 27th 2018)
   • PermaLink
   Author: ehogle
   Format: MarkdownItexThanks! I like this idea that a dependent type could capture an implication in a way that's sensitive to $x:A$. Definitely closer to the idea of implication as we use it colloquially if the reason $x:A$ that $A$ is true affects the reason we conclude $B$.

   Thanks! I like this idea that a dependent type could capture an implication in a way that’s sensitive to $x:A$. Definitely closer to the idea of implication as we use it colloquially if the reason $x:A$ that $A$ is true affects the reason we conclude $B$.

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeFeb 27th 2018
   • PermaLink
   Author: Urs
   Format: MarkdownItex> if the reason $x$ is true affects the reason we conclude $B$. Just to amplify, it's: "...if the reason $x$ that $A$ is true entails a reason $f(x)$ that $B$ is true".

   if the reason $x$ is true affects the reason we conclude $B$.

   Just to amplify, it’s:

   “…if the reason $x$ that $A$ is true entails a reason $f(x)$ that $B$ is true”.

8. • CommentRowNumber8.
   • CommentAuthorehogle
   • CommentTimeFeb 27th 2018
   • PermaLink
   Author: ehogle
   Format: MarkdownItexOh, yeah, I was definitely missing some words there. Thank you. So this dependent-type-as-a-richer-version-of-implies seems to have more subtlety than I realized at first. As a toy example, say $A$ has two points, $a_1$ and $a_2$. Then $\sum_{x:A}B(x)=B(a_1)\sqcup B(a_2)$. Suppose $B(a_1)=B$ (or maybe just $B(a_1)\subseteq B$?) while $B(a_2)=\emptyset$. Then I can know $A$ is true because I know $a_2:A$, and yet conclude nothing about $B$, while on the other hand if I know $A$ because of $a_1:A$ then I have $f(a_1):B(a_1)$ telling me B. Is this right? I can have one proposition implying another in a "well, it depends how you know" way? It's also possible I've completely misunderstood what you meant by $f$.

   Oh, yeah, I was definitely missing some words there. Thank you.

   So this dependent-type-as-a-richer-version-of-implies seems to have more subtlety than I realized at first. As a toy example, say $A$ has two points, $a_1$ and $a_2$.

   Then $\sum_{x:A}B(x)=B(a_1)\sqcup B(a_2)$. Suppose $B(a_1)=B$ (or maybe just $B(a_1)\subseteq B$?) while $B(a_2)=\emptyset$. Then I can know $A$ is true because I know $a_2:A$, and yet conclude nothing about $B$, while on the other hand if I know $A$ because of $a_1:A$ then I have $f(a_1):B(a_1)$ telling me B.

   Is this right? I can have one proposition implying another in a “well, it depends how you know” way?

   It’s also possible I’ve completely misunderstood what you meant by $f$.

9. • CommentRowNumber9.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 27th 2018
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI'd recommend taking a look at [[propositions as types]]. You'll see that there's one approach called 'proposition as some types', where we take a special class of types, called [[mere propositions]], which have at most one element. Your $A$ above can't be a mere proposition, since $B(a_1)$ is not equivalent to $B(a_2)$. If $A$ is a set with multiple elements, then it won't be a surprise that the $B(a_i)$ may differ.

   I’d recommend taking a look at propositions as types. You’ll see that there’s one approach called ’proposition as some types’, where we take a special class of types, called mere propositions, which have at most one element.

   Your $A$ above can’t be a mere proposition, since $B(a_1)$ is not equivalent to $B(a_2)$.

   If $A$ is a set with multiple elements, then it won’t be a surprise that the $B(a_i)$ may differ.