Fwd: [SCL] proposition variables in SCL??

Pat Hayes phayes at ihmc.us
Tue Feb 17 17:10:06 CST 2004 

>(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