In
logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the study of deductively valid inferences or logical truths. It examines how conclusions follow from premises based on the structure o ...
and
deductive reasoning
Deductive reasoning is the process of drawing valid inferences. An inference is valid if its conclusion follows logically from its premises, meaning that it is impossible for the premises to be true and the conclusion to be false. For example, t ...
, an
argument
An argument is a series of sentences, statements, or propositions some of which are called premises and one is the conclusion. The purpose of an argument is to give reasons for one's conclusion via justification, explanation, and/or persu ...
is sound if it is both
valid in form and has no false
premise
A premise or premiss is a proposition—a true or false declarative statement—used in an argument to prove the truth of another proposition called the conclusion. Arguments consist of a set of premises and a conclusion.
An argument is meaningf ...
s. Soundness has a related meaning in
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
, wherein a
formal system of logic is sound
if and only if
In logic and related fields such as mathematics and philosophy, "if and only if" (often shortened as "iff") is paraphrased by the biconditional, a logical connective between statements. The biconditional is true in two cases, where either bo ...
every
well-formed formula
In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language.
The abbreviation wf ...
that can be proven in the system is logically valid with respect to the
logical semantics of the system.
Definition
In
deductive reasoning
Deductive reasoning is the process of drawing valid inferences. An inference is valid if its conclusion follows logically from its premises, meaning that it is impossible for the premises to be true and the conclusion to be false. For example, t ...
, a sound argument is an argument that is
valid and all of its premises are true (and as a consequence its conclusion is true as well). An argument is valid if, assuming its premises are true, the conclusion ''must be'' true. An example of a sound argument is the following well-known
syllogism
A syllogism (, ''syllogismos'', 'conclusion, inference') is a kind of logical argument that applies deductive reasoning to arrive at a conclusion based on two propositions that are asserted or assumed to be true.
In its earliest form (defin ...
:
: ''
(premises)''
: All men are mortal.
: Socrates is a man.
: ''
(conclusion)''
: Therefore, Socrates is mortal.
Because of the logical necessity of the conclusion, this argument is valid; and because the argument is valid and its premises are true, the argument is sound.
However, an argument can be valid without being sound. For example:
: All birds can fly.
: Penguins are birds.
: Therefore, penguins can fly.
This argument is valid as the conclusion ''must be'' true assuming the premises are true. However, the first premise is false. Not all birds can fly (for example, ostriches). For an argument to be sound, the argument must be valid ''and'' its premises must be true.
Some authors, such as
Lemmon, have used the term "soundness" as synonymous with what is now meant by "validity", which left them with no particular word for what is now called "soundness". But nowadays, this division of the terms is very widespread.
Use in mathematical logic
Logical systems
In
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
, a
logical system
A formal system is an abstract structure and formalization of an axiomatic system used for deducing, using rules of inference, theorems from axioms.
In 1921, David Hilbert proposed to use formal systems as the foundation of knowledge in math ...
has the soundness property if every
formula
In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwe ...
that can be proved in the system is logically valid with respect to the
semantics
Semantics is the study of linguistic Meaning (philosophy), meaning. It examines what meaning is, how words get their meaning, and how the meaning of a complex expression depends on its parts. Part of this process involves the distinction betwee ...
of the system.
In most cases, this comes down to its rules having the property of ''preserving
truth
Truth or verity is the Property (philosophy), property of being in accord with fact or reality.Merriam-Webster's Online Dictionarytruth, 2005 In everyday language, it is typically ascribed to things that aim to represent reality or otherwise cor ...
''.
The
converse of soundness is known as
completeness.
A logical system with
syntactic entailment and
semantic entailment is sound if for any
sequence
In mathematics, a sequence is an enumerated collection of objects in which repetitions are allowed and order matters. Like a set, it contains members (also called ''elements'', or ''terms''). The number of elements (possibly infinite) is cal ...
of
sentences
The ''Sentences'' (. ) is a compendium of Christian theology written by Peter Lombard around 1150. It was the most important religious textbook of the Middle Ages.
Background
The sentence genre emerged from works like Prosper of Aquitaine's ...
in its language, if
, then
. In other words, a system is sound when all of its
theorem
In mathematics and formal logic, a theorem is a statement (logic), statement that has been Mathematical proof, proven, or can be proven. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to esta ...
s are
validities.
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
In mathematics and logic, an axiomatic system is a set of formal statements (i.e. axioms) used to logically derive other statements such as lemmas or theorems. A proof within an axiom system is a sequence of deductive steps that establishes ...
, 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
In propositional logic, (; MP), also known as (), implication elimination, or affirming the antecedent, is a deductive argument form and rule of inference. It can be summarized as "''P'' implies ''Q.'' ''P'' is true. Therefore, ''Q'' must ...
(and sometimes substitution).
Soundness properties come in two main varieties: weak and strong soundness, of which the former is a restricted form of the latter.
Weak soundness
Weak soundness of a
deductive system
A formal system is an abstract structure and formalization of an axiomatic system used for deducing, using rules of inference, theorems from axioms.
In 1921, David Hilbert proposed to use formal systems as the foundation of knowledge in math ...
is the property that any sentence that is provable in that deductive system is also true on all interpretations or structures of the semantic theory for the language upon which that theory is based. In symbols, where ''S'' is the deductive system, ''L'' the language together with its semantic theory, and ''P'' a sentence of ''L'': if ⊢
''S'' ''P'', then also ⊨
''L'' ''P''.
Strong soundness
Strong soundness of a deductive system is the property that any sentence ''P'' of the language upon which the deductive system is based that is derivable from a set Γ of sentences of that language is also a
logical consequence
Logical consequence (also entailment or logical implication) is a fundamental concept in logic which describes the relationship between statement (logic), statements that hold true when one statement logically ''follows from'' one or more stat ...
of that set, in the sense that any model that makes all members of Γ true will also make ''P'' true. In symbols, where Γ is a set of sentences of ''L'': if Γ ⊢
''S'' ''P'', then also Γ ⊨
''L'' ''P''. Notice that in the statement of strong soundness, when Γ is empty, we have the statement of weak soundness.
Arithmetic soundness
If ''T'' is a theory whose objects of discourse can be interpreted as
natural numbers
In mathematics, the natural numbers are the numbers 0, 1, 2, 3, and so on, possibly excluding 0. Some start counting with 0, defining the natural numbers as the non-negative integers , while others start with 1, defining them as the positiv ...
, we say ''T'' is ''arithmetically sound'' if all theorems of ''T'' are actually true about the standard mathematical integers. For further information, see
ω-consistent theory
In mathematical logic, an ω-consistent (or omega-consistent, also called numerically segregative) W. V. O. Quine (1971), ''Set Theory and Its Logic''. theory is a theory (collection of sentences) that is not only (syntactically) consistentS. C. ...
.
Relation to completeness
The converse of the soundness property is the semantic
completeness property. A deductive system with a semantic theory is strongly complete if every sentence ''P'' that is a
semantic consequence of a set of sentences Γ can be derived in the
deduction system
A formal system is an abstract structure and formalization of an axiomatic system used for deducing, using rules of inference, theorems from axioms.
In 1921, David Hilbert proposed to use formal systems as the foundation of knowledge in math ...
from that set. In symbols: whenever , then also . Completeness of
first-order logic
First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...
was first
explicitly established by
Gödel, though some of the main results were contained in earlier work of
Skolem.
Informally, a soundness theorem for a deductive system expresses that all provable sentences are true. Completeness states that all true sentences are provable.
Gödel's first incompleteness theorem shows that for languages sufficient for doing a certain amount of arithmetic, there can be no consistent and effective deductive system that is complete with respect to the intended interpretation of the symbolism of that language. Thus, not all sound deductive systems are complete in this special sense of completeness, in which the class of models (up to
isomorphism
In mathematics, an isomorphism is a structure-preserving mapping or morphism between two structures of the same type that can be reversed by an inverse mapping. Two mathematical structures are isomorphic if an isomorphism exists between the ...
) is restricted to the intended one. The original completeness proof applies to ''all'' classical models, not some special proper subclass of intended ones.
See also
*
Soundness (interactive proof)
In computational complexity theory, an interactive proof system is an abstract machine that models computation as the exchange of messages between two parties: a ''prover'' and a ''verifier''. The parties interact by exchanging messages in order ...
*
Type soundness
In computer science, type safety and type soundness are the extent to which a programming language discourages or prevents type errors. Type safety is sometimes alternatively considered to be a property of facilities of a computer language; that i ...
References
Bibliography
*
*
*Boolos, Burgess, Jeffrey. ''Computability and Logic'', 4th Ed, Cambridge, 2002.
External links
Validity and Soundnessin the ''
Internet Encyclopedia of Philosophy
The ''Internet Encyclopedia of Philosophy'' (''IEP'') is a scholarly online encyclopedia with around 900 articles about philosophy, philosophers, and related topics. The IEP publishes only peer review, peer-reviewed and blind-refereed original p ...
.''
{{Mathematical logic
Arguments
Concepts in logic
Deductive reasoning
Model theory
Proof theory