Lambda the Ultimate

inactiveTopic A Revolution in Logic?
started 10/13/2003; 12:41:43 PM - last post 10/14/2003; 11:47:29 PM
Patrick Logan - A Revolution in Logic?  blueArrow
10/13/2003; 12:41:43 PM (reads: 7416, responses: 9)
A Revolution in Logic?
I am not sure of the implications of this idea for programming languages. So I'll turn it over to LtU readers to inform me.

Frege's formulation of first-order logic contains a fundamental error. It is manifested already in his formation rules. And this same virus has infected all the subsequent formulations and versions of first-order logic... The real ground floor of the edifice of logic... is Independence-Free (IF) first-order logic.
Posted to Logic/Declerative by Patrick Logan on 10/13/03; 12:42:02 PM

Marc Hamann - Re: A Revolution in Logic?  blueArrow
10/13/2003; 1:37:27 PM (reads: 707, responses: 3)
I didn't read this whole paper carefully, since I started to wonder if it wasn't a hoax.

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? ;-)

Ehud Lamm - Re: A Revolution in Logic?  blueArrow
10/13/2003; 2:56:30 PM (reads: 702, responses: 2)
I haven't read the paper but Jaakko Hintikka is a prominent philosopher (with books dedicated to him).

Marc Hamann - Re: A Revolution in Logic?  blueArrow
10/13/2003; 3:57:25 PM (reads: 687, responses: 0)
Unless someone can point out a subtlety that I missed (entirely possible), I would have to conclude that the standard of logic in philosophy is divergent from that in mathematics.

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

Marc Hamann - Re: A Revolution in Logic?  blueArrow
10/13/2003; 5:01:09 PM (reads: 671, responses: 0)
Hmmm. I found this reference to a paper by van Benthem (man that guy gets around... ;-) ) that discusses Hintikka's IF proposal with what I read as polite skepticism (though he seems to think there might be something lurking in there somewhere).

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. ;-)

water - Re: A Revolution in Logic?  blueArrow
10/14/2003; 3:11:41 AM (reads: 543, responses: 1)

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.

Marc Hamann - Re: A Revolution in Logic?  blueArrow
10/14/2003; 4:39:49 AM (reads: 527, responses: 0)
I don't understand Marc's cynicism here: Hintikka's extension to logic is strictly more expressive and removes ambiguities.

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.

Frank Atanassow - Re: A Revolution in Logic?  blueArrow
10/14/2003; 5:40:58 AM (reads: 501, responses: 0)
The paper introduces some new notation, claims its meaning is obvious, and then natters on about what was never clearly defined.

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.

Sjoerd Visscher - Re: A Revolution in Logic?  blueArrow
10/14/2003; 9:45:23 AM (reads: 445, responses: 0)

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

Ken Shan - Re: A Revolution in Logic?  blueArrow
10/14/2003; 11:47:29 PM (reads: 366, responses: 0)
IF logic is not just notation, but its semantics can be surprising or unclear. I find it helpful to work through some of the (counter)examples in Theo Janssen's paper "Independent choices and the interpretation of IF logic".