Skip to main content
191 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 ...
John Gowers's user avatar
  • 25.1k
75 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 ...
Stefan Mesken's user avatar
71 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 ...
Chris Grossack's user avatar
63 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
54 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 ...
user21820's user avatar
  • 59.1k
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-...
Qiaochu Yuan's user avatar
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 ...
vadim123's user avatar
  • 83k
35 votes

What exactly is circular reasoning?

Of course my proof contains its thesis within its assumptions. Each and every proof must be based on axioms, which are assumptions that are not to be proved. Hold it right there, Alice. These ...
fleablood's user avatar
  • 125k
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 ...
user21820's user avatar
  • 59.1k
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 ...
Eric Wofsey's user avatar
29 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 ...
Bilbottom's user avatar
  • 2,658
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 ...
Mauro ALLEGRANZA's user avatar
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 ...
Bill Cook's user avatar
  • 29.6k
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 ...
PMar's user avatar
  • 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 $\...
user21820's user avatar
  • 59.1k
23 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 ...
Taroccoesbrocco's user avatar
23 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 ...
Daniel Schepler's user avatar
19 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 ...
Noah Schweber's user avatar
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 ...
Noah Schweber's user avatar
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 :...
David's user avatar
  • 297
18 votes
Accepted

Proving there is only one proof?

This depends strongly on both the proof system you're using and the theorem you're trying to prove. For this answer we'll work in a particularly simple proof system: Gentzen style natural deduction ...
Chris Grossack's user avatar
17 votes

Are there are any inherent mathematical reasons difficult proofs exist?

You received already good answers, but I want to add a point that has not been covered: combinatorics. True, you may start with few simple assumptions and operations, but how many ordered ways are ...
Rexcirus's user avatar
  • 445
17 votes
Accepted

A seemingly contradictory function - where's the issue?

Your claimed proof that $f$ always halts and returns $0$ or $1$ relies on the assumption that if there is a PA-proof that a Turing machine halts for all inputs, then it actually halts for all inputs. ...
Arno's user avatar
  • 4,191
16 votes
Accepted

Is it a paradox if I prove something as unprovable?

Unprovable ≠ Undecidable. If PA can prove neither the conjecture nor its negation, it is undecidable in PA. If you ever prove such a result, you certainly cannot be working within PA, because PA ...
user21820's user avatar
  • 59.1k
16 votes
Accepted

Has a conjecture ever originally been decided by constructing the proof with mathematical logic?

I do not know about a conjecture, but I would like to mention the Ax–Grothendieck_theorem. A very nice way of proof is to show that the (first-order) theory $ACF_0$ of algebraically closed fields ...
Aphelli's user avatar
  • 34.8k
16 votes

What theory of logic or types considers the "category of propositions"?

There is a "small" way to do this and a "big" way to do this that I'm aware of. The "small" way is to axiomatize what properties you'd want a category of propositions to ...
Qiaochu Yuan's user avatar
16 votes

What is the point of model theory?

Model theory is an excellent tool for talking about the semantics of formal languages, particularly first order logic with equality and with constants, functions and non-logical predicates, by ...
Greg Nisbet's user avatar
  • 11.9k
15 votes
Accepted

What is the role of associative and commutative properties in Mathematics and what if someone want to prove them??

It has since been clarified in the comments that the OP is specifically interested in proving the relevant properties for addition and multiplication. Let me show how to prove that addition is ...
Noah Schweber's user avatar

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