Jtdylktuy

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?

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.

One could say that there is some ambiguity to the term "proof-theoretic semantics". Some people apply it to the BHK interpretation and Martin-Löfs meaning explantions. These are no formal semantics. They are called "proof-theoretic" because, as the OP already remarked, they are based on the notion of proof. In this context, the term "semantics" in "proof-theoretic semantics" is used in the broader sense of (informal) meaning explanations.

Starting in the early seventies, Prawitz (and others) tried to combine the BHK interpretation and the inversion principle of natural deduction systems (or "deductive harmony", as it is often called today) in order to obtain a formal semantics. Roughly speaking, one could say that the properties afforded by the inversion principle (normalization, subformula property etc.) are used as an antidote against the highly impredicative character of the BHK clauses, in particular, the clause for implication. The resulting semantics actually provide formal definitions of logical validity. For these formal semantics, the questions of soundness and completeness (with respect to intuitionistic logic) are pertinent.

A constructivist may have reservations with respect to Kripke semantics (among other things, because it is not based on the notion of proof, or construction, and because the completeness theorem relies on strictly classical reasoning in the meta level) and may favour either an informal or formal proof-theoretic semantics instead.