ABSTRACT
Implication with its standard inferential role acts as an “internalizer” of arguments, for it can produce, given an argument, a sentence that is a theorem (that is, it is inferable from no premises) if and only if the argument is correct. This allows us to transform Gentzenian calculi into something closer to axiomatic systems in the traditional sense. The axiomatic arguments are turned into sentences, the rules for deducing arguments from arguments are turned into inferential rules, and instead of theorematic arguments we also have sentences. In this way, we reach Hilbertian calculi. Such calculi define the relation of inference indirectly, in terms of the concept of proof, but it is easy to show that this is, in a certain respect, equivalent to what we can do with the Gentzenian calculi.
