Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: Formal Proof Language Example - Human-Readable?
Replies: 39   Last Post: Jun 27, 2009 11:09 PM

 Messages: [ Previous | Next ]
 Slawomir Posts: 15 Registered: 12/8/04
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 25, 2009 10:49 AM

On Jun 24, 10:53 am, David Bernier <david...@videotron.ca> wrote:
> I looked at the _Binomial_coefficients_  example page at Formalpedia:
> <http://formalpedia.org/Binomial_coefficients>
>
> I can guess some of what the notation means, but not all.
>
> For example, why is there a 'k' as the first character of
> k.Binomial_coefficients.binom  ?
>
> Another thing I don't understand is the meaning of Arith.fact
> in  "Theorem (binom_fact_thm)" .

This is an example what happens when the proof language does not
satisfy the "readability by mathematician" criterion. I can only guess
that the k.Binomial_coefficients.binom string there sets up the
context so that \forall k really means \forall k \in N , where N is
the set (type?) of natural numbers.
I believe that any system based on type theory (rather than set
theory) will be difficult to read for an average mathematician.
Standard mathematics is based on set theory and proof languages based
on type theory must have additional notation for indicating types. For
example, Isabelle's Isar is very readable when used with ZF logic, but
much less so when used with HOL, with all that "`a" and "::" noise in
the notation.

Date Subject Author
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Jan Burse
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Jan Burse
6/24/09 Andrew Tomazos
6/25/09 MeAmI.org
6/25/09 Jan Burse
6/26/09 Andrew Tomazos
6/27/09 Jan Burse
6/27/09 Andrew Tomazos
6/27/09 Jan Burse
6/27/09 Andrew Tomazos
6/27/09 Joshua Cranmer
6/27/09 Andrew Tomazos
6/21/09 Marshall
6/21/09 Spiros Bousbouras
6/24/09 Tim Smith
6/21/09 Charlie-Boo
6/21/09 William Elliot
6/22/09 MeAmI.org
6/22/09 MeAmI.org
6/23/09 Slawomir
6/24/09 David Bernier
6/24/09 MeAmI.org
6/24/09 MeAmI.org
6/24/09 Andrew Tomazos
6/24/09 Andrew Tomazos
6/25/09 Slawomir