cianfa72
- 2,810
- 298
- TL;DR Summary
- About the use of turnstile symbol ⊢ in metalanguage discourses on the formal system
I was reading documentation about the soundness and completeness of logic formal systems.
Consider the following $$\vdash_S \phi$$
where ##S## is the proof-system making part of the formal system and ##\phi## is a wff (well formed formula) of the formal language. Note the blank on left of the turnstile symbol ##\vdash_S##, as far as I can tell it actually represents the empty set.
So what does it mean ? I guess it actually means ##\phi## is a theorem of the formal system, i.e. there is a formal deductive proof of it starting from the list of axioms included in the formal system (by using the formal system's rules of inference). Therefore, even though the set on the left is left empty, the list of axioms are actually tacitly implied/included.
Does it make sense ? Thanks.
Consider the following $$\vdash_S \phi$$
where ##S## is the proof-system making part of the formal system and ##\phi## is a wff (well formed formula) of the formal language. Note the blank on left of the turnstile symbol ##\vdash_S##, as far as I can tell it actually represents the empty set.
So what does it mean ? I guess it actually means ##\phi## is a theorem of the formal system, i.e. there is a formal deductive proof of it starting from the list of axioms included in the formal system (by using the formal system's rules of inference). Therefore, even though the set on the left is left empty, the list of axioms are actually tacitly implied/included.
Does it make sense ? Thanks.
Last edited: