1
$\begingroup$

I've been reading on type theory, and it being a possible foundation of mathematics. I have to say it is all very abstract to me. I'm very used to using set theory to think about mathematical proofs, but I find it very hard to imagine using type theory to think about mathematical proofs (I hardly understand type theory yet btw).

So in order to make it less abstract and more concrete: Can you give an example of a mathematical proof, and how it would be formalized in type theory, rather than in set theory?

For example, let's take the proposition:

Proposition. Let $x$ be a real number and $x_n$ a sequence of real numbers. Let $f$ be a function continuous at $x$). Then if $x_n$ converges to $x$, then $f(x_n)$ converges to $f(x)$.

The way I think about proving this formally, would be to state first the definition of $x_n$ converging to $x$: $$\forall \epsilon_{\in\mathbb R},\exists N_{\in \mathbb N},\forall n_{\in \mathbb N}:\left[(e>0 \land n>N)\implies|x_n-x|<\epsilon\right]$$

Then we can do the same for continuity of $f$. And then we simply apply some basic deductive axioms to get to the conclusion. I won't write down all the steps because you can imagine what it looks like.

I however, cannot imagine what the equivalent process would look like for type theory. Can you show how you would prove this theorem (or any other simpler theorem) formally using type theory rather than set theory and first order logic?

$\endgroup$
4
  • $\begingroup$ You might be interested in the later chapters of the HoTT book, and in particular chapters 10 (Set theory) and 11 (Real numbers) which is available at homotopytypetheory.org/book $\endgroup$
    – neptun
    Dec 12 '17 at 10:47
  • $\begingroup$ I hope you may be interested in this. Also, see here: math.stackexchange.com/questions/612122/… $\endgroup$
    – user371838
    Dec 12 '17 at 10:49
  • $\begingroup$ You might note that prop 11.3.39 of the HoTT book uses your proposition as a definition of continuous, so your particular example won't be proven therein! $\endgroup$
    – neptun
    Dec 12 '17 at 10:53
  • 1
    $\begingroup$ Everything in the Coq libraries, the Agda libraries, the NuPRL libraries is an example of a (truly) formal proof in an intuitionistic type theory. Then everything in the Isabelle/HOL, HOL4, HOL Light libraries are examples in a non-dependent type theory. I'd be a bit surprised if you've actually seen a truly formal, i.e. machine-checked, set theoretic proof. MetaMath, TLAPS, and Mizar (though that's a bit ambiguous) would provide examples. $\endgroup$ Dec 14 '17 at 1:23
2
$\begingroup$

Can you give an example of a mathematical proof, and how it would be formalized in type theory, rather than in set theory?

Here is an example of a simple proof in Coq, which is based on dependent type theory.

Lemma pow_add : forall (x:R) (n m:nat), x ^ (n + m) = x ^ n * x ^ m.
Proof.
  intros x n; elim n; simpl; auto with real.
  intros n0 H' m; rewrite H'; auto with real.
Qed.

And here is a longer proof of a different lemma:

Lemma poly : forall (n:nat) (x:R), 0 < x -> 1 + INR n * x <= (1 + x) ^ n.
Proof.
  intros; elim n.
  simpl; cut (1 + 0 * x = 1).
  intro; rewrite H0; unfold Rle; right; reflexivity.
  ring.
  intros; unfold pow; fold pow;
    apply
      (Rle_trans (1 + INR (S n0) * x) ((1 + x) * (1 + INR n0 * x))
        ((1 + x) * (1 + x) ^ n0)).
  cut ((1 + x) * (1 + INR n0 * x) = 1 + INR (S n0) * x + INR n0 * (x * x)).
  intro; rewrite H1; pattern (1 + INR (S n0) * x) at 1;
    rewrite <- (let (H1, H2) := Rplus_ne (1 + INR (S n0) * x) in H1);
      apply Rplus_le_compat_l; elim n0; intros.
  simpl; rewrite Rmult_0_l; unfold Rle; right; auto.
  unfold Rle; left; generalize Rmult_gt_0_compat; unfold Rgt;
    intro; fold (Rsqr x);
      apply (H3 (INR (S n1)) (Rsqr x) (lt_INR_0 (S n1) (lt_O_Sn n1)));
        fold (x > 0) in H;
          apply (Rlt_0_sqr x (Rlt_dichotomy_converse x 0 (or_intror (x < 0) H))).
  rewrite (S_INR n0); ring.
  unfold Rle in H0; elim H0; intro.
  unfold Rle; left; apply Rmult_lt_compat_l.
  rewrite Rplus_comm; apply (Rle_lt_0_plus_1 x (Rlt_le 0 x H)).
  assumption.
  rewrite H1; unfold Rle; right; trivial.
Qed.

Coq allows you to define tactics (like the rewrite and intros tactics above), which help you do the proof. They have a bunch of built in ones as well.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.