Originally Posted by

**james121515** __THEOREM__: Let f : A -> B and g : B -> D. If g o f is one-to-one, [p ->....] then f is one-to-one.[...(q ->r)]

__PROOF:__ Suppose g o f is one-to-one. [Here we're supposing p] Suppose f(a1) = f(a2) = b. [Here we're supposing q] Since g : B ->D there exist d in D such that g(b) = d. So, g(f(a1)) = g(f(a2)) =d. Equivalently, (g o f)a1 = (g o f)a2. Since g o f is one-to-one, [here we're also supposing p, so p /\ q] a1 = a2

I added the text in blue to show where we assume the first premise p.

I am not sure about two things. When you say "here we're also supposing p", you don't mean that this supposition is done by the phrase "Since g o f is one-to-one", do you? We assumed p, which is "g o f is one-to-one", in the beginning of the proof.

Second, why do you say "so p /\ q"? During a proof, we may have multiple assumptions that are separate independent formulas. Suppose that we have three assumptions: P, Q, and R. As a set, they are equivalent to P /\ Q /\ R. Namely, we can prove P /\ Q /\ R from P, Q, R; we also can prove any of P, Q, and R from P /\ Q /\ R. There is relatively little difference between the two, so sometimes it makes sense to identify the set {P, Q, R} with P /\ Q /\ R and move implicitly from one to the other. However, formally they are different: one is a set of three formulas, the other a formula (or a set of one formula); to move from one to the other one has to use the rules called Simplification and Conjunction in this Wikipedia table.

Below I write some fun extension of this that you may ignore.

The universal quantifier behaves very similarly to implication. When we need to probe , we assume and prove . When we need to prove , we consider an arbitrary and prove . Conversely, when we know , we can combine it with to get . Similarly, when we know , we can combine it with some concrete to produce . The first two rules, regarding assumption, are called introduction rules: one of implication, and the other of universal quantifier.

The exact form of some theorem depends on how much we unfold definitions. The following are actual snippets from the automated proof assistant program that I used to prove this theorem. The theorem may look like

Code:

injective (g o f) -> injective f

If we unfold the second "injective", we get

Code:

injective (g o f) ->
forall x1 x2 : A,
f x1 = f x2 -> x1 = x2 (*)

((*) is a mark for the future.) It's not exactly of the form P -> (Q -> R), but, since forall and -> are very similar, it's close.

Now we can start use the introduction rules. After four rules, our proof state looks as follows:

Code:

H1 : injective (g o f)
x1 : A
x2 : A
H2 : f x1 = f x2
============================
x1 = x2

This means we have two formulas and two objects (x1 and x2) as assumptions.

If, for example, instead of (*) we start with

Code:

forall x1 x2 : A,
injective (g o f) ->
f x1 = f x2 -> x1 = x2

and perform all introductions, we end up with the same proof state as above. On the other hand, if we start with

Code:

forall x1 x2 : A,
injective (g o f) /\ f x1 = f x2 ->
x1 = x2

we get

Code:

x1 : A
x2 : A
H : injective (g o f) /\ f x1 = f x2
============================
x1 = x2

It's trivial to transform it again to

Code:

x1 : A
x2 : A
H1 : injective (g o f)
H2 : f x1 = f x2
============================
x1 = x2

Note that so far we took the sets A, B, C and functions f, g as fixed. If we quantify over then as well, we get the following theorem:

Code:

forall (A B C : Set) (f : A -> B)
(g : B -> C),
injective (g o f) -> injective f

And if, in addition, we unfold "injective", we get a whopping

Code:

forall (A B C : Set) (f : A -> B)
(g : B -> C),
(forall x1 x2 : A, (g o f) x1 = (g o f) x2 -> x1 = x2) ->
forall x1 x2 : A, f x1 = f x2 -> x1 = x2

If we introduce everything, we get

Code:

A : Set
B : Set
C : Set
f : A -> B
g : B -> C
H1 : forall x1 x2 : A, (g o f) x1 = (g o f) x2 -> x1 = x2
x1 : A
x2 : A
H2 : f x1 = f x2
============================
x1 = x2

Disclaimer: no animal suffered during these experimants. All computations were performed by a computer.