🚀 go-pugleaf

Hi,  I have just started trying to learn about intuitionistic logic,
and constructive logics in general, and am a little puzzled by some notions
there, particularly of implication. Perhaps someone would be kind enough to
help me. (By e-mail please, I don't read this newsgroup regularly).

From what I could understand from the book I was reading ("Intuitionism" by
Heyting -- but I don't any more have access to the book ),  a mathematical 
proposition demands a construction *with certain properties*  and can be 
asserted when such a construction (in what seems to be an extremely general 
sense of the term) is carried out.  

About implication: P->Q can be asserted iff there is a construction r such 
that "joined to" any construction, say s, proving P, would automatically effect
a construction proving Q. 

I am a little puzzled by what "joined to" exactly means.  In all the 
examples I've seen, it has been juxtaposition of r and s -- which is
okay for applications such as the type system for functional languages etc.
(I think Heyting, in fact, says something to the effect of "by the definition 
of  implication, the construction consists of simply the juxtaposition of
r and s").

My first question is whether (and if so, what) constructions C[r,s] 
more complicated than juxtaposition can be used for defining implication
in an object language different from propositional intuitionistic logic. 
That is, in general, what are these "certain properties" that the 
constructions must have? 

Thanks,

Sanjiva Prasad			(sanjiva@ecrc.de)