I've run into the following question concerning the Suppes system of inference, that consists of the typical Modus Ponens, introduction and elimination rules and conditional and indirect proofs.
Which of the following claims concerning the Suppes inference system are true?
- If $\vdash_S\phi$, then the proof of the formula $\phi$ is finite.
- If $\vdash_S\phi$, then the proof of the formula $\phi$ is unique.
- There are a finite number of provable theorems in the Suppes system
- If $\vdash_S\phi$, then $\Sigma\vdash_S\phi$ for any set of premises $\Sigma$.
Inference and provability are defined as follows:
- A sentence $\phi$ can be inferred with the Suppes system from a set of premises $\Sigma$, denoted $\Sigma\vdash_S \phi$, if and only if there exists a Suppes-proof $\alpha_1, \ldots, \alpha_n$, so that $\alpha_n = \phi$ and the suppositional assumption or hypothesis $H_n = \emptyset$.
- A sentence is a theorem or provable in a Suppes system, if and only if $\emptyset \vdash_S \phi$, or written more concisely, $\vdash_S\phi$.
My issue
I'm not sure what a finite proof is, or what it means for a proof to be unique. In the first place, I could pedantically add an infinite number of useless steps to a finite proof and make it infinite. This would only pose a problem to the first part of the definition (inferrability), but is the question asking about inferrability or provability? In the same vein, are two proofs the same, if they consist of the same steps in the same order, or does order not matter?
Second, How would I even begin to observe if there are a finite number of proofs in a system of inference?
Thirdly (and this is not really a question but more of a possibly wrong comment), I'm pretty sure that it doesn't make sense for us to be able to start from any set of premises $\Sigma$, and end up with a valid proof of an arbitrary theorem $\phi$. Isn't there a famous theorem that states something related to this? Something about incompleteness...?