I was going through these notesand wanted to understand proposition 2.2.2 on page 20. Which is:

If $\Sigma \vdash p$ then $\Sigma \models p$

I understand what it says but the proof eludes me completely because I do not understand how to connect truth/semantics (i.e. mapping to 0 or 1 according to how we label the atoms with a truth function $t:A \to \{0,1 \}$ and (syntactic) provability. The only thing the text says is:

This should be clear from earlier facts that we stated and which the reader was asked to verify.

However, I have no idea how this suppose to be true at all. Anyone has any ideas how this is done? Why is this suppose to be trivial/obvious? What am I missing/not connecting from what I should know so far?

My difficulty is understanding how we actually come up with a model (i.e. a truth assignment) given only that a formal proof $p_1, \dots, p_n$ exists. The only relationship between truth and provability that we know is that the axioms are tautologies (so any truth assignment to them makes them true, always for any entry in the truth table). Being in $\Sigma$ only means you are in that set but nothing else...essentially, I assume we have to be able construct a truth function but thats not clear.

  • 1
    $\begingroup$ "My difficulty is understanding how we actually come up with a model (i.e. a truth assignment) given only that a formal proof p1,…,pn exists." That's not what you're trying to do, though: you're trying to show that there isn't a model in which $p$ fails. That's much easier to think about in this context than showing that there is a model in which $p$ holds (and indeed just showing that there is some model in which $p$ holds wouldn't show $\Sigma\models p$; you'd need to show that every model of $\Sigma$ satisfies $p$). $\endgroup$ – Noah Schweber Oct 9 '18 at 0:05
  • $\begingroup$ @NoahSchweber lol your right. That was a dum confusion. Still I wouldn't know what to do at all since provability is mainly a syntactic/mechanic thing (except for the axioms which I've already shown are tautologies). $\endgroup$ – Pinocchio Oct 9 '18 at 0:08
  • $\begingroup$ HINT: if its true for some recursively defined structure/set/object, the natural thing is to check if its true using its own inductive definition (proof by induction). $\endgroup$ – Pinocchio Oct 13 '18 at 20:04

This property is called soundness. You don't need to construct a particular valuation, you need to show that $p$ is true in any valuation that satisfies $\Sigma$ (i.e. any valuation such that all the sentences of $\Sigma$ are true).

You can prove it by induction on the length of the proof. $p$ is the last line of a proof from $\Sigma.$ It is either

  1. An axiom instance.
  2. A sentence in $\Sigma.$
  3. An inference from modus ponens applied two previous lines.

