
Re: Formal Proof Language Example  HumanReadable?
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

