Double turnstile
Double Turnstile[edit | edit source]
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[edit | edit source]
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[edit | edit source]
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[edit | edit source]
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[edit | edit source]
References[edit | edit source]
- Enderton, H. B. (2001). A Mathematical Introduction to Logic. Academic Press.
- Mendelson, E. (2015). Introduction to Mathematical Logic. CRC Press.
External Links[edit | edit source]
- Model-Theoretic Semantics on the Stanford Encyclopedia of Philosophy
Navigation: Wellness - Encyclopedia - Health topics - Disease Index - Drugs - World Directory - Gray's Anatomy - Keto diet - Recipes
Search WikiMD
Ad.Tired of being Overweight? Try W8MD's physician weight loss program.
Semaglutide (Ozempic / Wegovy and Tirzepatide (Mounjaro / Zepbound) available.
Advertise on WikiMD
WikiMD is not a substitute for professional medical advice. See full disclaimer.
Credits:Most images are courtesy of Wikimedia commons, and templates Wikipedia, licensed under CC BY SA or similar.
Translate this page: - East Asian
中文,
日本,
한국어,
South Asian
हिन्दी,
தமிழ்,
తెలుగు,
Urdu,
ಕನ್ನಡ,
Southeast Asian
Indonesian,
Vietnamese,
Thai,
မြန်မာဘာသာ,
বাংলা
European
español,
Deutsch,
français,
Greek,
português do Brasil,
polski,
română,
русский,
Nederlands,
norsk,
svenska,
suomi,
Italian
Middle Eastern & African
عربى,
Turkish,
Persian,
Hebrew,
Afrikaans,
isiZulu,
Kiswahili,
Other
Bulgarian,
Hungarian,
Czech,
Swedish,
മലയാളം,
मराठी,
ਪੰਜਾਬੀ,
ગુજરાતી,
Portuguese,
Ukrainian
Contributors: Prab R. Tumpati, MD