Deductive proof in logic formal systems

[cianfa72]

TL;DR

About the use of turnstile symbol ⊢ in metalanguage discourses on the target formal language

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 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.

 

[jedishrfu]

When a sequent like: $\Gamma \;\vdash\; \varphi$ is used, it means:

From the set of assumptions/premises $\Gamma$, the formula: $\varphi$ is derivable in the proof system (i.e., there is a formal proof of $\varphi$ using the axioms and inference rules, assuming all formulas in $\Gamma$).

However, when you see: $\;\vdash\; \varphi$ (with nothing before the turnstile),

It's shorthand for $\emptyset \;\vdash\; \varphi$

It means that $\varphi$ is a theorem of the system, derivable from the system’s axioms alone, using the rules of inference. It means that no additional premises beyond those already built into the formal system are needed.

 

[cianfa72]

When a sequent like: $\Gamma \;\vdash\; \varphi$ is used, it means:

Ah ok, so an expression like $\Gamma \;\vdash\; \varphi$ is an instance of a sequent.

As an aside, we can say that a formal system has: a formal language (a set of logical and non-logical symbols taken from the formal language's alphabet), a set of syntax rules for defining wffs within it, a set of axioms and a proof-system (i.e. a set of rules of inference).

So far, no semantic concepts are included in the definition (formal system = purely syntactic).

Semantics comes separately. It comes by adding an intended interpretation (i.e. assign a meaning) to the formal language's non-logical symbols.

Is a formalized logic system or formal theory what we get by adding a semantic to a formal system ?

 

[jedishrfu]

Adding semantics to a formal system doesn’t make it a “formal theory.” A theory involves the addition of specific non-logical axioms. A formal logic (or logical system) is when you combine a formal system with a semantics.

Look at the way a first-order logic system can be transformed into a formal theory like Group Theory when adding some non-logical axioms and then into a functional model through interpretation, like how we apply group theory to the set of real numbers.

---

This is beyond my pay grade, and I defer to @fresh_42 for further refinement and specificity.

-- Jedi

 

[cianfa72]

Adding semantics to a formal system doesn’t make it a “formal theory.” A theory involves the addition of specific non-logical axioms. A formal logic (or logical system) is when you combine a formal system with a semantics.

Ah ok. So the point is: combining a formal system with a semantics (i.e. assigning an interpretation of the non-logical symbols) results in a formal logic (aka logical system). Then to transform it into a formal theory of something some specific non-logical axioms must be added.

Look at the way a first-order logic system can be transformed into a formal theory like Group Theory when adding some non-logical axioms and then into a functional model through interpretation, like how we apply group theory to the set of real numbers.

Another example should be Peano Arithmetic (PA). It is a formal theory in which the underlying formal logic is the first-order logic (its semantics is defined by the structure consisting of the set $\mathbb N$ as domain of discourse plus an intended natural interpretation function $I$ mapping non-logical symbols to "arithmetic" predicates, functions, and constants). Adding to it the set of Peano non-logical axioms one gets the PA formal theory.