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

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

### 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 ...
• 38.7k
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 ...
• 431k
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 ...
• 59.1k

• 59.1k
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 ...
• 17.2k

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

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

• 34.8k

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

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