How can logical soundness be determined, if it is the rules of the logic itself which dictate what is true and false?

Question

The idea of soundness sounds conceptually intuitive.

Logic commonly has a syntax and a semantics. The syntax is a set of symbols with formation rules for creating new expressions from currently existing one. The semantics are a set of rules explaining the connection between an expression in the logic, and anything - i.e., “p v q” is true when proposition p and proposition q are true. (I imagine there could be much more creative and unconventional examples of how freely you can choose a semantics or an interpretation of your formal language).

Soundness is merely if the formation rules on the syntax side never lead to the derivation of expressions which, under their interpretation, are known to be false. In other words, we don’t want to use a set of logical axioms which is capable of deriving nonsense “proofs”, like that 3 = 7.

Or, do we? Thinking about this, my amateur understanding of logic makes me feel like this doesn’t make sense. For, isn’t the purpose of devising a logic - a formal, deductive system - to discover what is true, in accordance with those axioms and formation rules? Isn’t the point of logic to begin with particular assumptions, and then discover what conclusions, surprising or expected, would follow from them?

To be able to a priori decide what conclusions are false sounds like it utterly defeats the point of logic. In that way, I could simply say: “Gödel’s incompleteness theorem simply can not be true. In this way, I know that the logical system devised in order to prove it must be unsound, since it proved something I consider false.” How can you know that it is false, apart from if it is provable from axioms? But then, that’s the point: if the logic can derive it, then the logic has delivered the result that, according to the logic, the proposition holds.

I know that I am completely wrong, so I would like to know what soundness really is.

---

I am talking about soundness in mathematical logic:

In mathematical logic, a logical system has the soundness property if every formula that can be proved in the system is logically valid with respect to the semantics of the system. In most cases, this comes down to its rules having the property of preserving truth. The converse of soundness is known as completeness.

A logical system with syntactic entailment ⊢ and semantic entailment ⊨ is sound if for any sequence A1, A2,...,An of sentences in its language, if A1, A2,...,An ⊢ C, then A1, A2,...,An ⊨ C. In other words, a system is sound when all of its theorems are tautologies.

Soundness is among the most fundamental properties of mathematical logic. The soundness property provides the initial reason for counting a logical system as desirable. The completeness property means that every validity (truth) is provable. Together they imply that all and only validities are provable.

Most proofs of soundness are trivial. For example, in an axiomatic system, proof of soundness amounts to verifying the validity of the axioms and that the rules of inference preserve validity (or the weaker property, truth). If the system allows Hilbert-style deduction, it requires only verifying the validity of the axioms and one rule of inference, namely modus ponens (and sometimes substitution).

The last boldface sentence is what I mean. “Validity” means the interpretation of the sentence is true with regards to the semantics. To prove soundness, you check the validity of the axioms, and you prove that the formation rules preserve validity. But how can you “check the validity of the axioms”? It sounds deeply philosophical, like it is Platonist rather than formalist - that it believes there is an intrinsic truthhood or falsehood to mathematics which transcends language; the purpose of logic is to try to write down the “Truth” in a valid language.

I do not understand how this is possible. How can you check if an axiom is valid? I thought axioms were a free-for-all. You can have any axiom you want. It will affect the character of the system that comes from that axiom. Axioms are assumptions. They do not need to be true or false. In fact, they are just assumed to be true. And how can you “check”, or prove, that a rule of inference “preserves validity”? In order to do so, I would already need a pre-existing system in place which determines which propositions are true or false; to check if my new logic meets up with that. It’s as if you would need a second logic to compare the first one to.

In other words:

Syntactically, let’s say S1 -> S2 (Sentence 2 can be derived from Sentence 1). In order to check soundness, I want to know, semantically, if the interpretation of S1 and S2 are true (roughly). How can I do that? This is mathematics. I will need a proof that S1 and S2 are actually true assertions. In order to prove them, I will need a deductive system which derives them via rules of inference from axioms.

So, clearly, there is something I fail to grasp.

Answer 1

The updated version of your question indicates that you are interested in the property of soundness as it applies to a formal system of logic. Soundness in this sense is a relation between a formal logic, or more precisely a deductive system, and a formal semantics. Suppose we have a deductive system that proves some sentences as theorems, and we have a formal semantics that assigns truth values to sentences, then that deductive system is sound if every theorem it proves is a valid sentence, and it is semantically complete if every valid sentence is provable. (Some texts use 'tautology' rather than valid sentence, but others use tautology in a more narrow sense.)

