[CL] Quantified sentences
cross at kojeware.com
Thu Dec 3 08:43:28 CST 2009
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.
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
> 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)
> CL mailing list
> CL at philebus.tamu.edu
More information about the CL