TITLE: Can we prove we know all the ways to prove things?
QUESTION [2 upvotes]: The things like induction and contradiction, they're all ways we prove things. Is that set of ways to prove things complete? Does the self referential nature of this question make it unprovable with something related to Gödel's incompleteness theorem? Has it been proven to be unprovable if this is the case? Is there some proof that shows we have found all the ways to prove things?

REPLY [3 votes]: I feel it is important to clarify some definitions, because there are two distinct notions of completeness: semantic completeness and syntactic completeness. The answer is yes with respect to semantic completeness, but no with respect to syntactic completeness. It seems to me what you are after is semantic completeness.
In what follows, we suppose that we have specified a logical (deductive) system, and a theory in this logical system. For example, take first order logic with ZFC set theory, or first order logic with group theory.
Semantic completeness
A statement $\phi$ in the theory is provable if one can derive it from the rules of the deductive system.
Now for each theory there is the notion of a model of that theory, and given a specific model we can ask whether a statement is satisfied in this model. I won't attempt to define this, but here are some examples: a group is a model for the theory of groups, the set of natural numbers is a model for Peano arithmetic, a set-theoretic universe is a model for set theory. So we define a statement to be valid in a theory if it is satisfied in every model of the theory.
Two reasonable questions we could ask about our system are

Soundness: Does provability entail validity?
(Semantic) completeness: Does validity entail provability?

In general we always ask that our system is sound. For completeness, Gödel's completeness theorem tells us that any theory over first order logic is complete in this sense. For example, the statement $\phi := \forall x,y. (x*y)^{-1} = y^{-1}*x^{-1}$ is something that is true in every group, and indeed, it is easily derivable from the axioms of group theory. This form of completeness also holds for ZFC set theory.
Syntactic completeness
However there is yet another notion of completeness. A theory is (syntactically) complete if for any statement $\phi$, we can either derive $\phi$ or $\neg\phi$ in our system. Now we know that $\phi$ can only be derivable if it is satisfied in every model of our theory, and similarly for $\neg \phi$.
An interesting question is therefore whether our theory has a statement $\phi$ which is satisfied in some model $M$, and its negation $\neg\phi$ is satisfied in another model $N$. If this is the case, then we can deduce that neither $\phi$ nor $\neg \phi$ is derivable in our system (note: this says nothing about the derivability of $\phi\vee\neg\phi$)! For the theory of groups, the statement $\forall x,y. x* y = y * x$ is such a statement, because some groups are abelian and others are not.
Now Gödel's incompleteness theorem tells us that any theory which is strong enough to do arithmetic is incomplete in this way. In fact, there are numerous axioms of set theory which hold in some models of set theory but not others, such as the axiom of choice or the continuum hypothesis, meaning that they are independent of the theory.
{"set_name": "stack_exchange", "score": 2, "question_id": 3773199}