reverting two implications in a hypothesis

Stream: new members

[Kwame Porter Robinson]

(deleted)

[Kwame Porter Robinson]

I'm a newbie; I have a hypothesis like so h : k ≠ 0 → k * b = k * c → b = c and was wondering if I could split it into two hypotheses, h1 : k ≠ 0 → k * b = k * c and h2 : k * b = k * c → b = c. Splitting h would allow me to apply the implications of hypothesis h more selectively, e..g apply h1

[Eric Rodriguez]

this isn't true in general - look at your h2, for example, with k = 0!

[Stuart Presnell]

More generally, for any types A, B, and C, the type A → B → C is A → (B → C), meaning that a function f : A → B → C takes in a term a : A as input and returns a function f(a) : B → C as output. If you can provide a further term b : B to this function then you get f(a)(b) : C.

[Stuart Presnell]

In your case where the types are propositions, your term h : k ≠ 0 → k * b = k * c → b = c says the following: if you can provide a proof of k ≠ 0 and a proof of k * b = k * c, then I'll give you a proof of b = c.

[Stuart Presnell]

So you should read something of the form A → B → C as saying "A and B together imply C". But this isn't the same as "A implies B and also B implies C".

[Stuart Presnell]

In a lot of areas of mathematics (such as category theory) we often draw diagrams where arrows are chained together: if we have an arrow from some thing X to some thing Y and an arrow from Y to Z, we can compose them to make an arrow from X to Z that we might draw like X → Y → Z. But that's NOT what's going on here!

[Stuart Presnell]

This notation — writing A → B → C when we mean A → (B → C) — can be confusing at first, and you might well think that we should just put in the brackets to be clear about what we mean. But in practice it turns out to be useful to write functions in this way: for a function that takes a lot of inputs, we can write its type as A → B → C → D → ... → Z without piling up loads of brackets.