Choosing axiom schemes for a logical theory In a Hilbert system, there are many ways that we can choose axiom schemes. My question is:
1- How do we know that we have defined enough schemes? What would happen if I remove a scheme from the list?
2- How do we decide on the form of these schemes?
3- How can we determine that a particular choice of axioms results in a consistent theory?
Please also let me know if you know a source that discusses such issues.
 A: I think you are talking about adding axiom schemes to the deductive system. The ultimate goal for the deductive system is soundness and completeness: a sentence should be provable if and only if it is true in every model. So there are "enough" schemes when this is provable for the system that has been defined. 
If you remove schemes from a typical system, the resulting system is not complete - typical systems in books don't include redundant schemes. But it would be possible to include redundant axiom schemes if you wanted.
There is no algorithm to decide on the form of the schemes. Investigation leads to ideas for possible schemes, and then in the end the key is to prove soundness and completeness. But there are many different Hilbert systems based on different schemes.
There are two general ways that we prove a set of schemes is consistent. One is to show that the set of true formulas in a model is preserved under the schemes: we cannot take a set of true formulas in any model and deduce a formula that is false in that model.   The other way, which is part of the field of proof theory, is to analyze the structure of a derivation using the schemes, and somehow show that no such derivation can end in an inconsistent result. However, is it usually straightforward to show that the logical axiom schemes are consistent - the usual challenge is with the non-logical axioms of a particular theory. 
