A comparison of three kinds of monotonic proof-theoretic semantics and the base-incompleteness of intuitionistic logic

Abstract I deal with two approaches to proof-theoretic semantics: one based on argument structures and justifications, which I call reducibility semantics, and one based on consequence among (sets of) formulas over atomic bases, called base semantics. The latter splits in turn into a standard reading, and a variant of it put forward by Sandqvist. I prove some results which, when suitable conditions are met, permit one to shift from one approach to the other, and I draw some of the consequences of these results relative to the issue of completeness of (recursive) logical systems with respect to proof-theoretic notions of validity. This will lead me to focus on a notion of base-completeness, which I will discuss with reference to known completeness results for intuitionistic logic. The general interest of the proposed approach stems from the fact that reducibility semantics can be understood as a labelling of base semantics with proof-objects typed on (sets of) formulas for which a base semantics consequence relation holds, and which witness this very fact. Vice versa, base semantics can be understood as a type-abstraction of a reducibility semantics consequence relation obtained by removing the witness of the fact that this relation holds, and by just focusing on the input and output type of the relevant proof-object.