[Om] logic1 CD revision?

[W Naylor]

On Thu, 17 Aug 2006, Jacques Carette wrote:

> "the" logic???  Do you know how many two-valued boolean logics there are?
> 
> You might mean "classical two-valued, first-order Boolean propositional
> logic".

OK, then I propose the following sentence in the top level Description 
element:

This CD defines the operations and values of the classical two-valued, 
first-order Boolean propositional logic.

is this specific enough? As to circularity, full characterisation (etc.) 
of the FMPs, these are only supposed to be mathematical properties, not 
defining properties. In fact, since FMPs are written in terms of 
other symbols, I don't really see how one can escape circularity (if one 
intends to see them as defining properties), unless it is first agreed on 
which are the base terms that other symbols can be defined in terms of.

Bill

> 
> And while I am looking at it:
> 1) doesn't anyone see anything wrong with the FMP for 'equivalent'?  It seems
> to use a circular definition.
> 2) the FMP (and CMP) for 'not' does not characterize 'not' as this FMP is also
> satisfied by the identity.  The informal description is actually a better
> 'definition'.
> 3) in the same vein, the FMP for 'or', 'and' are not sufficient to uniquely
> define them either, as well as all being consequences of excluded-middle.  So
> _all_ the FMPs in this CD turn out to be restatements of excluded-middle!
> 4) those FMPs use the forall quantifier, which is defined in quant1 which
> depends on logic1.
> 
> Jacques
> 
> W Naylor wrote:
> > Clare is of course correct here. Would it be sufficient to change the top
> > level Description element to say:
> > 
> > This CD defines the operations of the two valued Boolean logic.
> > 
> > Bill
> > 
> > On Tue, 15 Aug 2006, Clare So wrote:
> > 
> > 
> > > Dear OpenMathers,
> > > 
> > > I would like to suggest that logic1 CD may need a revision.  The
> > > description
> > > of it does not say whether the functions are for two-value logic or
> > > not.  In
> > > some systems, three-value logic is used.  It would be better if we
> > > state the
> > > meanings of each OMS as explicit as possible.
> > > 
> > > Clare
> > > _______________________________________________
> > > Om mailing list
> > > Om at openmath.org
> > > http://openmath.org/mailman/listinfo/om
> > > 
> > > 
> > > 
> > > 
> > > 
> > 
> > -*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
> > -
> > -                  Dr. W.A. Naylor
> > -
> > -                  http://www.cs.bath.ac.uk/~wn
> > -                  http://orcca.on.ca/~bill
> > -
> > -                  work tel: +44 1225 386183
> > -
> > -*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
> > 
> > _______________________________________________
> > Om mailing list
> > Om at openmath.org
> > http://openmath.org/mailman/listinfo/om
> > 
> 
> 
> 

-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
-
-                  Dr. W.A. Naylor
-
-                  http://www.cs.bath.ac.uk/~wn
-                  http://orcca.on.ca/~bill
-
-                  work tel: +44 1225 386183
-
-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*