You need to show that $\Sigma\models p.$

  1. If $p$ is an axiom, then it is valid, so true in all truth valuations, regardless if they satisfy $\Sigma$. (This assumes you have proven all the axioms are valid previously. If not, do it, it's just a matter of checking their truth tables.)
  2. It is obvious that if $p\in\Sigma$ then $\Sigma \models p.$ In any valuation where all sentences in $\Sigma$ are true, $p$ is true, because $p$ is a sentence in $\Sigma.$
  3. If we have inferred $p$ from previous lines of the proof $p'$ and $p'\to p,$ we may assume by the induction hypothesis that $\Sigma \models p'$ and $\Sigma \models p'\to p.$ Now let $v$ be any valuation satisfying $\Sigma.$ Then since $\Sigma \models p'$ and $\Sigma\models p,$ we have $v(p')=v(p'\to p)=1.$ Using the truth tables for $\to,$ this implies $v(p)=1.$ Thus, since $v$ was an arbitrary valuation satisfying $\Sigma,$ we have $\Sigma \models p.$
  • $\begingroup$ is "induction on length of proof" same as "structural induction"? $\endgroup$ – Pinocchio Oct 8 '18 at 23:51
  • 1
    $\begingroup$ @Pinocchio It is one of many forms of structural induction. $\endgroup$ – spaceisdarkgreen Oct 8 '18 at 23:53
  • $\begingroup$ It's worth noting that this seems to be assuming a Hilbert-style proof system. The proof should also be adaptable to a natural deduction style proof system. For example, in the inductive step for a $\rightarrow I$ proof, suppose we know that $\Sigma, p \models q$. Then for any truth assignment which makes all statements in $\Sigma$ true, if this truth assignment makes $p$ false, then it also makes $p \rightarrow q$ true. On the other hand, if it makes $p$ true, then from the assumption $\Sigma, p \models q$, it follows that the truth assignment makes $q$ true also, so it also... $\endgroup$ – Daniel Schepler Oct 9 '18 at 0:07
  • 1
    $\begingroup$ @Pinocchio Experience, I guess. When you need to prove something holds for all proofs, the natural thing to do is look at is if it holds for very short proofs, and then see if that extends to longer ones. Induction is the way to make this into a rigorous argument. Same goes for 'all terms' or 'all formulas' or all anything that is recursively defined. $\endgroup$ – spaceisdarkgreen Oct 13 '18 at 0:19
  • 1
    $\begingroup$ @Pinocchio Cause you aren't trying to show something about all propositions, you're trying to show something about all proofs (namely that the statement they prove is valid). $\endgroup$ – spaceisdarkgreen Oct 14 '18 at 20:30

We want to show Soundness, i.e. that statements that are provable by our theory $\Sigma$ imply they are true in any model that satisfies our theory. In other words that provable statements only lead to true statements in $\Sigma$.

We will do this by induction on length of proofs. The proof can be done by complete strong induction, but I prefer to write out the whole thing out and explicitly show the base cases.

I will state the induction hypothesis first, for proof of length $n$:

$$ P(n) := \Sigma \vdash p_n \implies \Sigma \models p_n $$

For the base case we want to show $\Sigma \vdash p_1 \implies \Sigma \models p_1$. Thus suppose $\Sigma \vdash p_1$ (now we want to see if we can derive that every model of $\Sigma$ satisfies $p_1$). Thus, $p_1$ is a proof of length 1. Thus, $p_1$ is either a propositional axiom or some statement in our theory:

  1. If $p_1$ is a propositional axiom, then its true under every model. In particular its true under every model that satisfies every statement in $\Sigma$ (since any subset works since the whole set works). Thus $\Sigma \models p_1$.
  2. If $p_1 \in \Sigma$ then since $p_1$ is part of the theory of $\Sigma$ every model satisfies every statement in $\Sigma$ and so it satisfies this one in particular too. Thus, $\Sigma \models p_1$.

Assume assume strong induction $\forall m(m<n \to P(m))$. Now we want to show that implies $P(n)$. If we want to show $P(n)$ then we want to show $\Sigma \vdash p_n$ implies $\Sigma \models p_n$. Thus we (also) assume $\Sigma \vdash p_n$.

Now there are 3 cases:

  1. $p_n$ is a propositional axiom.
  2. $p_n \in \Sigma$
  3. $p_n$ was arrived via Modus Ponens (MP)

1 and 2 are exactly the same argument as in the base case (and don't need the I.H). The third goes as follows:

  1. $p_n$ was arrived via Modus Ponens. Then that means that there were two earlier proposition $p_k$ and $p_{k'} := p_k \to p_n$ in the proof. Since $k < n \land k' < n$ we have by the induction hypothesis that: $ \Sigma \vdash p_k \implies \Sigma \models p_k $ is true and so is $ \Sigma \vdash p_k \to p_n \implies \Sigma \models p_k \to p_n $. Since we assumed they were derived earlier by the proof we also have $\Sigma \vdash p_k$ and $\Sigma \vdash p_k \to p_n$. Thus, we know $\Sigma \models p_k $ and $\models p_k \to p_n $ are valid. Those two statements together give us "semantic Modus Ponens" and therefore we can conclude: $\Sigma \models p_n$ which is what we required.

Thus we have $ \Sigma \vdash p_n \implies \Sigma \models p_n $ for all $n \in \mathbb N$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.