# Hilbert calculus: Proof that every provable formula has a proof

For my indroduction to logic course I have to proof, that every provable formula has a proof.

It sounds first very funny, second also very logic, still I don't get to make of formally work..

The set of all provable formulas is the smallest set of formulas such that they fulfill the standard properties of Hilbert calculus/system (tautologies, axioms, $\exists$-introduction, modus ponens).

A proof of a formula $\varphi$ is a finite sequence $(\varphi_0,...,\varphi_{n-1})$ of formulas such that $\varphi_{n-1}=\varphi$ and for each $i<n$, either $\varphi_i$ is a tautology, $\varphi_i$ is an axiom, $\varphi_i$ is derived from the previous $\varphi_0,...,\varphi_{i-1}$ using Hilbert-calculus rules.

I tried induction over the stucture of $\varphi$ but didn't get very far and don't think it works that way. Usually our examples are very easy, so I guess there is a pretty simple argument I'm missing, could someone maybe give me a hint? Thanks a lot!!!

## 1 Answer

Hint: Consider the set of formulas that have a proof, and show that it fulfills the standard properties of Hilbert calculus.

• Thank you! That all formulas, that have a proof fulfill the standard properties of Hilbert calculus is pretty obvious from the definition of a proof, or am I missing something? Since the set of all formulas is the SMALLEST to fulfill those properties, they then have to be the same. Is that how you close it up? – user121314 May 7 '14 at 22:58
• Yes, that's it.. – Berci May 7 '14 at 23:01
• Ok that was really a short one :D Thanks s lot for the hint!!! – user121314 May 7 '14 at 23:03