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 ...
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 ...
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 ...
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$, ...
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
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 ...
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,...
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 ...
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 ...
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 ...
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 ...
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-...
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 ...
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: ...
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 ...
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. ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 (...
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 \...
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 ...
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 ...
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 ...
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.
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
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 ...
Only top scored, non community-wiki answers of a minimum length are eligible
Related Tags
formal-proofs × 855logic × 460
first-order-logic × 219
propositional-calculus × 199
natural-deduction × 166
proof-writing × 63
proof-theory × 62
discrete-mathematics × 60
solution-verification × 40
formal-systems × 33
soft-question × 27
real-analysis × 26
induction × 26
quantifiers × 25
sequent-calculus × 23
set-theory × 21
hilbert-calculus × 21
calculus × 20
formal-languages × 20
sequences-and-series × 17
axioms × 17
linear-algebra × 16
elementary-set-theory × 16
proof-explanation × 16
peano-axioms × 16