Double turnstile

Double Turnstile

A double turnstile is a logical symbol used in formal logic, particularly in the context of model theory and proof theory. It is denoted by the symbol "\( \vDash \)" and is used to express semantic entailment or logical consequence.

Usage in Logic

In formal logic, the double turnstile symbol "\( \vDash \)" is used to indicate that a particular set of formulas semantically entails another formula. This means that in every model where the set of formulas is true, the entailed formula is also true.

For example, if \( \Gamma \) is a set of formulas and \( \phi \) is a formula, the expression:

\[ \Gamma \vDash \phi \]

means that \( \phi \) is a logical consequence of \( \Gamma \). In other words, every model that satisfies all the formulas in \( \Gamma \) also satisfies \( \phi \).

Comparison with Single Turnstile

The single turnstile symbol "\( \vdash \)" is used in proof theory to denote syntactic derivability. It indicates that a formula can be derived from a set of formulas using a formal proof system. The distinction between the single and double turnstile is crucial:

• "\( \Gamma \vdash \phi \)" means \( \phi \) can be derived from \( \Gamma \) using a formal proof system.
• "\( \Gamma \vDash \phi \)" means \( \phi \) is true in every model where \( \Gamma \) is true.

The relationship between these two concepts is captured by the soundness and completeness theorems:

• A proof system is sound if whenever \( \Gamma \vdash \phi \), it follows that \( \Gamma \vDash \phi \).
• A proof system is complete if whenever \( \Gamma \vDash \phi \), it follows that \( \Gamma \vdash \phi \).

Applications

The double turnstile is widely used in various branches of logic and computer science, including:

• Model theory, where it is used to study the relationships between formal languages and their interpretations or models.
• Automated theorem proving, where it helps in understanding the logical consequences of a set of axioms.
• Formal semantics, where it is used to define the meaning of logical expressions in terms of truth in models.

Related Concepts

• Entailment
• Logical consequence
• Model theory
• Proof theory
• Soundness
• Completeness

References

• Enderton, H. B. (2001). A Mathematical Introduction to Logic. Academic Press.
• Mendelson, E. (2015). Introduction to Mathematical Logic. CRC Press.

External Links

• Model-Theoretic Semantics on the Stanford Encyclopedia of Philosophy