[CL] Clarification on boolean sentences
brunoemond at fastmail.fm
Thu Nov 26 09:39:54 CST 2009
Just to add more support to the interpretation of (and) and (or).
In Charles S. Peirce system of existential graphs, (and) corresponds
to a blank sheet of assertion, which is always true.
And (or) to an empty cut, which is interpreted as always false.
Interestingly, this is also what a Lisp interpreter returns
CL-USER 1 > (and)
CL-USER 2 > (or)
On 26-Nov-09, at 02:27 , Pat Hayes wrote:
> And not to be outdone, my own favorite way to think about this is
> that (and p1 ... pn) is made false by any one of the pi being false,
> and otherwise it must be true. And so the key property of (and) is
> that it can't be made false. Similarly, (or) cannot be made true.
> On Nov 25, 2009, at 11:58 PM, John F. Sowa wrote:
>> I agree with the point Chris made, but I'd like to add another
>> example to emphasize why (or) is defined to be false.
>> The point I'd like to add is a connection with resolution
>> theorem proving, which is based on a rule of inference applied
>> to *clauses*, such as
>> p or q or ~r, r or ~u or ~v, u or w, v, ~w, ~p, ~q
>> The resolution rule does a kind of cancellation, which takes two
>> clauses that contain a negative "literal" in one, such as '~r',
>> and a positive literal in the other, such as 'r'. It erases both,
>> and merges the remaining literals into a single clause. For
>> example, we can apply that rule to the first two clauses at the
>> left above:
>> p or q or ~r, r or ~u or ~v to derive: p or q or ~u or ~ v
>> Then we can take the newly derived clause and resolve it with
>> the third clause above to get
>> p or q or ~v or w
>> We continue to resolve each newly derived clause with the next
>> clause on the list above. The last two clauses are
>> q, ~q
>> Each of these is a disjunction of just one literal.
>> In CLIF, they would be represented
>> (or q), (or (not q))
>> These two clauses are contradictory. When we apply
>> resolution to them, they cancel each other out to
>> produce a disjunction of zero literals:
>> In resolution theorem proving, this is called the
>> *empty clause*, and it is false.
>> John Sowa
>> CL mailing list
>> CL at philebus.tamu.edu
> IHMC (850)434 8903 or (650)494
> 40 South Alcaniz St. (850)202 4416 office
> Pensacola (850)202 4440 fax
> FL 32502 (850)291 0667 mobile
> phayesAT-SIGNihmc.us http://www.ihmc.us/users/phayes
> CL mailing list
> CL at philebus.tamu.edu
More information about the CL