Fwd: Re: Fwd: [SCL] proposition variables in SCL??

[Pat Hayes]

>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>
>Date: Mon, 16 Feb 2004 16:41:19 -0800
>From: Mark Stickel <stickel at ai.sri.com>
>Reply-To:  stickel at ai.sri.com
>Organization: SRI International
>X-Accept-Language: en-us, en
>To: Pat Hayes <phayes at ihmc.us>
>Subject: Re: Fwd: [SCL] proposition variables in SCL??
>
>(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)
>
>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.
>
>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.  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).
>
>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