# [FOM] Intensional identicity and identicity of proofs

Aatu Koskensilta aatu.koskensilta at xortec.fi
Thu Jul 10 02:07:18 EDT 2003

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

```