Discussion of i2forge

Stream: general

[Bulhwi Cha]

In my heavily biased opinion, code written with a beginner-friendly proof assistant should be as readable as the following one:

Theorem Syllogism (φ ψ χ: wff)
  Hypotheses
    hyp1: φ → ψ
    hyp2: ψ → χ
  Assertion
    syl: φ → χ
  Proof
    phi: φ
      psi: ψ := ax_mp hyp1 phi
      chi: χ := ax_mp hyp2 psi
    syl: φ → χ := →I phi chi

[Scott Morrison]

I'm not sure that ax_mp and →I count as readable. Nor the strange repetition of variations, once in unicode, once spelled out.

[Bulhwi Cha]

Hmm, then how about this one?

Theorem Syllogism (φ ψ χ: wff)
  Hypotheses
    hyp1: φ → ψ
    hyp2: ψ → χ
  Assertion
    syl: φ → χ
  Proof
    hyp3: φ
      step3.1: ψ := modus_ponens hyp1 hyp3
      step3.2: χ := modus_ponens hyp2 step3.1
    syl: φ → χ := →_intro hyp3 step3.2

[Johan Commelin]

But this is miles away from how maths is taught and learned and practiced in maths departments.

[Mario Carneiro]

it is closer to how it is taught in logic class though

[Mario Carneiro]

although I don't think they get as far as syntax for proofs

[Johan Commelin]

I never took a logic course for my maths studies

[Mario Carneiro]

I certainly don't find that style particularly easy to write though, and I think it is important to acknowledge that math presentation is a very different task from proof construction

[Kevin Buzzard]

Mathematicians are expected to pick up classical logic (where all proofs are tauto!) by osmosis and are never taught things like natural deduction. At least this is how it works in most maths departments.

[Mario Carneiro]

I think this kind of approach would favor more the isabelle style of "statement, by hammer; statement, by hammer"

[Bulhwi Cha]

Johan Commelin said:

I never took a logic course for my maths studies

I used to strongly argue that we should teach formal logic to students who major in math or CS. Now I'm a little more cautious about saying it.

[Notification Bot]

11 messages were moved here from #announce > Help us build a platform for mathematicians by Johan Commelin.

[Notification Bot]

This topic was moved here from #announce > Discussion of i2forge by Johan Commelin.

[Bulhwi Cha]

Mario Carneiro said:

I certainly don't find that style particularly easy to write though, and I think it is important to acknowledge that math presentation is a very different task from proof construction

Right, this style would be tedious to write.

[Bulhwi Cha]

Kevin Buzzard said:

Mathematicians are expected to pick up classical logic (where all proofs are tauto!) by osmosis and are never taught things like natural deduction. At least this is how it works in most maths departments.

I assume most of them are also never taught things like dependent types or inductive types.

[Scott Morrison]

I've never seen dependent or inductive types taught in a math(s) department, outside of weird things like people teaching Lean. :-) Mathematicians are often weirded out by the idea you can do induction on anything except natural numbers!

[Kevin Buzzard]

In fact I'm not sure I've ever had to do induction on anything except natural numbers in my 25 years as a...erm... number theorist.

[Shreyas Srinivas]

Scott Morrison said:

I've never seen dependent or inductive types taught in a math(s) department, outside of weird things like people teaching Lean. :-) Mathematicians are often weirded out by the idea you can do induction on anything except natural numbers!

Ask graph theory folks

[Shreyas Srinivas]

On second thoughts, a lot of induction proofs in graph theory might be induction proofs on natural numbers so I take that back

[Mario Carneiro]

Even in logic / proof theory, the poster child for induction on syntax, you will see many proofs going by induction on the length or size of the formula instead, just to avoid introducing the concept of induction on syntax directly

[Mario Carneiro]

and borel sets, a canonical example of an inductively defined collection of subsets, is instead phrased as a transfinite induction on ordinals which iterates an operation aleph_1 times

[Mario Carneiro]

The only mathematical community I know that does induction on syntax without batting an eye is the PL theory community (also type theory, but those folks are pretty counter-cultural in other ways as well)

[Jireh Loreaux]

Several years ago now there was a blog post on the Math StackExchange called When can we do induction, and I thought it was common knowledge among mathematicians that you can do induction on well-founded orders.

Of course, now I realize that Mario is definitely aware of that post, seeing as he commented on it at the time!

[Jireh Loreaux]

I've always considered that the proof of the Fundamental Theorem of Arithmetic should proceed by induction on the well-founded order of divisibility.

[Yaël Dillies]

strict divisibility :grinning:

[Kevin Buzzard]

yeah but induction on number of prime factors works fine.

[Jireh Loreaux]

Sorry Kevin, I meant the existence portion. When I'm introducing my students to strong induction, I always use "every (n : ℕ) > 1 is the product of primes" as the canonical example where using the usual induction on n is insufficient and instead you need strong induction. But, if you induct on divisibility instead, then everything Just Works :tm: