Correctness (logic)

from Wikipedia, the free encyclopedia

Correctness ( English soundness ) is an important property of formal systems or calculi and concerns the connection between syntax and semantics , which is colloquially: What can be formally derived is also true, provided that the premises of the derivation are true.

In formal logic, derivability is expressed by the syntactic derivation operator and inferences by the semantic inference relation : A calculus is called correct if it always follows for sets of statements and from . The semantics of closing is defined in terms of model theory. holds if and only if every model of is also a model of .

For the correctness of a calculus it is sufficient if every single derivation rule is valid. In a correct calculus, which also correctly describes a selected model, no formula can be derived that is not true in the selected model. However, a correct calculation does not help when he describes the model wrong by axioms (z. B. postulated for a calculus of natural numbers that zero has a predecessor) or inconsistent (z. B. postulated for a calculus of natural Numbers that the zero has a predecessor and has no predecessor). From such a correct calculus, formulas can be derived that are not true in the selected model.

The opposite of correctness is the completeness of a formal system. It says: What is semantically correct can also be derived. Completeness sentences are usually much more difficult to prove than correctness sentences; as proof of the correctness of preparing sequent calculus of predicate logic no problems during the completeness theorem is more difficult.

See also

swell

  • Heinz-Dieter Ebbinghaus , Jörg Flum, Wolfgang Thomas: Introduction to Mathematical Logic , 5th Edition, Spectrum Academic Publishing House; 2007, ISBN 978-3827416919
  • Hans-Peter Tuschik, Helmut Wolter: Mathematical logic - in short. Basics, model theory, decidability, set theory , BI science . Verlag, Mannheim-Leipzig-Vienna-Zurich 1994, ISBN 3-411-16731-9 .

Individual proof

  1. Ebbinghaus, Introduction to Mathematical Logic, Mannheim-Leipzig-Vienna-Zurich 1992, p. 74