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!!!
Hint: Consider the set of formulas that have a proof, and show that it fulfills the standard properties of Hilbert calculus.