What does “prove” mean?

Question

What does "prove" mean?

I am using the following examples to understand the general cases. I don't know how to articulate my questions in the general case. I was wondering about at what levels the followings are stated, how the followings are formulated, and what differences and relations are between them :

1. Prove a formula $p$. Does it mean to prove $ \vdash p$ (or $\models p$?), and therefore convert the task to 3 below? ( I may have asked this in some comment, and someone may have replied that proving $p$ means to prove $\vdash p$, but I can't find the comments.)

2. Prove if $\phi$, then $\psi$. Which does it mean to prove: $\phi \to \psi$, $\phi \vdash \psi$, or $\phi \models \psi$, and therefore convert the task to 1 above or 3 below?

3. Prove $\phi \vdash \psi$.

   • Does it mean to derive $\phi \vdash \psi$, by using the inference rules and axioms in a given proof system (e.g. sequent calculus)?

   • Or does it treat $\phi \vdash \psi$ as a formula in a language at a higher level than the language containing $\phi$ and $\psi$, and prove $\vdash (\phi \vdash \psi)$ by applying a given proof system (e.g. sequent calculus) to this higher-level language?

4. Prove if $\phi' \vdash \psi'$, then $\phi \vdash \psi$.

   • Does it mean to derive $\phi \vdash \psi$, by using $\phi' \vdash \psi'$, and the inference rules and axioms in a given proof system (e.g. sequent calculus)?

   • Or does it treat $\phi' \vdash \psi'$ and $\phi \vdash \psi$ as formulas in a language at a higher level than the language containing $\phi$, $\psi$, $\phi'$ and $\psi'$, and prove $(\phi' \vdash \psi') \vdash (\phi \vdash \psi)$ by applying a given proof system (e.g. sequent calculus) to this higher-level language?

5. and 6. Consider replacing $\vdash$ with $\models$ in 3 and 4

Something related: I asked:

Does "provable" or "disprovable" apply only to formulas, not to " an inference " or "derivation" such as $∃𝑥𝑅𝑥⊢∀𝑦𝑅𝑦$? Can we rewrite $∃𝑥𝑅𝑥⊢∀𝑦𝑅𝑦$ as a formula, so that it is derivable (almost) if and only if the corresponding formula is provable?

lemontree replied:

"Provable" means "derivable without premises", that is, provability is a property of formulas whereas derivability is a property of inferences in general. What you are looking for is probably the deduction theorem aka import-export theorem, which states that $𝐴_1,…,𝐴_𝑛⊢𝐵$ if and only if $⊢(𝐴_1∧…∧𝐴_𝑛)→𝐵$. Thus, with $∃𝑥𝑅(𝑥)⊬∀𝑦𝑅(𝑦)$ we have that $⊬∃𝑥𝑅(𝑥)→∀𝑦𝑅(𝑦)$, that is, the formula $∃𝑥𝑅(𝑥)→∀𝑦𝑅(𝑦)$ is not provable.

I guess my questions above are a metalanguage thing, or proof theory, and I know little about them. At the same time, I was also wondering How are proof techniques formulated in mathematical logic?, which might be part of proof theory?

Thanks.

Answer 1

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