On Oct 11, 2010, at 10:21 PM, doug foxvog wrote:
> On Mon, October 11, 2010 23:04, Christopher Menzel said:
>> On Mon, 20101011 at 12:41 0700, Rich Cooper wrote:
>> ...
>> Higherorder languages are indeed more expressive [than FOL]. As a
>> consequence, they are not even partially decidable.
>
> Maybe Higherorder languages as a whole are not even partially decidable,
> but large numbers of statements in them are. (01)
Sure, but I'm not sure I see the point. We're talking about the logics
themselves. (02)
> It was noted that normal computer languages embodied HOL. (03)
That's a statement that needs a great deal of qualification. I am far from an
expert on these matters, so someone with a more authoritative grasp of the
subjects might well usefully correct/qualify some of my remarks. But I believe
the gist of the following is correct. (04)
The logic that corresponds to most programming languages is the untyped lambda
calculus, which is designed to represent recursion. The reason the lambda
calculus is often referred to as higherorder is because it quantifies over
functions. It is true that higherorder logics can quantify over functions
(and properties and relations) and, for this reason,
functions/properties/relations are often referred to as "higherorder
objects". But simply quantifying over such objects is not in itself what makes
a logic higherorder; rather, the function/property/relation space must consist
of all possible functions/properties/relations over (in the secondorder case)
the domain of individuals. Absent that requirement, in the context of basic
classical logic, one's logic is still firstorder. (I'd recommend Herbert
Enderton's article "Secondorder and Higherorder Logic" in the Stanford
Encyclopedia of Philosophy for more on this  http://goo.gl/Ubko.) (05)
Now, with its ability to represent recursion as well as basic arithmetic, the
lambda calculus certain far exceeds firstorder logic in expressive power. But
it is not straightforwardly classified as a species of classical higherorder
logic either, as standard higherorder logic does not of itself support
recursion, in the sense that mechanisms for defining recursive functions and a
proof of their existence do not simply fall out of the semantics of
higherorder logic; nor does the semantics allow for such constructs as
functional selfapplication, which is possible in the untyped lambda calculus.
Because of these features, the untyped lambda calculus does not have a
classical higherorder semantics and, indeed, finding a semantics for it proved
to be a very difficult problem that was not solved until Scott's discovery of
domain theory in the 1960s. Together with Strachey, Scott applied domain
theory to the development of denotational semantics for programming languages.
Theoretically, this is a very beautiful semantics, but it is much more complex
than the simple and straightforward semantics of ordinary higherorder logic. (06)
Bottom line: The sense in which normal computer languages "embody" higherorder
logic is not a simple and straightforward matter. (07)
chris (08)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontologforum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontologforum/
Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgibin/wiki.pl?WikiHomePage#nid1J
To Post: mailto:ontologforum@xxxxxxxxxxxxxxxx (09)
