[CL] Clarification on boolean sentences

[Bruno Emond]

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)
T
CL-USER 2 > (or)
NIL

Bruno

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.
>
> Pat
>
> 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:
>>
>>  (or)
>>
>> In resolution theorem proving, this is called the
>> *empty clause*, and it is false.
>>
>> John Sowa
>>
>> _______________________________________________
>> CL mailing list
>> CL at philebus.tamu.edu
>> http://philebus.tamu.edu/mailman/listinfo/cl
>>
>
> ------------------------------------------------------------
> IHMC                                     (850)434 8903 or (650)494  
> 3973
> 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
> http://philebus.tamu.edu/mailman/listinfo/cl