187
votes
Accepted
How do we prove that something is unprovable?
When we say that a statement is 'unprovable', we mean that it is unprovable from the axioms of a particular theory.
Here's a nice concrete example. Euclid's Elements, the prototypical example of ...
- 24.5k
78
votes
Are proofs by contradiction really logical?
Proof by contradiction, as you stated, is the rule$\def\imp{\Rightarrow}$ "$\neg A \imp \bot \vdash A$" for any statement $A$, which in English is "If you can derive the statement that $\neg A$ ...
- 56k
74
votes
How do we prove that something is unprovable?
First of all in the following answer I allowed myself (contrary to my general nature) to focus my efforts on simplicity, rather than formal correctness.
In general, I think that the way we teach the ...
- 16.5k
69
votes
Under the Curry-Howard correspondence or loosely "proofs-as-programs", do we also have "programs-as-proofs" and what would some arb. program prove?
Yes. But usually the associated proofs are uninteresting.
Remember that, under the correspondence, we have
Types $\longleftrightarrow$ Propositions
Programs $\longleftrightarrow$ Proofs
So let's ...
- 35.6k
52
votes
Accepted
Can proof by contradiction 'fail'?
The situation you ask about, where $P$ is inconsistent with our axioms and $\neg P$ is also inconsistent with our axioms, would mean that the axioms themselves are inconsistent. Specifically, the ...
- 70.3k
49
votes
Accepted
Computability viewpoint of Godel/Rosser's incompleteness theorem
Here I shall present very simple computability-based proofs of Godel/Rosser's incompleteness theorem, which require only basic knowledge about programs. I feel that these proofs are little known ...
- 56k
47
votes
Do nonconstructive proofs of isomorphism exist?
The simplest example I know: the existence of primitive roots tells us that if $p$ is a prime then the group $(\mathbb{Z}/p\mathbb{Z})^{\times}$ of units $\bmod p$ is cyclic, hence isomorphic to $C_{p-...
- 409k
46
votes
Accepted
What is exactly the difference between a definition and an axiom?
Axioms are not "defined to be true"; I'm not even sure what that would mean. What they are is evaluated as true. Practically speaking all this means is that in the mathematical context at hand, you're ...
- 9,565
44
votes
Accepted
Is a proof also "evidence"?
Hypothesis: $n^2-n+41$ is prime, for all natural $n$.
Evidence: True for $n=1, 2, 3,\ldots, 40$.
That seems persuasive, but for $n=41$ the hypothesis is false.
In general, science typically uses ...
- 82.3k
38
votes
Can proof by contradiction 'fail'?
It is possible for both $P$ and $ \neg P $ to be consistent with a set of axioms. If this is the case, then $P$ is called independent. There are a few things known to be independent, such as the ...
- 4,568
36
votes
Accepted
Why can't you prove the law of the excluded middle in intuitionistic logic (for layman)?
If you could prove the law of the excluded middle, then it would be true in all systems satisfying intuitionistic axioms. So we just need to find some model of intuitionistic logic for which the law ...
- 30k
35
votes
Accepted
Proving the existence of a proof without actually giving a proof
There are various ways to interpret the question. One interesting class of examples consists of "speed up" theorems. These generally involve two formal systems, $T_1$ and $T_2$, and family of ...
- 80.6k
35
votes
Accepted
Are there are any inherent mathematical reasons difficult proofs exist?
Although this question may superficially look opinion-based, in actual fact there is an objective answer. The core reason is that the halting problem cannot be solved computably, and statements about ...
- 56k
32
votes
Accepted
How can we know we're not accidentally talking about non-standard integers?
[I will take for granted in this answer that the standard integers "exist" in some Platonic sense, since otherwise it's not clear to me that your question is even meaningful.]
You're thinking about ...
- 323k
30
votes
Accepted
Why does proof by elimination work?
To reword my comment, consider this.
There are five cats in a room, and you know that exactly one of them is black. If you show that four of them are not black, then you can reasonably conclude that ...
- 2,648
29
votes
What is exactly the difference between a definition and an axiom?
A definition is a conservative extension of the language by a new symbol and some axioms involving this symbol. The key word here is conservative; in general axioms strengthen the system in question, ...
- 27.1k
29
votes
Why does proof by elimination work?
See Disjunctive syllogism :
\begin{align}
\frac{P \lor Q \ \ \ \lnot P}{Q}
\end{align}
which amounts to the following principle :
if we know that the ball is either black or white and we know ...
- 92.3k
28
votes
Is a proof also "evidence"?
In mathematics, "evidence" is weaker than "proof".
Mathematicians use the words "proof" and "evidence" differently from the sciences. When we speak of a "proof" that something is true, we mean an ...
- 28.7k
27
votes
How do we prove that something is unprovable?
Your question is partially based on an error of terminology. We don't speak of unprovable theorems - as you say, being a theorem implies having a proof. The correct thing to speak of is unprovable ...
- 279
23
votes
Accepted
Can every true theorem that has a proof be proven by contradiction?
In classical logic, the answer is yes. Take any theorem $T$ and any proof $P$ for $T$. Now write the following proof:
If $\neg T$:
[Write $P$ here.]
Thus $T$.
Thus a contradiction.
Therefore $\...
- 56k
22
votes
Do nonconstructive proofs of isomorphism exist?
We know that any two finite fields with the same cardinality are isomorphic. On the other hand, suppose you have two different polynomials $f, g \in \mathbb{F}_q[x]$ which are irreducible and have ...
- 19.6k
21
votes
Accepted
Under the Curry-Howard correspondence or loosely "proofs-as-programs", do we also have "programs-as-proofs" and what would some arb. program prove?
The Curry-Howard correspondence can be seen both as "proofs-as-programs" and "programs-as-proofs", provided that we specify what the logic for proofs and the language for programs ...
- 16.3k
19
votes
Proving the existence of a proof without actually giving a proof
Henkin's completeness proof is an example of what you seek: It demonstrates that for a certain statement there is a proof, but does not establish what that proof is.
- 33.3k
19
votes
Accepted
Infinitely long proofs
It's actually vastly easier to view proofs as trees in this context, so I'll do that.
Generally, an "infinitely long proof" is more accurately a well-founded infinitely-branching tree (or something ...
- 237k
18
votes
Accepted
Presburger arithmetic
Presburger arithmetic is clearly consistent - it has a model (namely, $\mathbb{N}$, or more precisely $(\mathbb{N}; +)$). So there's not much to say there.
Meanwhile, it is a recursively axiomatizable ...
- 237k
18
votes
Do nonconstructive proofs of isomorphism exist?
If a purely set theoretic example is acceptable:
The Cantor-Schröder-Bernstein theorem says that a bijection between two sets $A$ and $B$ exists when there are injections $i : A \rightarrow B$ and $j :...
- 297
Only top scored, non community-wiki answers of a minimum length are eligible