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 ]
 Jan Burse Posts: 1,472 Registered: 4/12/05
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 21, 2009 4:25 PM

Andrew Tomazos schrieb:

> Are you sure the way you have written it is really clearer?
>
> When you think about it - if I state that a series of propositions:
>
> A
> B
> C
> D
>
> are individually true in some context, than it is exactly the same as
> saying:
>
> A and B and C and D
>

Yes, but this is quite a myoptic view. You are now only thinking
inside the realm of theorems. How do you avoid confusion between
a proof figure (supposed it will use ";") and a conjunction (since
you will also use ";") here.

So discussion does not make sense, as long as you don't show us
your ideas for proofs. Maybe when you have shown me your ideas
about proofs, I will maybe fully agree on some points of your
syntax.

But there is also a semantical consideration here. Namely
for example in natural deduction, it is not obvious that
listing of axioms is the same as conjunction. So for
example in minimal logic, when we write:

A, B, C |- D

This is not the same as:

A & B & C |- D

Where & is classical. It is the same as:

A * B * C |- D

Where * is some kind of fusion. So it really makes sense to have
both available, some kind of listing and explicit forms
of conjunction, alas there is not only one conjunction.

This transposes also to "context" you mentioned. In the example
there is an exists context and a forall context. Whereas I know
the listing practice for the axiom context, the listing practice
for quantifier contexts is less known to me.

Except maybe the "," in Prolog, which has the meaning of a kind of
a conjunction. But in Prolog the "," is mostly treated as any other
operator. With a level and a associativity etc.. So maybe we can
advance the discussion as follows. You want the following operator
and :

";" : Conjunction
"forall" : Universal quantifier
"implies": Implication
"thereexists" : Existential quantifier

Ok, now tell me, how will the story continue for proof figures?

Bye

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