Skip to main content
69 votes
Accepted

Does every proof need an axiom saying it works?

This is a complicated question to answer for multiple reasons. We really have to say something about the foundational crisis to give a full account of the story here. Here is a caricatured brief ...
Qiaochu Yuan's user avatar
50 votes
Accepted

Are there statements so self-evident that writing a proof for them is meaningless? Is this an example of one?

Great question, and well done for thinking carefully about the basics of proof and mathematics. Let's get into it! It seems that you are just supposed to know that "all integers divisible by 4 ...
diracdeltafunk's user avatar
38 votes

Should a mathematical proof be 'convincing'?

The primary reason to write down a proof is in order to communicate with other mathematicians. If mathematicians acquainted with the relevant literature cannot understand your argument (i.e: do not ...
Andres Mejia's user avatar
  • 21.1k
25 votes

Each person has at most 3 enemies in a group. Show that we can separate them into two groups where a person will have at most one enemy in the group.

Split the house however you like. Let $E_i$ be the number of enemies person $i$ has in their group, and let $E = \sum E_i.$ For any person having more than $1$ enemy in their group, i.e. at least $2$, ...
cats's user avatar
  • 4,328
18 votes

What is the theorem that has the most proofs?

Well, there was a book with 367 proofs of the Pythagorean Theorem published. I'm sure there's more.
Alan's user avatar
  • 16.8k
16 votes
Accepted

Deriving A, ¬A ⊢ B in a weak Hilbert proof system

Mayhap you missed an additional axiom, or whoever assigned this problem tried to pull a fast one on you? Either way, you cannot derive $A \rightarrow \neg A \rightarrow B$ in the Hilbert system given ...
Z. A. K.'s user avatar
  • 11.9k
16 votes

Are there statements so self-evident that writing a proof for them is meaningless? Is this an example of one?

No Nothing is "self-evident" in mathematics, although this is a relatively new position (circa. 150 years). For millennia, mathematicians considered axioms (or postulates) to be self-evident,...
Dale M's user avatar
  • 2,979
15 votes

Each person has at most 3 enemies in a group. Show that we can separate them into two groups where a person will have at most one enemy in the group.

The question is ambiguous in two ways: we are not told whether being an enemy is a symmetric or asymmetric relation, nor whether the parliament has a finite or infinite number of members. I will show ...
bof's user avatar
  • 79.6k
14 votes
Accepted

Is "first-orderizability" a requirement for "legitimate" mathematical reasoning?

Yes, when someone says that ZFC is a suitable foundation for mathematics, that means that all standard mathematical notions can be expressed in the language of ZFC using first-order logic and all ...
Mitchell Spector's user avatar
13 votes
Accepted

What is "magic" about the combination of addition and multiplication in formal arithmetic?

Looking back at this question I'm quite dissatisfied with my original answer: it wasn't wrong, but it missed some important content. I believe this new version is much better. The end of your post ...
Noah Schweber's user avatar
13 votes

Is an axiom a proof?

One can say that a proof of a statement $X$ is a finite sequence of statements where a) each statement in the sequence is either an axiom or follows from some previous staements via one of a handful ...
Hagen von Eitzen's user avatar
13 votes
Accepted

What is the reason we usually don't use formal proofs in mathematics?

tl;dr There is little reason to make paper-and-pencil formal proofs other than learning about formal logic. Machine-checked proofs take less effort to produce and are more valuable than paper-and-...
Derek Elkins left SE's user avatar
13 votes

Are there statements so self-evident that writing a proof for them is meaningless? Is this an example of one?

There's an old joke, sometimes claimed to be about Wolfgang Pauli, of a mathematician who says "It is obvious that ..." and when questioned "Is it really?" spends a large amount of ...
ConMan's user avatar
  • 26.1k
12 votes

What is the theorem that has the most proofs?

Proofs of Euler's polyhedral formula in The Geometry Junkyard: Proof 1: Interdigitating Trees Proof 2: Induction on Faces Proof 3: Induction on Vertices Proof 4: Induction on Edges Proof 5: ...
Martín-Blas Pérez Pinilla's user avatar
12 votes
Accepted

Trying to understand the difference between metatheory and theory and circularity

Most of the time in mathematics we don't study logic; we study other things like real numbers, groups or differential equations. When we're studying these things we don't often stop to worry about ...
Oscar Cunningham's user avatar
11 votes

