Soundness | EPFL Graph Search

Are you an EPFL student looking for a semester project?

Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.

In logic or, more precisely, deductive reasoning, an argument is sound if it is both valid in form and its premises are true. Soundness also has a related meaning in mathematical logic, wherein logical systems are sound if and only if every formula that can be proved in the system is logically valid with respect to the semantics of the system. In deductive reasoning, 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: (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, penguins). For an argument to be sound, the argument must be valid and its premises must be true. 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 of sentences in its language, if , then . 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.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related concepts (33)

Related courses (2)

Related lectures (18)

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u

MATH-305: Introduction to partial differential equations

This is an introductory course on Elliptic Partial Differential Equations. The course will cover the theory of both classical and generalized (weak) solutions of elliptic PDEs.

Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or logical truths. It studies how conclusions follow from premises due to the structure of arguments alone, independent of their topic and content. Informal logic is associated with informal fallacies, critical thinking, and argumentation theory. It examines arguments expressed in natural language while formal logic uses formal language.

Deductive reasoning is the mental process of drawing deductive inferences. An inference is deductively valid if its conclusion follows logically from its premises, i.e. it is impossible for the premises to be true and the conclusion to be false. For example, the inference from the premises "all men are mortal" and "Socrates is a man" to the conclusion "Socrates is mortal" is deductively valid. An argument is sound if it is valid and all its premises are true.

What is a Formal Proof?CS-550: Formal verification

Covers the concept of formal proof systems, their structure, and soundness.

Automating First-Order Logic Proofs Using Resolution CS-550: Formal verification

Covers first-order logic, resolution proofs, Skolem functions, and satisfiability checking in mathematics and program verification.

Propositional Resolution CS-550: Formal verification

Explores completeness in propositional logic, resolution on clauses, conjunctive form, unit resolution, SAT solvers, and proof generation.