What we are trying to achieve is a correspondence between our system of proof and our system of semantics. This correspondence can be achieved in different ways. We may start with a deductive system and work out a semantic theory for it, or we may start with a semantic theory and devise a proof system for it. Or we may start from both ends and proceed iteratively until we get them to agree. It doesn't really matter as long as we end up with the desired soundness relation.

In the case of classical logic, we desire our logic to have the property of preserving truth. Classical logic provides the guarantee that in a valid argument we will never proceed from true premises to a false conclusion. Other logics do different things, and that is why they have different proof systems and different semantics. But in the case of classical logic, we want our proof system to contain axioms that are always and everywhere true, and rules that always preserve truth.

To satisfy ourselves that our axioms and rules do this, we need to check that the axioms themselves are valid sentences under the semantic theory and that the rules never allow a false sentence to be deduced from a true one. This does not imply Platonism about our subject domain, it just means we need to know the semantics of our logical constants. In the case of natural deduction systems, we have only rules and no axioms, so we only need to check the rules.

In your example of a sentence S1 → S2, to check that this is a valid sentence we don't need to know whether S1 and S2 are true, we only need to know whether the sentence "S1 → S2" is valid, which is equivalent to knowing that the relation between S1 and S2 is truth-preserving. For example, we may have as an axiom:

( ¬A → ¬B ) → ( B → A ) 

We don't need to know whether A and B are true, only that the logical constants → and ¬ guarantee the truth of the sentence.

---

Updated to answer additional questions in the comments:

Soundness, speaking quite generally, is a relation between a deductive system and a formal semantics such that anything proved by the deductive system is valid under the semantics. It is a highly desirable feature of a logic. In the case of first-order clasical logic, soundness and completeness with respect to the Tarskian theory of truth was proved by Gödel.

In the second paragraph above, I am considering the challenge of devising a logic. What if we don't want to use first-order classical logic, or we want to extend it in significant ways? We could start by adopting a bunch of axioms and/or rules and then seeing if we can find a formal semantics for them. This happened with modal logics. Back in the 1910s, C. I. Lewis devised formal systems of modal logic by writing down some axioms for them. The axioms included a □ operator with the intended idea that it meant 'necessarily' but at the time there was no formal semantics for these logics. That came later with Kripke in the 1950s with the development of possible world semantics. Many systems of modal logic are provably sound and complete with respect to model theory based on possible worlds.

A similar thing happened with intuitionistic logic. Axiom systems for it were developed by Heyting and Kleene, but it wasn't until the 1950s and 1960s that our friend Kripke provided a formal semantics for it, once again based on possible worlds.

It is possible, though less common, to start with the semantics and devise an axiom system. We may know what sentences we want to come out as true or false, and then formulate an axiom system that succeeds in proving those sentences, and not others.

The proof system of a logic is syntactic in the sense that it has purely syntactic rules that say in effect: if you have formulas of this form then you are allowed to write a formula of that form. It says nothing about truth or falsehood, or any other semantic property. The semantics assigns truth values to the formulas. It is possible, as you suggest, to regard the syntax and semantics of a logic as a single entity. Some critics of model theory say that it is not really semantic, it is just another kind of syntax. I would say this is a minority view. Most people consider that soundness and completeness proofs are substantial results that demonstrate a non-trivial relation between the syntax and the semantics.

I am not sure what you mean by "domain preservation". What we can do with proof systems is show that rules are harmonious and stable, i.e. that introduction and elimination rules are inverses of one another and do not lead to undesirable implications. This also has value in assuring us that logical constants have a well-defined meaning.

Answer 2

The idea of soundness has two different flavours, and perhaps you are confusing them. A logical argument can be sound if the logical is correctly applied and the premises are true. For example:

All the novels of Marco Ocram are unbelievably clever

X is a novel by Marco Ocram

Ergo X is unbelievably clever

That would be a sound argument if X is the name of one of my books. However, by definition you cannot apply that definition of soundness where there are no true/false premises. Take some abstract system of 12-dimensional geometry, say- it does not rest on premises, but on axioms, and it does not make sense to talk about axioms as being true or false. For such systems, there is a different test of soundness, which is whether the choice of axioms, combined with the rules for reasoning from them, leads to consistent conclusions. The system need not reflect 'reality' as such, so whether statements in the system are true or false is necessarily a question of compatibility with the axioms and rules.

Answer 3

Let's untangle 'logic' and 'soundness' first:

