What is the relationship between the BHK interpretation of propositional logic and Natural Deduction?

Question

I've been getting into intuitionistic logic lately, starting from propositional logic. I am interested in proof-theoretic semantics, meaning the idea that the truth of a proposition is derived from the existence of a proof of it. I have read different texts and while some authors mention Gentzen's Natural Deduction as the beginning of this proof theoretic semantics, many don't mention it at all and only refer to it as a proof system which is not based on axioms.
Those authors generally mention the Brouwer Heyting Kolmogorov interpretation as the source of this proof theoretic point of view, or Per Martin Lof's theory of verification.
My question is, how exactly are those three things related? Does Natural Deduction, except for being a proof system, provide proof theoretic semantics for propositional calculus? Lastly, what is the BHK interpretation regarded as exactly? I mean does it define a system of sorts?

Answer 1

You have to compare e.g. The Development of Proof Theory for an overview regarding proof systems, including Gentzen's creations: Sequent calculus and Natural Deduction, with Intuitionistic Logic.

Intuitionism gave birth to the first "alternative" logic, characterized by the rejection of some "classically" valid principles, like the Law of Excluded Middle.

Intuitionistic logic can be foramlized with suitable proof systems, i.e. with a peculiar version of the many well-known proof systems: Hilbert-style, Natural Deduction, Sequent Calculus, Tableau.

In short, we have an intuitionistic Natural Deduction as well as a classical one.

Classical logic has its standard two-valued semantics: the truth-functional one (see Boolean Algebra and the usual truth tables).

Intuitionsitic logic has been equipped with its own semantics, based on Brouwer–Heyting–Kolmogorov interpretation.

For classical logic we have a Completeness Theorem, stating that every (classically) valid formula is provable with e.g. Natural Deduction, while for intuitionistic logic we have the corresponding Completeness Theorem with respect to Heyting semantics as well as Kripke semantics.