Lambda the Ultimate

Take their formula (7) (in web-friendly notation)

(Ax)(Az)(Ey/Az)(Eu/Ax)S[x, y, z, u]

The "obvious" interpretation of this is that S is essentially a compound predicate of two other predicates of the form:

S1[x, z] ⁁ S2 [y, u]

If you stick the quantifiers into these subscopes, the "problem" goes away:

(Ax)(Ez)S1[x, z] ⁁ (Ay)(Eu)S2[y, u]

To make this concrete, let's assume the meaning of S1 is "z is the name of x" and the meaning of S2 is "u is the colour of y".

Then 7 says that for any object in our universe of discourse, I can assign a name to it, while independently selecting another object and assigning it a colour, at the same time!

Well, duh.

Unless I missed some brilliant insight in the parts I skipped over, this paper amounts to introducing a new "obvious" notation that describes something that is handled perfectly well with NO notation (independent scopes) and then makes it look like this is a problem by hiding the obvious interpretation under the hood of the predicate.

Was this someone's term paper? ;-)

Having read Wittgenstein, I was pretty sure of this already. ;-)

This paper is more focused on Game Theory, which in the Hintikka/Sandu paper (at least as far as I read it), was not in evidence, though Hintikka's website touts him as a grand poobah in Game Theory (among other things).

On the plus side, scholarship like this makes me feel much less bad about "human factors" arguments. ;-)

It's curious to see this, because I have a copy of the book he later wrote on this idea. I don't understand Marc's cynicism here: Hintikka's extension to logic is strictly more expressive and removes ambiguities. The equivalent expressions in non-IF logic for an IF expression with independent quantifiers are weaker; they can be false when their IF formulation is true. See also this Planet Math entry to get a full explanation of what this means.

Returning to the purpose of the post: the lesson for programming languages might be that lexical scope as a historical background for programming languages may cause language designers to shoehorn some issue into a lexically-shaped notation instead of something more natural to the problem. A recent Lisp extension to provide dynamically-scoped function bindings comes to mind, since it provides some very interesting features (fairly equivalent to AOP features), but previously was not a possibility that occurred to designers or users or considered worth even trying.

The use of game theory ideas in a formal language is also interesting. It could be used in declarative languages with quantifiers, and might even make a workable model of evaluation (reminiscent of Dynamo.

Having investigated the matter further, I don't deny that the system Hintikka later developed may have interesting features.

However, I read his paper the way I read numerous other papers by people I have never heard of: on its own merits.

In the paper in question, he doesn't mention his game theoretic model of truth, but rather that first order logic is screwed up and that there is an "obvious" new notation that fixes it.

The "obvious" interpretation to me was not a problem for FOL at all, and he didn't offer any evidence that it still was (though he may have offered some later; I stopped reading at that point)

He may be a flaming genius, but that paper did not make a compelling case for this as far as I'm concerned.

I have no idea what this is supposed to mean:

(all x)(A(x)(or/all x)B(x))

not only because I don't know what the slash means (yeah, yeah, `independence', I know), but also because it seems to bind x twice. water mentioned something about lexical scope, which gives me an inkling of what may be involved, but without an unambiguous definition I can't really evaluate what the authors claim.

I agree with Marc; perhaps the book and other papers do a better job, but this paper, judged on its own merits, sucks.

(all x)(A(x)(or/all x)B(x))

On the next page it's explained that it means:

(all x)A(x) or (all x)B(x)

Calling this "intuitively obvious" is weird indeed.