Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.
Sign up to join this community
Can one prove these properties at all without relying on notions of models and interpretations?
Are there other properties that proof-theorists usually prove instead?
From what I've read, I've only found people proving logical harmony and using this property of logical harmony as justification for the rules they define.
One typically does not, soundness and completeness are not particularly natural properties from the proof-theoretic point of view. Although rarely spelled out explicitly, there is in the background this idea of "correspondence" of the formal theory F to some Platonized fragment of "reality". "Sound" means that everything provable in F is "true", and "complete" means that everything "true" is provable in F, because ideally F ought to reflect the "reality" faithfully. Proof-theoretic semantics services very different philosophical worldviews, and so has different priorities, see Realism-Antirealism Debate in the Age of Alternative Logics volume.
In my opinion, the SEP article ties proof-theoretic semantics too closely to "meaning is use" and inferentialism, however. "Meaning is use" is in principle compatible with (holistic) truth-conditionalism (Davidson), or with the instrumentalist semantics of "embodied cognition" (see Dreyfus), while the Kantian streak of the classical intuitionism explicitly rejects that inference exhausts meaning, or that provability is formalizable. What does unite the proof-theoretically motivated is what Dummett calls "anti-realism", the rejection of the "picture" view of reality, where "reality" is imagined as a "mind independent" theory of itself. The correspondence bridge then becomes a bridge to nowhere, and soundness and completeness lose their pre-eminent status. Rather than faithfully reflecting Platonic entities "up there" proof-theorists' focus on how meaning of statements is learned and communicated "down here". If one does not believe in "verification-transcendent truths" there is no reason to expect that the law of excluded middle (hence completeness) holds in the first place, and if there is no mind-independent "theory" then soundness has to be replaced by some other sort of adequacy of language.
Harmony is one such notion demanding that the introduction and elimination rules for new terms are balanced in such a way that they extend the language of immediately meaningful "observation sentences" conservatively. In other words, what is provable with them is already provable (perhaps in a much more complicated way) without them. This dovetails nicely with Field's nominalist programme of purging scientific language of set-theoretic excesses of ZFC to show that predicative mathematics already suffices, see Dummett's What is Mathematics About.
This said, proof-theorists certainly can reinterpret soundness and completeness on their own terms. For instance, Abrusci and Pistone write in On Trascendental Syntax: a Kantian Program for Logic
"It is indeed a well known result in proof-theory, whose foundational relevance we believe has not yet been highlighted enough in the literature, that Gentzen’s Hauptsatz has, as corollaries, purely internal versions of the soundness and the completeness theorems for first-order logic, which establish a sort of duality...".
A more tradirional way is to reinterpret set-theoretic "models". To a proof-theorist a "model" is not a Platonic fragment described in ZFC language, but just another formal theory M. It is typically a (possibly non-conservative) extension of ZFC by derived objects that serve as "realizations" of the objects of F (think of the Cantor-Dedekind construction of real numbers). One can ask if F is sound relative to M, i.e. if none of its theorems are disprovable in M when applied to the realizations. So the Peano arithmetic with the negation of the Gödel sentence added will be unsound relative to, say, von Neumann's realization of arithmetic in ZFC. But ZFC with its law of excluded middle, infinity, choice, etc., is itself so "unsound" by proof-theoretic lights that it is not saying much (of course, one could still argue informally that von Neumann's realization better represents our "arithmetical intuitions" than Peano arithmetic). The notion can be of technical interest, however, for example if we wish to independently axiomatize some special segment of already accepted theory, say the theory of quaternions.
It is somewhat better with completeness, it can be defined intrinsically not as exhausting a model, but simply as having every well-formed sentence, or its negation, among its theorems. This was Hilbert's original view, and part of his programme was to establish such things by purely syntactic means, i.e. by reasoning about symbols. The main difference between a classical and a proof theorist here would just be in how much is allowed in such reasoning, we wouldn't want to reproduce ZFC with symbols in place of sets. Hilbert was still a Kantian intuitionist about such reasoning (as were Brouwer and Weyl about all mathematical reasoning), see Was there a Kantian influence on Hilbert's formalist programme? But after Gödel's adoption Skolem's Primitive Recursive Arithmetic became an explicit minimalistic standard for "syntactic" arguments in proof theory (it also roughly corresponds to what Wittgenstein outlined in the Tractatus).
Gödel's proof of the Incompleteness Theorem is therefore proof-theoretically acceptable, but with a caveat. All it proves is that Peano Arithmetic (and any stronger first order theory, assuming it is consistent) has sentences that are neither provable nor disprovable in it. The more popular Gödel's formulation concerning "true but unprovable" sentences appeals to "intuitions" most people (think they) have about natural numbers, and goes beyond "syntactic reasoning". As long as this austere standard is upheld in proofs and formulations, there is not much difference in proving soundness and completeness "classically" vs "proof-theoretically".
Soundness and completeness proofs establish a relationship between a formal proof system (derivability) and a formal semantics (validity). Soundness means that anything that is derivable is also valid, and completeness means that anything that is valid is also derivable.
The fact that most soundness and completeness proofs refer to models and/or interpretations merely reflects the fact that most formal semantics are based on models and/or interpretations. The pervasiveness of model-theoretic semantics may lead someone to think that semantics is synonymous with models and interpretations, which is not actually accurate (unless, perhaps, if it is taken to be a concious philosophical position).
As long as you have a formal semantics (a formal definition of validity), even if not based on models, it is meaningful to ask whether it corresponds exactly to the proof system (derivability) of some logic. Of course, there may be some constraints on what could legitimately be called a semantics, but, as already remarked, these constraints would probably depend one's philosophical convictions. As a limiting case, defining as valid anything that is derivable in a particular proof system would make soundness and completeness (of that proof system) trivial and also make the distinction between validity and derivability pointless. This is certainly not the case with standard proof-theoretic semantics, though.
The significance of soundness and completeness results may change depending on context and the philosophical outlook. Soundness and completeness can be considered as establishing the adequacy of a proof system to a semantics, or the other way around. So, for instance, it is common to introduce the semantics of classical propositional logic via truth tables and then, after presenting a tableau proof system, to establish its adequacy with respect to the semantics by means of soundness and completeness proofs. On the other hand, when Kripke proposed a semantics for intuitionistic logic, a legitimate question was whether his semantics provided an adequate interpretation of the canons of reasoning encoded in intuitionistic logic (which has already been around as proof system for some time). Kripke's soundness and completeness proofs showed that the semantics was adequate with respect to the proof system (although an intuitionist may complain that the completeness proof appeals to strictly classical reasoning in the metalevel).
In the case of proof-theoretic semantics, both Dummett and Prawitz conjectured completeness of intuitionistic logic with respect to some kind of proof-theoretic definitions of validity. Recently, some progress have been made with regard to this conjecture. Again, the significance of these results, especially incompleteness, would depend on one's philosophical stance: among other options, one could blame it on the semantics (intuitionistic logic is the target, there is something wrong with the semantic definitions, maybe we can amend them?), one could blame it on the logic (the semantics is OK, the logic is inadequate), one could maintain that there is no one to blame (OK, intuitionistic logic does not fit exactly into this semantics, maybe some other logic does?), or one could not attach any special significance to soundness and completeness proofs in the first place (the distinction between syntax and semantics is already spurious, so, who cares?).
