Fwd: [SCL] proposition variables in SCL??

Pat Hayes phayes at ihmc.us
Wed Feb 18 15:16:09 CST 2004 

>This confirms my original suspicion that propositional symbols
>and variables are not worth the trouble, although I became willing
>to consider it when you initially enthused about the extension.
>I now doubt that propositional symbols and variables would add
>much but complication, so agree that the idea should be dropped.
>
>My original remark that
>"It is perhaps worth noting in the text that
>(implies P Q)
>is not legal SCL; it must be written as
>(implies (P) (Q))"
>stands, since some users might expect otherwise.

Agreed, and will add this WIGT.

>
>On a slightly related topic, should SCL syntax contain
>'true' and 'false' truth-functional constants as sentences?

We thought of that but (iff true (and)) (iff false (or)) so we 
decided not to bother. Ugly, but workable, particularly if you keep 
muttering "null clause is false, null clause is false" to yourself 
over and over.

Pat


>
>Mark
>
>
>Pat Hayes wrote:
>
>>>(I'm not on the SCL mailing list yet, so was unable to send it
>>>there as I intended.  Anyway, here's my first feedback.  Mark)
>>
>>
>>Forwarded to SCL.
>>
>>>I'm undecided so far.  I can see merits to it, but cannot yet foresee
>>>all the complications that may arise. I was aware of the 
>>>possibility of this extension
>>>when I wrote the comment about (implies P Q) being syntactically
>>>inadmissable due to the absence of proposition symbols.  And SNARK
>>>does act partly in accord with Pat's suggestion: SNARK
>>>has constant symbols, function symbols, proposition symbols, and
>>>relation symbols, allows the same symbol to be used in multiple
>>>roles, but with no prescribed relationship between P being used
>>>in multiple roles.  The most important deviation between SNARK and
>>>SCL in this area is that SNARK is closer to GOFOL in that it does not allow
>>>variables in function, relation, or proposition position.
>>
>>
>>The killer that has just occurred to me is what happens with 
>>equality. Consider
>>
>>(= P Q)
>>P
>>
>>this ought to entail Q by =y  substitution.  Fine: the semantics 
>>for = and for iff are virtually the same anyway.  But now consider
>>(= P (f a))
>>P
>>which now has to entail
>>(f a)
>>which, to emphasize, is NOT an atomic sentence but instead is a 
>>term denoting a truth-value.
>>
>>I think I can see a way to make sense of this, but I'd really 
>>rather not go there, at least in this version. The logic is getting 
>>just too weird at this point.
>>
>>>
>>>As Pat writes, introducing proposition symbols as well as relation 
>>>symbols in SCL
>>>leads to quantification as in (forall (P) (iff P (P))) and (exists 
>>>(P) P).  But
>>>in general, the range of these quantifiers would in effect be the 
>>>set of all atomic
>>>formulas, not just proposition symbols.
>>
>>
>>Well, no, not in SCL: the range might even be empty. SCL has no 
>>built-in comprehension principles for any kind of quantification, 
>>so the class of 'propositional individuals' if I can call them 
>>that, might be empty in some models. So this would be satisfiable:
>>
>>(not (exists (p) p))
>>
>>and would be consistent with, say
>>(P a)
>>(P)
>>and even with
>>P
>>but not with, say, the combination
>>(and (Q P) P)
>>because this last has P both as an individual name and as a 
>>proposition letter.
>>
>>>  One might be tempted to
>>>go even further then: why not quantify over all formulas, not just atomic
>>>ones (this would require changes to the notion of reservedElements).
>>
>>
>>Well, there are now principled reasons to resist such temptations, 
>>however. That is, would this be necessary in order to allow someone 
>>on a network to use any FO reasoning pattern? (answer, no, I think.)
>>
>>Pat
>>
>>>So, to me the key questions are (1) whether you want to be able
>>>to quantify over atomic formulas and, if so, (2) whether you want to be able
>>>to quantify over nonatomic ones as well.
>>>
>>>Mark
>>>
>>>
>>>Pat Hayes wrote:
>>>
>>>>>X-Scanned-By: RAE MPP/Sophos http://raeinternet.com/mpp
>>>>>X-Scanned-By: RAE MPP/Cybersoft PA http://raeinternet.com/mpp
>>>>>X-Real-To: <phayes at ihmc.us>
>>>>>X-Original-To: scl at philebus.tamu.edu
>>>>>Delivered-To: scl at philebus.tamu.edu
>>>>>X-Sender: phayes at mail.ihmc.us
>>>>>Date: Mon, 16 Feb 2004 11:24:33 -0600
>>>>>To: scl at philebus.tamu.edu
>>>>>From: Pat Hayes <phayes at ihmc.us>
>>>>>Subject: [SCL] proposition variables in SCL??
>>>>>X-BeenThere: scl at philebus.tamu.edu
>>>>>X-Mailman-Version: 2.1.3
>>>>>List-Id: A mailing list for the Simplified Common Logic (SCL) 
>>>>>working group
>>>>>     <scl.philebus.tamu.edu>
>>>>>List-Unsubscribe: <http://philebus.tamu.edu/mailman/listinfo/scl>,
>>>>>     <mailto:scl-request at philebus.tamu.edu?subject=unsubscribe>
>>>>>List-Archive: <http://philebus.tamu.edu/pipermail/scl>
>>>>>List-Post: <mailto:scl at philebus.tamu.edu>
>>>>>List-Help: <mailto:scl-request at philebus.tamu.edu?subject=help>
>>>>>List-Subscribe: <http://philebus.tamu.edu/mailman/listinfo/scl>,
>>>>>     <mailto:scl-request at philebus.tamu.edu?subject=subscribe>
>>>>>Sender: scl-bounces at philebus.tamu.edu
>>>>>
>>>>>Feedback welcomed on the following issue.
>>>>>
>>>>>-------
>>>>>
>>>>>Mark Stickel made the following comment:
>>>>>
>>>>>>
>>>>>>================
>>>>>>
>>>>>>It is perhaps worth noting in the text that
>>>>>>  (implies P Q)
>>>>>>is not legal SCL; it must be written as
>>>>>>  (implies (P) (Q))
>>>>>>I did not notice this at first; it hit me
>>>>>>when you wrote that all sentences include parentheses.
>>>>>
>>>>>
>>>>>
>>>>>Which made me think of the possibility of allowing proposition 
>>>>>names into SCL. Right now we don't have names denoting 
>>>>>propositions, only relations and individuals.
>>>>>
>>>>>Do you think there is a use case for allowing propositional 
>>>>>names in SCL?  Does anyone (know people who) actually need to be 
>>>>>able to write (implies P Q) ?
>>>>>
>>>>>Here's the rub. Following the, er, logic of the current 
>>>>>introduction, if we have proposition names then they ought to 
>>>>>survive punning with other names, in particular with 
>>>>>individuals: so it ought to be possible to quantify over them, 
>>>>>which is definitely not standard FO syntax; not even standard HO 
>>>>>syntax, in fact.
>>>>>
>>>>>However, with our semantics, they could be, and in fact it would 
>>>>>be rather elegant, since then they would denote entities with 
>>>>>truth-functional extensions, i.e. genuine propositions.
>>>>>
>>>>>Here's how it would go: a name P can now have *three* kinds of 
>>>>>extension: a truth-value, a relation(al extension) and a 
>>>>>function; and they all can be 'folded' onto the denotation of 
>>>>>the name. You CAN write things like
>>>>>(iff P (P))
>>>>>but you aren't obliged to specify any connection. And you can 
>>>>>(that is, it makes semantic sense to) write things like
>>>>>(exists (P)  P)
>>>>>which could even be false in some interpretations. As far as I 
>>>>>can see, this introduces no new tautologies.
>>>>>
>>>>>In sum: this would be easy to do and might make SCL more 
>>>>>powerful and expressive for some users, but it makes the 
>>>>>language less conventional in ways that might give some people 
>>>>>the horrors.
>>>>>
>>>>>Any comments?
>>>>>
>>>>>Pat
>>>>>
>>>>>
>>>>>
>>>>>--
>>>>>---------------------------------------------------------------------
>>>>>IHMC    (850)434 8903 or (650)494 3973   home
>>>>>40 South Alcaniz St.    (850)202 4416   office
>>>>>Pensacola            (850)202 4440   fax
>>>>>FL 32501            (850)291 0667    cell
>>>>>phayes at ihmc.us       http://www.ihmc.us/users/phayes
>>>>>
>>>>>_______________________________________________
>>>>>SCL mailing list
>>>>>SCL at philebus.tamu.edu
>>>>>http://philebus.tamu.edu/mailman/listinfo/scl


-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes at ihmc.us       http://www.ihmc.us/users/phayes

More information about the SCL mailing list