[solinent]

Essentially, all logically valid formulae have proofs in first-order logics.

Remember, logically valid formulae means that if you enumerate all possible interpretations (boolean values for the variables), the formulae remains true.

So you could prove everything that ever exists by creating a set of all possible proofs using the given deduction rules.

[xamuel]

This is 1st-order logic so it's a bit more complicated, though you're on the right track (what you stated is the completeness theorem for propositional logic, not first-order logic).

Rather than boolean values for the variables, you need to enumerate all possible...

* Ambient universes where the language is interpreted

* Values (taken from the ambient universe) for the constant symbols

* Sets-of-tuples-of-values (from the ambient universe) for the predicate symbols

* Functions-from-tuples-of-values-to-values (from the ambient universe) for the function symbols

[solinent]

Yup, my definition of interpretation was limited for pedagogical purposes, but I should have been clearer. The propositional logic version is much simpler to understand, but the implications of the theorem are much more interesting in first-order logic, so introducing all of this nomenclature may be too much for someone who isn't motivated yet.