Are there other methods of proof other than contrapositive, induction, contradiction, construction, and counter example?

Question

I have only heard of a few methods of proof, namely, contrapositive, induction, contradiction, construction, and counter example. Are there other types of proofs?

Answer 1

Your question is one that I wish other mathematics students ask as well. You probably realize that you've been taught some valid forms of argument, but are now wondering whether there may be some other valid argument forms that are necessary to prove some theorems.

What you're looking for is a formal system, which basically specifies what sentences you can write down given what you have already written down. There is a variety of formal systems, based on different styles of presentation. A few examples are natural deduction (Gentzen's tree-style,Fitch's indentation-style), Hilbert-style calculii, sequent calculus (which can be used to reason about formal systems themselves!).

In some of these, such as Fitch-style natural deduction, what you can write down depends on the current context. For example, in the context where you have assumed that a sentence $A$ is true, of course you can write down $A$, and of course you cannot write $A$ outside that context unless you've already proven it outside, namely without using that assumption. Also, I couldn't find online any user-friendly extension of Fitch-style natural deduction for propositional logic to first-order logic, so please refer to this for a formal specification of such an extension that I personally use.

As I've described it, one does not need to have axioms in a formal system as a separate notion, because each axiom can be treated as a rule instead (it says that you can always write down ...). However, it is sometimes useful to consider axioms as separate from the formal system, namely as the starting collection of sentences on which the rules of the formal system are to be applied to.

It is a surprising fact about classical first-order logic that there is a formal system with rules that can be completely described that can prove every sentence that is true in all situations that satisfy the axioms (called models). This is a non-trivial result, and does not hold for many other logics such as second-order logic. This fact is itself proven in a separate formal system called a meta-system, which is capable of reasoning about sentences and is strong enough to perform certain constructions of models. It turns out that all the formal systems I listed above are sufficient for this purpose, namely that every one of them can prove every sentence that is true for every model, although some of them such as Hilbert-style calculii are extremely not user-friendly, though they can be useful for theoretical analysis of various logics.