What does "prove" mean?

“To prove” in mathematics means to write a proof of a statement in the context of a mathematical theory. A proof will be an "argument" starting from the axioms of the theory and previous proven results and concluding with the statement to be proved that uses logical "correct" deductive steps (i.e. a valid argument).

In logic we have the concept of derivation i.e. the formal mathematical model of a proof in the context of a logical calculus e.g. Natural Deduction.

The logical deductive steps are usually formalized through inference rules, that are the basic building blocks of the proof system, aka: "logical calculus".

Trying to follow Ebbinghaus's textbook, the symbol $\vDash$ is a meta-language expression used in the semantical context with different usages: flanked to the right by a formula it abbreviates “it is valid” (page 35); between the name of a set of formulas and a formula it abbreviates “it is a consequence of” (page 33).

Finally, flanked by the name of an interpretation and a formula it abbreviates "it is true under the interpretation".

It is not part of the formal language of the calculus: it is used to express properties of the formulas of the calculus; in the context of propositional calculus, we read expression "$⊨ A ∨ ¬A$" as “formula ... is a tautology”, i.e. it is a valid formula of propositional calculus.

We can prove (in the meta-theory) that formula $A ∨ ¬A$ is a tautology using truth table method (this "proof" is a mathematical proof, and not a derivation in the calculus).

Similar for the symbol $\vdash$ (see definition page 61).

Following Ebbinghaus, $\varphi \to \varphi$ is a formula i.e. an expression of the formal language that we read: “if $\varphi$, then $\varphi$”.

We can easily derive it in the proof system and we symbolize the existence of such a derivation with $\vdash \varphi \to \varphi$ which again is not a formula of the formal language but an expression of the meta-language abbreviating the statement: “there is a derivation of....” and we read it (as per answer to your previous post): “formula... is derivable (in the calculus)".

Unfortunately, in some formulation of ND and Sequent Calculus the symbol $\vdash$ is part of the formal language, in which case we can have trouble using it also in the meta-theory.

Finally, we have to consider the Soundness and Completeness Theorem, a meta-theorem that holds for propositional calculus as well as for predicate one (see page 70 and page 75) that say in a nutshell:

“$\vdash \text { iff } \vDash$”.

This theorem expresses a property of the calculus and its semantics. We prove it in a “standard” mathematical way.

As said above, we can use the truth table to prove that $A ∨ ¬A$ is a tautology ($⊨ A ∨ ¬A$) and then use Completeness to prove $⊢ A ∨ ¬A$.

In this way, we use an argument (truth table) to prove a "semantical" property of a certain formula and then use a meta-theorem (Completeness) to prove a second property of the same formula: the existence of a derivation in the corresponding proof system.

This is the gist of the two ubiquitous symbols.