[CL] Quantified sentences

[Cameron Ross]

Thanks for your input John.  Based on these points and the fact that, as 
Pat put it, "there was a general methodological principle in the CL 
design, which was to always permit rather than forbid", it is clear that 
a CLIF parser must admit such cases (as per the current CLIF grammar).  
I do, however, like Randall's suggestion of issuing warnings to help 
identify where oversights may have occurred while constructing 
handwritten CLIF text.  I'll probably add a feature to my CLIF parser, 
similar to gcc's -pedantic flag, that will issue such warnings when enabled.

Thanks everyone.
Cameron.


John F. Sowa wrote:
> Cameron and Randall,
>
> RS> I should point out that in my CLIF parser, I emit a warning
> > diagnostic when a quantifier binds an name not referred to
> > in the matrix. I do that because, at least for now, I'm dealing
> > mostly with hand-written CLIF and this is typically a spelling error.
>
> CR> Warning on such cases is a great idea.
>
> Yes, indeed.  But that is only if you are dealing with human
> generated input.
>
> The empty cases are very common during intermediate stages
> of a theorem prover.  For example, the empty clause in
> resolution theorem provers (which is falsum) is represented
> by (or) in CLIF and ~[ ] in CGIF.
>
> The verum, which is (and) in CLIF and a blank sheet or [ ]
> in CGIF, is the only axiom in systems of natural deduction,
> which include Peirce's rules for existential graphs.
>
> Another important special case is the double negation in
> CGIF:  ~[ ~[ ] ], which is equivalent to (if (and) (and)).
>
> In Gentzen's system of natural deduction, the first stage
> of proving p->q is to assume the hypothesis p, carry out
> the deduction of q, and then "discharge the assumption"
> by asserting p->q.
>
> But Gentzen's method requires a complex system of bookkeeping
> (or a recursive procedure) for going off on a side proof,
> discharging the assumption, and using the result in the
> main proof.
>
> With Peirce's rules (which can operate *inside* a nested
> expression), the proofs are all done in a straight line:
>
>  1. Draw a double negation around the blank:  ~[ ~[ ] ]
>
>  2. Insert the hypothesis into the negative area:  ~[p ~[ ]]
>
>  3. Copy p into the doubly nested area:  ~[ p ~[ p ] ]
>
>  4. Apply the rules that transform p to q inside the nested
>     area.
>
>  5. The result is ~[ p ~[ q ] ], which is p->q.
>
> With some adjustments, you can apply Peirce's rules to CLIF:
>
>  1. (if (and) (and))
>
>  2. (if (and p) (and))
>
>  3. (if (and p) (and p))
>
>  4. Apply rules to generate (if (and p) (and q))
>
>  5. Simplify:  (if p q)
>
> John
>
> _______________________________________________
> CL mailing list
> CL at philebus.tamu.edu
> http://philebus.tamu.edu/mailman/listinfo/cl