I am reading Lof's Intuitionistic type theory. He says,
.. intuitionistically, truth is identified with provability, though of course not (because of Godel’s incompleteness theorem) with derivability within any particular formal system
I am not sure if i understand this right, I have been thinking provability and derivability are same notions and Godel's theorem applies to both. Can someone explain me how they are different notions?
I also read somewhere that, derivability is syntactic while provability is more meta level. I dont think i understand that either.
See The Development of Intuitionistic Logic : the "natural" semantics for intuitionistic logic is based on proof (or construction) instead of truth.
Thus, it is in some way an "undefined" concept.
In the context of a formalization of Intuitionistic Logic, the concept of derivation is relative to a calculus, and it is defined as usual as a sequence of formulae, "derived" by way of application of the allowed rules of inferences from axioms or assumptions.