# Abstract

A system of logic usually comprises a language for which a model-theory
and a proof-theory are defined. The model-theory defines the semantic notion of
model-theoretic logical consequence (⊨), while the proof-theory defines the proof-
theoretic notion of logical consequence (or logical derivability, ⊢). If the system in
question is sound and complete, then the two notions of logical consequence are
extensionally equivalent. The concept of full formalization is a more restrictive one
and requires in addition the preservation of the standard meanings of the logical terms
in all the admissible interpretations of the logical calculus, as it is proof-theoretically
defined. Although classical first-order logic is sound and complete, its standard
formalizations fall short to be full formalizations since they allow non-intended
interpretations. This fact poses a challenge for the logical inferentialism program,
whose main tenet is that the meanings of the logical terms are uniquely determined by
the formal axioms or rules of inference that govern their use in a logical calculus, i.e.,
logical inferentialism requires a categorical calculus. This paper is the first part of a
more elaborated study which will analyze the categoricity problem from its beginning
until the most recent approaches. I will first start by describing the problem of a full
formalization in the general framework in which Carnap (1934/1937, 1943) formulated
it for classical logic. Then, in sections IV and V, I shall discuss the way in which the
mathematicians B.A. Bernstein (1932) and E.V. Huntington (1933) have previously
formulated and analyzed it in algebraic terms for propositional logic and, finally, I shall
discuss some critical reactions Nagel (1943), Hempel (1943), Fitch (1944), and Church
(1944) formulated to these approaches.