[FOM] Intensional identicity and identicity of proofs

[Aatu Koskensilta]

In a post here some time ago I asked for a precise definition for 
intensional identicity of concepts that does not make necessarily 
co-extenensive concepts intensionally identical.

The reason I asked this is that the Carnapian account, which is used in 
most intensional logic, makes the concepts "a non-identical object" and 
"a bijection from the set of well-orderings of omega onto the reals" 
intensionally identical if the continuum hypothesis is false. Now surely 
these two are *not* intensinally identical under any condidition, and 
thus the Carnapian definition for intensional identicity is flawed.

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". (These can be found at 
http://www.math.ucla.edu/~ynm/papers.htm). I haven't yet studied them in 
detail, but it's obvious that they provide at least one possible real 
answer to my question.

As far as I gathered from a quick browsing trough of these articles, 
Moschovaki's begins noting the flaws of the Carnapian account, and then 
proposes to replace Carnapian account of intensional identicity with one 
that states that two concepts are intensionally identical if they, in an 
abstract sense, define the same algorithm (in a general, idealised 
sense, not in the sense of being a "recipe" for a recursive function) 
for determining whether the concept applies to a particular object or 
not. The rest of the paper is devoted to a development of a calculus 
formalising this intuition.

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.

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

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