# Tag Info

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

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

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

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

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

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