60
votes
Accepted
When writing proofs, is logical notation a crutch?
It's perfectly normal. In fact, I think that's how a mathematitian's mind grows.
First, you are naive and "intuistic", and you do a lot of "well, of course this is so!" like statements that are not ...
- 122k
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 ...
- 20.7k
23
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$, ...
- 4,298
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.
- 16.5k
14
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 ...
- 76.7k
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 ...
- 239k
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 ...
- 372k
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-...
- 24.7k
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: ...
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. ...
- 573
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 ...
- 34.2k
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 ...
- 24.9k
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 ...
- 11k
10
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 ...
- 16.1k
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 ...
- 98k
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 ...
- 30.9k
8
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 ...
- 4,784
8
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 ...
- 4,784
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 ...
- 36.2k
7
votes
Direct Proof for sum of $n$ integers equation?
Do what Gauss did, reverse the sequence and add it with the original. Now each term is 2n + 4, and there are n such terms. The sum is n(2n+4). Since this results from two sequences, divide by 2 and ...
- 2,623
7
votes
natural deduction: introduction of universal quantifier and elimination of existential quantifier explained
Example
Let $\Gamma$ the set of first-order Peano axioms: no variables free.
1) $\Gamma \vdash \exists x (x = 0)$ --- easily provable
2) $\Gamma, x=0 \vdash x=0$ --- obvious
3) $\Gamma \vdash x=0$ ...
- 93k
7
votes
Calculus of Natural Deduction That Works for Empty Structures
The easiest (and in my opinion cleanest) way to do this is to augment the context. In the sequent calculus you presented, you have the left-hand of the sequent being a set $Γ$ of formulae. Instead of ...
- 56.6k
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 $...
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.
- 148k
7
votes
What is the theorem that has the most proofs?
It must be Pythagoras's theorem. There's hundreds of proofs (famously, a whole book of them). Cut-the-Knot has a few of them...
- 67.1k
7
votes
Is this proof correct? (natural deduction)
You were right to doubt your proof; it's not quite right.
The main mistake is that you are effectively closing two subproofs at once once you go from 2.2.3 to 3, but you can only close one subproof ...
- 98k
7
votes
Accepted
Nested induction
The argument for double induction/nested induction is:
$$\begin{array}{|l}\text{In the domain of }\Bbb N^+\\\hdashline 1\quad P(1,1)\\2\quad \forall m\geq 1:P(m,1)\to P(m+1,1)\\3\quad \forall m\geq 1,...
- 128k
7
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 ...
- 24.7k
7
votes
Accepted
How to prove $((A \to B) \to A) \to A$ using Lukasiewicz's axioms, MP and deduction theorem?
The statement is known as Peirce's Law, and the proof is pretty nasty. I can believe someone can spend $10$ years on it without cracking it!
The proof uses some helpful Lemma's.
First, let's prove: $...
- 98k
Only top scored, non community-wiki answers of a minimum length are eligible