1. Logic works with "true" and "false" tags, and rules to manipulate them. Additionally, it's used for communication and checking of systems.
2. Soundness is something more, i.e. for a "sound" statement it needs to be logical and agree with data/evidence. So soundness, in the way you're referring to, can termed as absolute (real world) true/false.

About other things you mentioned:

• So deciding/generating a "sound opinion" based on logic alone wouldn't be enough, you need reasonable evidence as well.
• As far as generation is concerned, it depends on training. Manipulating variables to derive an "unseen" result may be trivial to a trained person, who already vaguely guessed the property was derivable, vs a novice who hasn't built the intuition. Anyway, such manipulation is very useful, assuming your axioms hold. Example: Discovery of Neptune via math. The key here is we had established physical laws by doing reasonably good experiments. So, in a way, it is generation. But, doing a similar thing in the future for some other system wouldn't be that "cool", you'll not say its "new".

FYI, I'm not a philosophy academic.

Answer 4

Meaning and Context

When I am ten, eleven, and twelve years old, my reading comprehension teacher, Ms. Wexler, tells us to decode the meaning of words, phrases, and sentences in context. The thing about words is that they are abstract symbols that we use to evoke the meaning of our sensory context. True and false arise as evaluations of the statement with its context.

Emotions of pleasure and pain actually arise for me - a bad or false argument may cause me pain if I have sufficient grasp of the context. Galileo said something like this about the arguments of respected ancient philosophers. In the context of his observations of motion he said certain ideas of the philosophers, that had been accepted for centuries on the authority of the philosopher, caused him a great pain.

True and not-True (False) are otherwise undefined values that map to propositions and to the conclusion of the argument. This is a relation that the mind maps to the propositions: (p, T) or (p, F) where one assumes that T and F are mutually exclusive so only one value maps to the proposition in the relation. All statements cannot be evaluated as true or not-true - many symbols or statements are vague or fuzzy in context.

Validity and Soundness

https://rintintin.colorado.edu/~vancecd/phil1440/validity.pdf

A deductive argument proves its conclusion ONLY if it is both valid and sound.

Validity: An argument is valid when, IF all of it’s premises were true, then the conclusion would also HAVE to be true. In other words, a “valid” argument is one where the conclusion necessarily follows from the premises. It is IMPOSSIBLE for the conclusion to be false if the premises are true.

So, validity is more about the FORM of an argument, rather than the TRUTH of an argument. So, an argument is valid if it has the proper form. An argument can have the right form, but be totally false, however.

Notice however that, IF the premises WERE true, then the conclusion would also have to be true. This is all that is required for validity. A valid argument need not have true premises or a true conclusion.

On the other hand, a sound argument DOES need to have true premises and a true conclusion:

Soundness: An argument is sound if it meets these two criteria: (1) It is valid. (2) Its premises are true. In other words, a sound argument has the right form AND it is true.

Note #3: A sound argument will always have a true conclusion. This follows every time these 2 criteria for soundness are met. Do you see why this is the case? First, recall that a sound argument is both valid AND has true premises. Now, refer back to the definition of “valid”. For all valid arguments, if their premises are true, then the conclusion MUST also be true. So, all sound arguments have true conclusions.

Answer 5

You are probing the limits of logic, and of certainty. Both are suspect per contemporary thinking in both logic and empiricism.

The Duhem-Quine Thesis is crucial in answering your question. https://faculty.fairfield.edu/rdewitt/Psci/Ch05.pdf

WE CANNOT KNOW with certainty what "truth" is -- because all empirical knowledge is based on inference off a web of assumptions about our world, our observations, and the nature of logic. This includes all empirical observations of our world. Therefore, "soundness" can never be established with certainty.

What we can do, is show validity of a conclusion within an assumed logic system. And we can show coherence of the assumed starting "facts" with a set of other knowledge and assumptions we also hold by.

Also, given logical pluralism, logics themselves are multiple, with multiple alternate conclusions possible off the same set of assumed "facts". Each of these conclusions may be valid within their logic, and the probability of their "soundness" could plausibly be reasonably argued for.

Answer 6

I think of it this way:

There are different classes of logic, in an infinite tower which sort of contain smaller members as subsets. There is first-order logic, like Zermelo-Frankel set theory (ZFC), which is a predicate logic, and not a propositional logic which does not contain quantifiers or relations.

Gödel proved that no first-order theory is sufficient to describe structures with infinite domain, and that in order to concretely describe these structures you would need a stronger logic like second-order logic.

You can't use the given axioms of ZFC or Peano arithmetic to describe the reals or natural numbers. In order to do so you have to expand your logical tools from first-order to second. But then using the second-order logic, it would not be sufficient to describe the "second-order domain" induced by the second-order logic.

