# Tag Info

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 ...
• 442k
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 ...
• 15.8k

### 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 ...
• 21.1k

### 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,328

### 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.8k
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 ...
• 11.9k

### 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,...
• 2,979

### 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 ...
• 79.6k
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 ...
• 10.4k
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 ...
• 251k

### 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 ...
• 377k
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-...
• 25.3k

### 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 ...
• 26.1k

### 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: ...
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.5k

### 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

### 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 ...
• 36.3k

### 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 ...
• 25.4k

### 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 ...
• 11.3k
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,854
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 ...
• 102k
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 (...
• 17.4k
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) \dfrac{\ulcorner \lnot \...
• 17.4k
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,854

### 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 ...
• 31.2k
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 ...
• 25.3k

### 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.
• 151k
### 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 \$...