Model-theory and Proof-theory in Propositional Logic
I'm trying to link results of model theory and proof-theory in propositional language.
Here i will use $\models$ to denote logical consequence, in the model-theory sense. Being $x,y$ two formulas of a propositional language , we say that $x \models y$ if every interpretation (or truth-assignment) that satisfies $x$ (makes $x$ true), also satisfies $y$.
I'm using $\models x$ to denote that $x$ is a tautology, that is, every interpretation satisfies it.
I'm using $\vdash x$ to denote that $x$ is provable (in the proof-theoretic sense), that is, there exists a formal proof of $x$ (from the axioms, obviously).
I'm using $x \vdash y$ to denote that $y$ is deducible from $x$, that is, there exists a formal deduction of $y$ from $x$ (a list where each formula is either $x$, one of the axioms, or obtained preeceding formulas in the list, by the use of a rule of inference).
Now, i'm following a book (Mathematical Logic, Kleene) that states that the following four expressions are equivalent :
- $\models x \to y$
- $\vdash x \to y$
- $x \models y$
- $x \vdash y$
I'm particularly interested in seeing the intuition (or maybe some more formal proof) that expression 3 is equivalent to 4 , that is, if $y$ is a logical consequence from $x$, then $y$ is deducible from $y$, and if $y$ is deducible from $x$, then $y$ is a logical consequence from $x$. How do we link the syntactical (proof-theory) with the semantic (model-theory) aspect on that case ?
Any hints ?
Thanks in advance !
Solution 1:
About intuition.
Aristotle introduced a notion of consequence along the following lines. Suppose $A$ and $B$ are sentences, each of them either true or false. We study the relation :
(1) 'If A is true, then B has to be true too'.
Many logicians reckoned that the main use of logic is derive conclusions from premises, with the obvious goal that if we start from true premises, and we use “logical rules”, we will derive true conclusions. This idea of logic gives rise to the relation :
(2) 'From A, we can prove B'.
Now we try to translate all this into modern terms.
(1) translates into the relation of logical consequence $A \vDash B$ :
'For every interpretation $\mathcal I$, if A is true under $\mathcal I$, then B is true under $\mathcal I$.'
We “generalize” it putting in place of the sentence A a set $\Gamma$ of sentences :
$\Gamma \vDash \varphi$
which means that :
'For every interpretation $\mathcal I$, if all of $\Gamma$ are true under $\mathcal I$, then $\varphi$ is true under $\mathcal I$.'
Lastly, we have the “special acse” when $\Gamma = \emptyset$ : $\vDash \varphi$ means that the sentence $\varphi$ is valid (in propositional logic it is a tautology) when it is true under every interpretation.
In this case, we call it also logical (or universally) valid sentence, meaning that it is true “under all possible circumstances”.
For (2) [see Neil Tennant, Natural logic (1978), page 5], we have that, in order to demonstrate the validity of an argument one needs a proof.
A proof of an argument is a sequence of steps starting from its premisses, taken as starting points, to its conclusion as end. Within a proof each step, or 'inferences', must be obviously valid.
A system of proof is a codification of these obviously valid kinds of inference, which we call rules of inference. A proof in accordance with these rules must, in order to meet the demands of certainty, satisfy the following conditions :
(i) It must be of finite size.
(ii) Every one of its steps must be effectively checkable.
A system of this type is a logical calculus (i.e.proof systems) formalizing the relation of derivability :
$A \vdash B$
which is :
'B is derivable using only the logical rules of the calculus, starting from A as premise’.
We “generalize” it putting in place of the sentence A a set $\Gamma$ of sentences :
$\Gamma \vdash \varphi$.
Lastly, we have the “special case” when $\Gamma = \emptyset$ : $\vdash \varphi$ means that the sentence $\varphi$ is theorem of the calculus (it is provable) when it is derivable from no premises.
Obviously there must be no invalid proofs in our system : the system must be sound.
Moreover we wish to be able to prove any valid argument expressible in the language. The system, that is, must be complete (or adequate).
Soundness : if $\Gamma \vdash \varphi$, then $\Gamma \vDash \varphi$ (with the particular case : if $\vdash \varphi$, then $\vDash \varphi$)
Completeness : if $\Gamma \vDash \varphi$, then $\Gamma \vdash \varphi$ (with the particular case : if $\vDash \varphi$, then $\vdash \varphi$).
Solution 2:
Kleene's Theorems 12 and 14 imply the equivalence of "1: |= x -> y" and "2: |- x -> y"
For the equivalence of "3: x |= y" and "4: x |- y" the following will work, though you might want to note how it switches between different versions or types of what one might call "modus ponens" throughout:
Suppose that x $\vdash$ y. By the deduction (meta) theorem it follows that $\vdash$ (x $\rightarrow$ y). Theorem 12 of Kleene's Mathematical Logic p. 43 (soundness) says "if $\vdash$E, then |=E". Thus, by modus ponens and substitution, it follows that |=(x$\rightarrow$y). Now suppose we have x as true (or |=x). The rule of modus ponens in model theory implies that y is true. Or even without the rule of modus ponens in model theory, looking at the truth tables here we can infer that y is true, or in symbols |=y. Thus, we may infer that x|=y.
Suppose that x|=y. Suppose that it is not the case that |=(x$\rightarrow$y). Then "x" would have to come as true, and y would have to come as false, as this is the only instance where |=(x$\rightarrow$y) fails. But, if so, then x|=y would fail also. So, if x|=y, then |=(x$\rightarrow$y). Since we have x|=y, by modus ponens we may now infer |=(x$\rightarrow$y). Theorem 14 p. 14 reads "if |=E, then $\vdash$E". So, by modus ponens and substitution, we may infer that $\vdash$(x$\rightarrow$y). Now suppose that x is either an axiom or obtainable from the axioms using the primitive proof-theoretic rule of modus ponens. Since we have $\vdash$(x$\rightarrow$y), and $\vdash$x by hypothesis, by the proof-theoretic version of modus ponens it follows that $\vdash$y. Thus, we may infer that x$\vdash$y.
That 4 is equivalent to 2 follows from the deduction metatheorem and modus ponens. Via chaining of equivalences, this implies all 4 statements equivalent for Kleene's system.