4
$\begingroup$

When proving a mathematical statement $p \Rightarrow q$, we normally do it:

1) Assuming $p$, then showing $p \Rightarrow q$ (Direct proof)

2) Assuming $¬q$, then showing $¬q \Rightarrow ¬p$. (Indirect proof by counterpositive)

3) Assuming $p$ and $¬q$, then reaching a contradiction. (Indirect proof by absurd).

Is there any way to prove a statement besides these 3?

I think this is a very natural question and probably it has been already asked in this website, but I did not find anything related in search. Also I am not really sure that proof theory is a proper tag.

$\endgroup$
  • $\begingroup$ There is proof by induction. Would you say that induction falls into one of the three categories you listed? It's not obvious, to me, that it does. $\endgroup$ – NicNic8 Jul 2 '18 at 2:52
  • 3
    $\begingroup$ Here's a list of 36 types of mathematical proof, among them: Proof by Intimidation ("Don't be stupid; of course it's true!") and Proof by Illegibility. See also the list on this page. $\endgroup$ – Blue Jul 2 '18 at 3:29
  • $\begingroup$ @Blue: I just saw this question, and my first thought was "by handwaving". Then I saw the list you linked to. However, handwaving isn't among these! I guess by general agreement and by plausibility might be close enough, however. I've had quite a few handwaving proofs presented in classes I've taken (most of which, but not all, I was told were handwaving proofs)! $\endgroup$ – Dave L. Renfro Jul 3 '18 at 18:02
3
$\begingroup$

There are several issues with what you've said. First, you've not stated the rules clearly/correctly. The first rule would be something like: "If by assuming $P$ we can show $Q$, then we've proven $P\Rightarrow Q$." Next, not all statements are of the form $P\Rightarrow Q$. You presumably also want some way of using all these things that you are assuming. In Hilbert-style systems, this is typically modus ponens which states that if we know $P\Rightarrow Q$ and we know $P$ then we can conclude $Q$.

For a typical Hilbert-style system for propositional logic, there is only one rule: modus ponens. The only way to conclude anything in such a system is either 1) for it to be an instance of an axiom, or 2) via modus ponens. There is no concept of "assuming" something in a Hilbert-style system, so none of the rules you mention are part of a Hilbert-style system. Hilbert-style systems are rather inhumane though (but they are very minimalistic which makes them nice for proving meta-theorems about the proof system).

A proof system that much more closely matches informal proofs is natural deduction. (Closely, related is the sequent calculus which has a lot of nice properties but whose rules are usually less intuitive though often easier to work with.) In natural deduction, each connective has its own rules, each split into two groups: introduction rules and elimination rules. Introduction rules show how to conclude a statement involving a connective, while elimination rules show how to make use of a statement involving a connective. Natural deduction also has a notion of proving something under assumptions: hypothetical proofs. Modus ponens is the elimination rule for $\Rightarrow$ (and is called simply $\Rightarrow$-elimination in natural deduction), and the first rule you mention is the introduction rule. In these more structural proof systems, each connective is defined by the rules independently of the other connectives. Often in natural deduction systems, $\neg P$ is defined as $P\Rightarrow\bot$ where $\bot$ is the nullary connective that stands for the always false formula. It is defined by the elimination rule that if under some assumptions we can prove $\bot$, then under those same assumptions we can prove anything. That is, the principle of explosion is the elimination rule for $\bot$. There is no introduction rule.

