[FOM] Intensional identicity and identicity of proofs

[Kenneth Walden]

Moschovakis gave a class on referential intensions and synonymy at NASSLLI 
this year. I believe the lecture notes for the course are somewhat more 
detailed in the development of the calculus than Moschovakis's original 
papers. The notes are available at www.indiana.edu/~nasslli/program.html

You are right that Moschovakis gives a precise notion of intensional 
identity, but his development relies on the philosophical claim that 
meaning is in some broad sense algorithmic. He does not dispense with 
Carnap intensions altogether; in fact the algorithmic account he offers 
uses maps between Carnap intensions in much the way Montague described 
them. But since Moschovakis does not give a philosophical argument for his 
meaning-qua-algorithm approach, you ought judge his system by the 
interpretation it gives to natural language. But that's a non-fom digression.

As for applications to proof theory, Moschovakis's system is a (fairly 
elaborate) typed lambda calculus, so I'm not sure that it could be 
effectively stripped down to applicable to formal languages and still have 
enough power to give sophisticated notion of "synonymy". But I guess you 
can't be sure until it's tried. The general idea of identity based on 
algorithm might bear fruit even if the typed lambda calculus is ill-fit for 
proof theoretic concerns.

Best,

KW


At 08:28 AM 7/8/2003 +0300, Aatu Koskensilta wrote:
Receiving no response here, I later stubmled upon Y. N. Moschovaki's two 
papers "Sense and denotation as algorithm and value" and "A logical 
calculus of meaning and synonymity".
I wonder whether these formulations could be used also in proof theory to 
provide an adequate criterion for identicity of proofs, as the problem 
there seems quite related

________________________________________________
Kenneth E. Walden
kwalden at fas.harvard.edu
617.504.3439