What does "prove" mean?
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 :
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.)
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?
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?
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?
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?
"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.
$\endgroup$ 21 Answer
$\begingroup$β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.
$\endgroup$
