Are provable statements true

logicphilosophyprovability

I recently started reading an introductory logic textbook, and I haven't got yet to the chapter that talks about completeness theorem, but I just couldn't wait to read about it using shortcuts. I just read Completeness Theorem and had the below question.

So in the link above, there is a proof for "every true statement is provable" by using Henkin's Theorem: if $T$ is syntactically consistent, then $T$ has a model.

But I am wondering what would be the proof for the converse: every provable statement is true.

Intuitively, this sounds obvious because if $T$ is provable, then in any model, we should be able to use the proof that $T$ is provable. This implies $T$ is provable in any model, (which implies there exists a proof of $T$ in any model???)$\leftarrow$ not sure.

Also, let's say we have a proof that every provable statement is true. But then that just tells me "every provable statement is true" is provable, not necessarily true???

Please assist me!

Best Answer

The completeness theorem is a result about the traditional systems of proof that states $$ (T\vDash \phi) \Rightarrow (T \vdash \phi). $$ That is, if $\phi$ holds in every model where $T$ holds, then there exists a proof of $\phi$ from $T$. Conversely, the soundness theorem states $$ (T\vdash \phi) \Rightarrow (T\vDash \phi), $$ so that if you can prove $\phi$ from $T$ then in every model where $T$ holds, $\phi$ must also hold. The proof of the soundness theorem is considered elementary and goes like this:

(1) First prove that the proof system's laws of inference are truth-preserving. That is, any result deduced from statements true in model are also true in that model.

(2) Use induction on proof length to show that the last line of any finite length proof must be true in a model if the assumptions are true in that model.

My final comment is that you seem to be confusing theory with metatheory. When we carry out the proof sketched above we are trusting our metatheory, the set of assumptions we use when performing formal deductions on logical systems, to make true statements about our theory. But we can't expect the metatheory to logically vindicate itself, because at some point we have to just trust our assumptions.