Gerhard Gentzen is the founder of proof-theoretic semantics, providing the formal basis for it in his account of cut-elimination for the sequent calculus, and some provocative philosophical remarks about locating the meaning of logical connectives in their introduction rules within natural deduction.
[citation needed] This idea lies at the basis of the Curry–Howard isomorphism, and of intuitionistic type theory.
Michael Dummett introduced the very fundamental idea of logical harmony, building on a suggestion of Nuel Belnap.
In brief, a language, which is understood to be associated with certain patterns of inference, has logical harmony if it is always possible to recover analytic proofs from arbitrary demonstrations, as can be shown for the sequent calculus by means of cut-elimination theorems and for natural deduction by means of normalisation theorems.
A language that lacks logical harmony will suffer from the existence of incoherent forms of inference: it will likely be inconsistent.