Each person has at most 3 enemies in a group. Show that we can separate them into two groups where a person will have at most one enemy in the group.

I will give a counter-example for the case where the enemy relationship is not assumed to be symmetric (but is assumed to be irreflexive). Imagine four kingdoms called North, South, East, and West. ...
Brian Moths's user avatar
11 votes

Should a mathematical proof be 'convincing'?

Everything about a mathematical proof is psychological. Including the valid and convincing part. Who gets to decide if it is valid and if it is convincing? The primary audience for a proof is the ...
Somos's user avatar
  • 36.3k
10 votes

What is the theorem that has the most proofs?

There are also a lot of ways to prove that there are infinitely many primes. See for example: Euclid's theorem on the infinitude of primes: A hisorical survey of its proofs on arXiv, by Romeo ...
wythagoras's user avatar
  • 25.4k
10 votes

Should a mathematical proof be 'convincing'?

Mathematical proofs often, if not always, have some gap, and consequently, we have the 'convincing' part of the definition. Note that the author indicates gaps in his/her proof as he/she talks about ...
Doug Spoonwood's user avatar
10 votes
Accepted

Higher inductive type: what for?

Good question. To start with I should be clear that I think HITs are probably much more interesting to a homotopy theorist than to a computer scientist. However, it seems that they are not ...
Mike Shulman's user avatar
  • 4,854
10 votes
Accepted

Proving $\vdash \neg \neg P \to P$ (double negation elimination) in first order logic, preferrably without deduction theorem

First, here is proof that shows $\neg \neg P \vdash P$: \begin{array}{lll} 1&\neg \neg P & Premise\\ 2&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & Axiom \ 1\\ 3&\neg ...
Bram28's user avatar
  • 102k
10 votes
Accepted

Are there axioms in a natural deduction system?

Hilbert system and natural deduction can be seen as two "dual" approaches to writing formal proofs. Roughly, when it comes to deriving formulas that are valid in a specific logical system (...
Taroccoesbrocco's user avatar
9 votes
Accepted

Trouble understanding proof to $\vdash ((\neg(\phi\rightarrow \psi))\rightarrow\phi)$?

The reductio ad absurdum rule RAA (I use $\ulcorner \!\cdot\! \urcorner$ to mark discharged assumptions, with a superscript to point at the discharging rule) \begin{equation} \dfrac{\ulcorner \lnot \...
Taroccoesbrocco's user avatar
9 votes
Accepted

In Homotopy Type Theory, how do the continuous notions of spaces and paths, match the discrete notions of constructible terms and proofs?

I would say there is no mistake in your thinking. Rather, the mistake happened many decades ago when algebraic topologists gradually came to use the word "space" for a discrete object that ...
Mike Shulman's user avatar
  • 4,854
8 votes

What is the theorem that has the most proofs?

There are actually a surprisingly large number of ways to prove the Fundamental Theorem of Algebra, ranging from real analysis to complex analysis to Galois theory to Riemannian Geometry. At least one ...
Stella Biderman's user avatar
8 votes
Accepted

Why typeclasses rather than inductive types to define mathematical structures in Lean?

Formalizing mathematics in a proof assistant involves what are essentially software engineering concerns that largely don't exist in informal mathematics. Do you want to refer to ...
Derek Elkins left SE's user avatar
7 votes

prove that the $\sqrt{n}$ is unbounded

Not a valid proof. From $$-K < \sqrt{n} < K$$ one cannot conclude that $$K^2 < n < K^2$$ Example: $-3<1<3$ is true but $9<1<9$ is not true because $9<1$ is not true.
Siong Thye Goh's user avatar
7 votes
Accepted

Proving that $ax^2 + bx + c = dx^2 + ex + f$

.Since the equation: $$ (a-d)x^2 + (b-e)x+(c-f)=0 $$ is true for all values of $x$, we can substitute values of $x$ and the resulting equation will still be true: Put $x=0$, then we get $c-f=0$, so $...
Sarvesh Ravichandran Iyer's user avatar
7 votes

A simple proof of Descartes's rule of sign

This is an old question that I think deserves an answer that is at the level of a high-schooler. There are however a couple of details that, although intuitively obvious, require some basic results ...
Mittens's user avatar
  • 41.5k

Only top scored, non community-wiki answers of a minimum length are eligible