Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 17th 2014
   • (edited Feb 17th 2014)
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI was thinking last week when I introduced the first year philosophy students to material implication that HoTT (or at least dependent type theory) might ease their pain. The trouble they have is with the truth-functional interpretation of $A$ implies $B$, $A \to B$. Hearing that if either $A$ is true or $B$ is false, they should say $A \to B$ is true is bewildering. E.g., * (a) 2 + 2 = 4 implies London is in the UK * (b) 2 + 2 = 5 implies London is in the UK * (c) 2 + 2 = 5 implies London is in France are all true. Clearly, one needs to suggest to them that there are functions taking any proof of the antecedent to a proof of the consequent. In case (a), the constant function does; if cases (b) and (c), we choose the unique function from the empty set. Using 'implies' in these situations seems odd, since we expect a connection. Presumably we expect there to be some further structure shared between propositions, for example, as when there is a dependency which has been realised at a constant. So we might have $$ x : A \vdash B(x), C(x): Type $$ then $$ x: A \vdash (B(x) \to C(x)) : Type. $$ If then we have $$ x: A \vdash f(x) : (B(x) \to C(x)), $$ then $$ f(a): (B(a) \to C(a)). $$ As you may imagine there's a vast [literature](http://plato.stanford.edu/entries/conditionals/) on the adequacy or inadequacy of material implication for all kinds of if-then situation, such as counterfactuals: >I was caught in traffic. If I had taken the train, then I would have been on time. Some want to take this in a modal direction, e.g., by thinking of close possible worlds. In the nearest possible world in which I take the train, I am on time. Do we have any clever things to say about such things? I guess there was some kind of generalisation operating about people taking the train, taking a certain amount of time. Plugging this into my case, then with that amount of time, I wouldn't have been late.

   I was thinking last week when I introduced the first year philosophy students to material implication that HoTT (or at least dependent type theory) might ease their pain. The trouble they have is with the truth-functional interpretation of $A$ implies $B$, $A \to B$. Hearing that if either $A$ is true or $B$ is false, they should say $A \to B$ is true is bewildering. E.g.,

   • (a) 2 + 2 = 4 implies London is in the UK
   • (b) 2 + 2 = 5 implies London is in the UK
   • (c) 2 + 2 = 5 implies London is in France

   are all true.

   Clearly, one needs to suggest to them that there are functions taking any proof of the antecedent to a proof of the consequent. In case (a), the constant function does; if cases (b) and (c), we choose the unique function from the empty set.

   Using ’implies’ in these situations seems odd, since we expect a connection. Presumably we expect there to be some further structure shared between propositions, for example, as when there is a dependency which has been realised at a constant.

   So we might have

   $$x : A \vdash B(x), C(x): Type$$

   then

   $$x: A \vdash (B(x) \to C(x)) : Type.$$

   If then we have

   $$x: A \vdash f(x) : (B(x) \to C(x)),$$

   then

   $$f(a): (B(a) \to C(a)).$$

   As you may imagine there’s a vast literature on the adequacy or inadequacy of material implication for all kinds of if-then situation, such as counterfactuals:

   I was caught in traffic. If I had taken the train, then I would have been on time.

   Some want to take this in a modal direction, e.g., by thinking of close possible worlds. In the nearest possible world in which I take the train, I am on time. Do we have any clever things to say about such things? I guess there was some kind of generalisation operating about people taking the train, taking a certain amount of time. Plugging this into my case, then with that amount of time, I wouldn’t have been late.

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeFeb 17th 2014
   • (edited Feb 17th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI'd think that the bewilderment here is dealt with by "constructivism". Because what is bewildering about inhabiting the type "2+2=4 implies that London is in the UK" with a term is that this term is not constructed in an elementary way from term forming rules, but is really constructed using an oracle that hands you an inhabitant of "London is in the UK" (say when you build that constant function that you mention: before you construct that, you need an oracle to hand you the term that your function is constant on). That's what makes it different from "2+2=4 implies that 2+3=5" where there is only an elementary construction rule being applied, not an oracle.

   I’d think that the bewilderment here is dealt with by “constructivism”.

   Because what is bewildering about inhabiting the type “2+2=4 implies that London is in the UK” with a term is that this term is not constructed in an elementary way from term forming rules, but is really constructed using an oracle that hands you an inhabitant of “London is in the UK” (say when you build that constant function that you mention: before you construct that, you need an oracle to hand you the term that your function is constant on).

   That’s what makes it different from “2+2=4 implies that 2+3=5” where there is only an elementary construction rule being applied, not an oracle.

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 17th 2014
   • (edited Feb 17th 2014)
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexIs an oracle the best language? Can't I just complain that whatever I'm given, I throw away, and use what I already have? Imagine I already have $$ \vdash P : Type, p : P, q: IsProp(P), S: Type. $$ Presumably I'm allowed $$ x : S \vdash p : P, $$ so I have $$ \vdash (x \mapsto p) : (S \to P), $$ without actually constructing a term in $S$.

   Is an oracle the best language? Can’t I just complain that whatever I’m given, I throw away, and use what I already have?

   Imagine I already have

   $$\vdash P : Type, p : P, q: IsProp(P), S: Type.$$

   Presumably I’m allowed

   $$x : S \vdash p : P,$$

   so I have

   $$\vdash (x \mapsto p) : (S \to P),$$

   without actually constructing a term in $S$.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 17th 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexYes, constructivism doesn't help with this sort of "irrelevance to premise". However, *linearity* does help!

   Yes, constructivism doesn’t help with this sort of “irrelevance to premise”. However, linearity does help!

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeFeb 18th 2014
   • (edited Feb 18th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItex.

   .

6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeFeb 18th 2014
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexYou can also try the trick attributed to Russell when reportedly asked to prove that he was the Pope, on the assumption that 1 = 2: ‘The Pope and I are two. Therefore, the Pope and I are one.’. You can run any ex-falso-quodlibet through some elementary finite-set theory in this way.

   You can also try the trick attributed to Russell when reportedly asked to prove that he was the Pope, on the assumption that 1 = 2: ‘The Pope and I are two. Therefore, the Pope and I are one.’. You can run any ex-falso-quodlibet through some elementary finite-set theory in this way.

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeFeb 18th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexI had posted a reply above and then canceled it because I am not sure if I want to be distracted by this. But now that I need a minute of procrastination, I'll give in. David, re #3: your line "Imagine I already have" is what I was referring to as "an oracle": if $p \colon P$ falls from the sky or else you have constructed it earlier already and forgotten how you did it then you can use it. What makes the resulting deductions seem bewildering is that you forgot how the $p$ came about. In your original example, there is the secret assumption that we have already figured out that London is in the UK. Then we forget how we did this and are left with just heavenly inspiration, we just know its true, even though we forget why. That's what makes the implication then bewildering. We just know its true, so we keep being able to deduce it whatever. But if you keep the whole construction of the proof that London is in the UK in the context, then the implication is not bewildering anymore.

   I had posted a reply above and then canceled it because I am not sure if I want to be distracted by this.

   But now that I need a minute of procrastination, I’ll give in.

   David, re #3:

   your line “Imagine I already have” is what I was referring to as “an oracle”: if $p \colon P$ falls from the sky or else you have constructed it earlier already and forgotten how you did it then you can use it. What makes the resulting deductions seem bewildering is that you forgot how the $p$ came about.

   In your original example, there is the secret assumption that we have already figured out that London is in the UK. Then we forget how we did this and are left with just heavenly inspiration, we just know its true, even though we forget why. That’s what makes the implication then bewildering. We just know its true, so we keep being able to deduce it whatever. But if you keep the whole construction of the proof that London is in the UK in the context, then the implication is not bewildering anymore.

8. • CommentRowNumber8.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 18th 2014
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI see. But I still think my students are bemused in this case even if they remember clearly how to prove the consequent. I think in ordinary language we take 'implies' to suggest relevance. One consideration concerns conversational norms. If you tell me 'P or Q', and I later found out that you knew P to be false and Q to be true, I can accuse you of being misleading. I don't tell someone that Prof. Jones is either in the lecture hall or in his office, if I know he's in his office. Similarly $P \to Q$ is weaker than $Q$, so odd to assert it if you already know $Q$.

   I see. But I still think my students are bemused in this case even if they remember clearly how to prove the consequent. I think in ordinary language we take ’implies’ to suggest relevance.

   One consideration concerns conversational norms. If you tell me ’P or Q’, and I later found out that you knew P to be false and Q to be true, I can accuse you of being misleading. I don’t tell someone that Prof. Jones is either in the lecture hall or in his office, if I know he’s in his office. Similarly $P \to Q$ is weaker than $Q$, so odd to assert it if you already know $Q$.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeFeb 18th 2014
   • (edited Feb 18th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexIf this is about real world examples, then I would suggest this: I hand out a multiple choice test to students. One student asks me: "Is there maybe a mistake in question A? Since it seems to me that no choice is right." I reply: "No, either answer a) or b) is true." Even though I know it's a). Next another student asks me: "I don't understand how to answer question Q. Can this be solved with what we actually did in the course?" And I reply: "Yes, if you worked your way through to question P, then you have enough information to answer Q." Even though I know that they should be able to answer Q right away from what we had in class, even without thinking about P first. The class material is the context. Only if the students forget what we did in class will they find the multiple choice test bewildering. :-)

   If this is about real world examples, then I would suggest this:

   I hand out a multiple choice test to students.

   One student asks me: “Is there maybe a mistake in question A? Since it seems to me that no choice is right.” I reply: “No, either answer a) or b) is true.” Even though I know it’s a).

   Next another student asks me: “I don’t understand how to answer question Q. Can this be solved with what we actually did in the course?” And I reply: “Yes, if you worked your way through to question P, then you have enough information to answer Q.” Even though I know that they should be able to answer Q right away from what we had in class, even without thinking about P first.

   The class material is the context. Only if the students forget what we did in class will they find the multiple choice test bewildering.

   :-)

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 18th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI think #1 is right that propositions-as-types is a good explanation. There's nothing wrong with a function that doesn't use its argument.

    I think #1 is right that propositions-as-types is a good explanation. There’s nothing wrong with a function that doesn’t use its argument.

11. • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 20th 2014
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexThere are two things that go into defining material implication: that it's a function on truth values alone, and which function it is. The first part is why we ignore issues of relevance, likelihood, and so on. It has to be frankly admitted that material implication is used in logic for the purposes of logic, and it simply does not capture or attempt to capture all of what ‘if’ means in a natural language. As for the second part, you can get the true parts by examining a statement such as ‘If $x = 3$, then $x^2 = 9$.’, noting that this sounds true, and claiming that you want it to be true no matter what you put in for $x$. On the other hand, ‘If $x^2 = 9$, then $x = 3$.’ sounds false, but we do allow it to be true for certain values of $x$. One or the other must give to have a function of truth values, so to decide which we have to consider how we want to use implication (as with modus ponens). We must be able to rely on the first statement's being true; we don't need to rely on the second statement's being false.

    There are two things that go into defining material implication: that it’s a function on truth values alone, and which function it is. The first part is why we ignore issues of relevance, likelihood, and so on. It has to be frankly admitted that material implication is used in logic for the purposes of logic, and it simply does not capture or attempt to capture all of what ‘if’ means in a natural language.

    As for the second part, you can get the true parts by examining a statement such as ‘If $x = 3$, then $x^2 = 9$.’, noting that this sounds true, and claiming that you want it to be true no matter what you put in for $x$. On the other hand, ‘If $x^2 = 9$, then $x = 3$.’ sounds false, but we do allow it to be true for certain values of $x$. One or the other must give to have a function of truth values, so to decide which we have to consider how we want to use implication (as with modus ponens). We must be able to rely on the first statement’s being true; we don’t need to rely on the second statement’s being false.