# Tag Info

Accepted

### What is predicativity?

Impredicativity is one of those soft concepts that appears in many related forms, but it is difficult to explain what precisely they share. Let me try anyhow. Impredicativity allows us to single out, ...
• 10.1k
Accepted

### What are the bases for different Proof Assistants?

There are a lot of bases, theories and techniques in proof assistants. Let me show you how deep the rabbit hole is (in suggested order of implementation): (Fibrational) Dependent Type Theories CoC (...
• 1,297

### Proof-theoretic comparison table?

Here are a few comparisons of dependent type theories with fragments of Peano arithmetic and set theories that I know of: Predicative systems (the MLTT family) Predicative systems are comparable with ...
• 1,489

### What are the bases for different Proof Assistants?

Here are some other points in the space: NuPrl has dependent types but is pretty different from, e.g., Coq; as I understand it, it's based on a model of untyped computation and proofs of well-...
• 1,547
Accepted

### Tools for checking the consistency of a type theory

One can think of type theory as an algebraic theory on steroids (there is technical merit to this claim). Every algebraic theory has a model, namely the trivial one whose carrier is the singleton. A ...
• 10.1k
Accepted

### Do you need a Hilbert style Epsilon operator for definitions in set theory?

The type theories implemented in proof assistants have definitions which allow introduction of new symbols. Traditional first-order logic avoids definitions by using instead a meta-theorem stating ...
• 10.1k
Accepted

### What is the role of impredicativity in program extraction?

I have occasionally thought about this question. My inconclusive conclusion is that impredicativity hinders program extraction. Let me try to give an argument in the context of realizability. I am ...
• 10.1k

### What are the bases for different Proof Assistants?

ACL2 is based on the logic of Common Lisp. This means several things: The universe (over which one quantifies and defines predicates) consists of the s-expressions. Logically, it is equivalent to ...
• 2,320

### Can the development of proof assistants make mathematicians switch their framework?

The following is a made up opinion piece based on the observation of a statistically small sample of mathematicians. Please take it with a grain of salt. A typical working mathematician has little ...
• 10.1k
Accepted

### What is the computational complexity of theorem proving?

Briefly: Propositional logic: determining whether there is a proof is $\mathsf{NP}$-hard, since proving a formula entails determining that its negation is not satisfiable. First-order logic: ...

• 2,353