Skip to content
Axiomatic Wiki
Theorem·T52

The pairing function is injective

Distinct pairs of naturals always encode to distinct naturals - omega squared is countable.

The pairing function is an injection: for , if then .
In words
The pairing function is whenever two inputs give the same output forced to have been the same pair to begin with - the defining property of an injection.
Rests onF02F03F04F06F08F09F11F12F14A01A06A08
Never needed: F05 · F10 · F13 · A02 · A03 · A04 · A05 · A07 · A09 (computed from the citation graph, not asserted).

Proof

  1. 1
    Write , . Note and (L17, adding a natural to resp. ).
  2. 2
    . By trichotomy, suppose toward a contradiction . By the gap clause of T51 (with ): . Since means (L15), the monotonicity clause of T51 (or equality if ) gives . Adding : (L17). Chaining: , contradicting . Symmetrically also contradicts the hypothesis. By L16, .
  3. 3
    . With : , so gives ; cancelling (cancellation of addition) gives .
  4. 4
    . With and : ; cancelling gives .
∎

Remarks

Since injects into , , i.e. is countable (D050 is exactly this domination). This is the base case for showing alphabets, terms, and formulas over a countable language are all countable - the raw material Lindenbaum's lemma enumerates to build a maximal consistent extension.
Wikipedia ↗Nat.pair ↗

Used by

T53T54
Propose an edit1 published revision