[FOM] Intensional identicity and identicity of proofs
Kenneth Walden
kwalden at fas.harvard.edu
Wed Jul 9 14:23:20 EDT 2003
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
More information about the FOM
mailing list