[FOM] Intensional identicity and identicity of proofs

[Aatu Koskensilta]

Kenneth Walden wrote:

> 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

This is the lecture "Referential intensions: a logical calculus for 
meaning and synonymity", which can also be found at Moschovakis' 
homepage I referred to earlier. Also, it appears that the paper at 
Moschovakis' homepage contains some corrections.

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

I myself found Moschovakis' account quite plausible. I don't have the 
papers at hand right now, but if I recall correctly, Moschovakis defines 
the referential intension of a term A by means of it's normal form nf(A) 
= A_0 where {p_1 := A_1, ..., p_n := A_n}, where all of the A_i are 
irreducible. Now, the intension of A is the algorithm that takes as 
input a state a and begins with such p_i as have immediate denotations, 
finds those denotations in a, then proceeds to those p_k that involve 
only the already found denotations, and so forth, until one comes to 
A_0, the denotation of which can now be computed and is the denotation 
of A. It's assumed that the where-clause is acyclic, i.e. p_i can be 
assigned ranks so that if rank(p_k) < rank(p_m), then p_m does not occur 
in A_k. If we allow for cyclic where-clauses, then we may get 
non-terminating algorithms. Two terms are synonymous if and only if they 
are immediate and are intensionally identical according to the Carnapian 
definition or if the algorithms of their referential intensions are 
naturally isomorphic.

This notion of synonymity is very strict, and it might be possible to 
use other conditions more relaxed than natural isomorphism. However, 
finding sensible other synonymity conditions might simply be equivalent 
or closely related to the problem of finding natural conditions for two 
proofs to be considered identical.

> The general idea of identity 
> based on algorithm might bear fruit even if the typed lambda calculus is 
> ill-fit for proof theoretic concerns.

True. Are there other promising notions of identity/synonymity not based 
on algorithms?

-- 
Aatu Koskensilta (aatu.koskensilta at xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
  - Ludwig Wittgenstein, Tractatus Logico-Philosophicus