It's turtles all the way down...or in this case up.

Aside from the incompleteness of first-order logic is actually a proof of Gödel's called the Completeness Theorem which https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem

From Wikipedia: "Gödel's incompleteness theorems show that there are inherent limitations to what can be proven within any given first-order theory in mathematics."

Answer 7

How can logical soundness be determined, ...

Logical soundness? No, soundness is by definition not a consequence of how logic works. A logical inference is sound or unsound depending on whether the premises are respectively true or false. That the premises are true or false is usually not dependent on logic, but on the real world, so to speak.

... if it is the rules of the logic itself which dictate what is true and false?

It is usually not logic which decides that premises are true or false. It is reality, or the real world, if you prefer.

A logical argument with the premise "Donald Trump is a Martian" would be unsound, not because logic says so, but because the real Donald Trump is not, presumably, a Martian. Another logical argument with the premise "On January 13, 2024, the president of the United States of America is Joe Biden" would be sound, not because logic says so, but because it is true in the real world that Joe Biden is the president at this point in time.

Thus, logic has (usually) nothing to do with soundness, and soundness has nothing to do with logic.

It is indeed possible, in principle, to make up logical arguments where the premises would be true as a consequence of how logic works. However, nobody ever makes this sort of arguments because from a logical truth you could only ever infer another logical truth, which wouldn't say anything about how the real world is.

isn’t the purpose of devising a logic - a formal, deductive system - to discover what is true,

The purpose of creating a formal logic would be to model or emulate human logic so as to extend our innate logical calculus capabilities beyond, hopefully well beyond, what they are as a consequence of our nature. This would indeed help us decide some of the things that are true that we cannot decide today.

Propositional Logic, and by consequence Predicate Logic, both created in the 19th and 20th century, fail in this respect. For example, both are unable to prove the trivial truth that (α → β) ∨ (β → α) is false.

Answer 8

I have been intrigued by this question for a long time, and I had to spend a while studying mathematical logic to get a clearer understanding of the answer to my question. It is possible I did not phrase my question in a way that someone who knew the answer would recognize as the question I intended. In that case, perhaps I can rewrite it someday.

What I believe my question is really getting at is the difference between Tarskian semantics and proof-theoretic semantics. While I am still studying their technicalities, I currently understand their difference to be quite significantly different on philosophical grounds. The following is a sketch of an intuition, and not a confident claim.

To me, Tarskian semantics could have a range of philosophical interpretations, from being a "psychological" view of logical truth, to more Platonist or metaphysical. However, I think we can faithfully represent Tarskian semantics by describing it as literally as possible, to avoid over-interpreting it: Tarskian semantics defines the meaning or interpretation of symbols in a logical language in terms of natural language. This is where we get the seemingly odd (to the initiate, anyway) "definitions" in this type of logic, such as:

Sentence "P" is true if P.

and

"P ∧ Q" is true if P and Q.

To me, these sounds like tautologies, which is why I found it strange that it would be considered a necessary task to prove that a formal system was "sound". The idea makes sense to me that if we define a system of rules which derive new sentences using rules of deduction, we would indeed wish to check if that system corresponded to the "actual nature of truth" of whatever thing it described. Yet, because Tarskian semantics seemed tautological to me, I felt like there were two options:

One, we "check the correspondence between syntax and semantics" by making a second, separate system of logical deductions for the semantics, and then check if these two formal systems "correspond", mathematically (probably "are isomorphic").

Or, we reject "formality" for the semantics. This is the approach I saw in my textbook, Mathematical Logic by Ebbinghaus et al. I found it surprising how significant of a philosophical a claim this mathematical textbook was based on, when it seemed to me like some mathematicians did not think it was particularly noteworthy. This text explicitly says there is a difference between "formal truth" and "mathematical truth", and so the goal of first-order logic is a syntactic system which can be used to prove things about mathematical truth, because the rules it features for its formal proof system corresponds to "actual, real world mathematical truth".

To me, the latter is weirdly anti-formalist. Up until recently I always thought of mathematics as an uncompromisingly formalized discipline. I have been surprised recently to learn just how many mathematicians do not feel this way at all, but actually believe there are limits to formalization, and that in a way it isn't as important to mathematics as some people think.