To support classical logic, we need to add an extra rule or an axiom. Unlike the other rules, this rule will involve multiple connectives which weakens some of the nice properties about natural deduction. (The sequent calculus doesn't have this issue which is one of its nice aspects.) A common choice is essentially your third rule which I'll restate as: if under some assumptions including $\neg Q$ (i.e. $Q\implies \bot$) we can derive $\bot$, then we can prove $Q$ under the same assumptions excluding $\neg Q$. Your second rule is then derivable from the rules for elimination and introduction rules for $\Rightarrow$, the elimination rule for $\bot$, and this last rule.

For classical propositional logic, you could reduce every formula to one involving only $\Rightarrow$ and $\neg$ or $\Rightarrow$ and $\bot$. So the four rules indicated above suffice to prove everything for this logic. For first-order logic, you'll need to add additional rules for the quantifiers. Even Hilbert-style systems usually take universal generalization (i.e. $\forall$-introduction) as an additional rule. Still, proving $P\lor Q$ by assuming $\neg P$ and showing $Q$ will often be a bit silly. In natural deduction, $\lor$ has two introduction rules, namely: if we can prove $P$ (under some assumptions), then we can prove $P\lor Q$ (under the same assumptions), and if we can prove $Q$, then we can prove $P\lor Q$. These rules are derivable from the four rules mentioned above if we define $P\lor Q$ as $(P\Rightarrow\bot)\Rightarrow Q$. We can derive the rules for all the other propositional connectives in terms of the four rules I mentioned given suitable definitions of those connectives in terms of $\Rightarrow$ and $\bot$. We can also, of course, derive a limitless set of additional rules to capture common patterns of reasoning such as the contrapositive rule. We can also make a different choice for what connectives and rules we want to take as primitive.

While I would say the first rule you mention ($\Rightarrow$-introduction) is intimately related to $\Rightarrow$, the other two are not particularly related to it. They are intimately related to classical logic, but both are not necessary and, given some other rule/axiom to incorporate classical logic, both could potentially be derivable. There is no reason to include both of the latter two rules as being somehow special, while excluding the infinite number of other derivable rules that conclude $P\Rightarrow Q$.

$\endgroup$
  • $\begingroup$ "The only way to conclude anything in such a system is either 1) for it to be an instance of an axiom, or 2) via modus ponens." That could hold for the definition of a proof. However, oftentimes such as in Frege or Lukasiewicz, a formula could also be an instance of a formal theorem instead of an instance of an axiom. $\endgroup$ – Doug Spoonwood Jul 3 '18 at 18:39
2
$\begingroup$

When proving a mathematical statement $p \Rightarrow q$, we normally do it:

1) Assuming $p$, then showing $p \Rightarrow q$ (Direct proof)

2) Assuming $¬q$, then showing $¬q \Rightarrow ¬p$. (Indirect proof by counterpositive)

3) Assuming $p$ and $¬q$, then reaching a contradiction. (Indirect proof by absurd).

Is there any way to prove a statement besides these 3?

Yes. In adddition, you could either:

4) Prove $q$ is true.

5) Prove $p$ is false.

Amazing but true, both these methods follow directly from the truth table for $p\implies q$. In the truth table, $p\implies q$ is true whenever $q$ is true. Likewise, $p\implies q$ is true whenever $p$ is false, .

$\endgroup$
1
$\begingroup$

When you need to prove that some statement is true for any $n \in \mathbb{N}$ you can do induction. The process looks like domino. You prove the statement is true for some small natural number (usually $n=1)$, and you prove that if your statement is true for any $k\in\mathbb{N}$, so it's true for $k+1$.

For example, prove the following: $$1+2+3+\cdots+n=\frac{n(n+1)}{2} $$

For $n=1$, we have $1+2+3+\cdots+n=1=\frac{1(1+1)}{2}=\frac{n(n+1)}{2}$.

Now, we suppose for any $k\in\mathbb{N}$ the statement is true, and we will use this to prove it's true for $n=k+1$. We have $$1+2+\cdots+n=1+2+\cdots+k+(k+1)=\frac{k(k+1)}{2}+(k+1)=\frac{k^{2}+k+2k+2}{2}=\frac{k^{2}+3k+2}{2}=\frac{(k+1)(k+2)}{2}=\frac{n(n+1)}{2}. $$

$\endgroup$
  • 2
    $\begingroup$ this is a form of a direct proof $\endgroup$ – gt6989b Jul 2 '18 at 3:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.