This thesis is part of a line of research aimed at investigating how insights and results from the algebraic and relational semantics of given families of logics can contribute to the design of ‘good’ proof calculi for these logics. It focuses on the intersection between syntax and semantics in structural proof theory. The results of the present thesis develop the interface between syntax and semantics for proof-theoretic purposes in very specific ways: on the semantic side, these results build on and further develop the link between relational and algebraic semantics of logics given by discrete dualities and their associated unified correspondence results; on the syntactic side, these results further develop the theory of proper multi-type display calculi. The results of this thesis include: a systematic connection between the syntactic shape of analytic inductive axioms and the generation of cut-free derivations of these axioms from their associated analytic structural rules; the introduction of proper display calculi for monotone modal logic and conditional logic and a large family of their axiomatic extensions, thanks to a reformulation of their neighbourhood semantics in a suitable multitype relational environment; extending the semantic analysis for monotone modal logic and conditional logic to graded modal logic and proposing a new definition of graded bisimulation.