Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

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


Math Forum » Discussions » sci.math.* » sci.math

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

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Jan Burse

Posts: 463
Registered: 4/12/05
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 21, 2009 4:25 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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
Read Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/25/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/25/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/26/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Joshua Cranmer
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Marshall
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Spiros Bousbouras
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Tim Smith
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Charlie-Boo
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
William Elliot
6/22/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/22/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/23/09
Read Re: Formal Proof Language Example - Human-Readable?
Slawomir
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
David Bernier
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/25/09
Read Re: Formal Proof Language Example - Human-Readable?
Slawomir

Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.