Luckily, I now believe there is a second option, which is proof-theoretic semantics, largely established by Gentzen (I think). I am new to the details, but I believe the idea is that instead of saying that the symbols in a signature "map to mathematical structures" (which implies they already have their own logic that the syntax is trying to map to), you do not assume there already exists some mathematical structures, let's say defined in a "weak set theory". You actually define the concept of a model, in the syntax. So, once we have a proof-system (a language with a deduction system), we can define a model as a "complete, consistent theory", where a theory is a collection of formulae.

I'll try to define a difference.

In Tarskian semantics, the "satisfaction" relation is defined in that natural language way I outlined above. We judge if a model models a formula basically through human judgment.

In proof-theoretic semantics, the satisfaction relation is defined syntactically, which means that a model satisfies a formula if that formula is "in the model". In this case, a model is a collection of formulas, rather than an "external structure". But I am pretty sure that this means that the satisfaction relation is synonymous with the consequence relation.

I am going to go ahead here and quote Claude 3.5 Sonnet because even if it is factually inaccurate, it does a good job of sketching out a possible way forward regarding what I had in mind:

Here's how we can approach this more rigorously:

Start with a formal language L and a proof system (like natural deduction) defined purely syntactically. Define derivability (⊢) in terms of the proof system. T ⊢ φ means there's a finite sequence of formulas ending in φ, where each formula is either in T, an axiom, or follows from previous formulas by an inference rule. Define consistency: T is consistent if there's no formula φ such that T ⊢ φ and T ⊢ ¬φ. Define completeness: T is complete if for every sentence φ, either T ⊢ φ or T ⊢ ¬φ. Define a "syntactic model" M as a complete, consistent set of sentences. Define "truth in M" (M ⊨ φ) simply as φ ∈ M.

The key point is that we're not using a separate meta-language or "second copy of syntax". Everything is defined in terms of the original syntax and proof system. This approach essentially collapses the distinction between syntax and semantics that exists in traditional model theory. "Truth" becomes equivalent to provability in a complete, consistent theory. Some important points:

This approach doesn't assume any set theory beyond what's needed to talk about formal languages and proof systems. It aligns closely with how we actually use logic in practice (through proofs). It can be extended to develop analogues of many model-theoretic concepts (elementary equivalence, types, etc.) in purely syntactic terms. However, it doesn't provide the intuitive "picture" of models as structures that interpret the language, which many find helpful. Some results that are straightforward in set-theoretic model theory become more complex in this approach.

This syntactic approach to model theory is less common than the set-theoretic approach, but it's a legitimate alternative that avoids some foundational assumptions and provides a different perspective on logical semantics. It's particularly relevant in constructive approaches to logic and in exploring the relationships between syntax and semantics.

Let's unpack this:

In traditional model-theoretic semantics:

Satisfaction (⊨) is defined in terms of truth in a model. Derivability (⊢) is defined in terms of formal proofs. The completeness theorem establishes a connection: Γ ⊨ φ if and only if Γ ⊢ φ (for first-order logic).

In the proof-theoretic approach we've discussed:

There isn't a separate notion of satisfaction based on models. "Truth in M" is defined as membership in M, where M is a complete, consistent set of formulas. Derivability (⊢) is still defined in terms of formal proofs.

The key insight: In this proof-theoretic approach, for a complete theory T: T ⊨ φ (φ is "true" in T) if and only if φ ∈ T if and only if T ⊢ φ

In this proof-theoretic semantics, the notions of consequence/satisfaction and derivability essentially collapse into one another. This is not a flaw but a fundamental feature of this approach. Some implications:

This unification of syntax and semantics is seen as a strength by proponents of proof-theoretic semantics. It avoids the need for a separate semantic theory. It aligns well with philosophical positions that view meaning as grounded in use (like Wittgenstein's later philosophy) rather than in reference to abstract objects. It can be particularly useful in constructive mathematics, where proofs are given primacy over truth in arbitrary models. However, it does make some model-theoretic concepts less intuitive. For instance, the notion of a non-standard model becomes less clear in this framework. This approach can be extended to more complex logical systems, but the details can become intricate, especially for higher-order or non-classical logics.

It's worth noting that while this proof-theoretic approach equates consequence and derivability for complete theories, there's still a distinction for incomplete theories. This preserves some of the richness of the interplay between syntax and semantics that we see in traditional model theory. This proof-theoretic perspective on semantics remains an active area of research in logic and philosophy of mathematics, offering a different lens through which to view foundational issues in logic and mathematics.

Some references:

https://plato.stanford.edu/entries/tarski-truth/

https://plato.stanford.edu/entries/proof-theoretic-semantics/

If anyone wants to correct or edit or refine anything I said, go ahead, as I just want this post to become as accurate as possible. Thanks.