37 votes
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, ...
Andrej Bauer's user avatar
  • 8,969
29 votes
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 (...
Namdak Tönpa's user avatar
27 votes

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-...
Jason Gross's user avatar
  • 1,457
26 votes

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 ...
Loïc's user avatar
  • 1,459
18 votes
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 ...
Andrej Bauer's user avatar
  • 8,969
18 votes
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 ...
Andrej Bauer's user avatar
  • 8,969
14 votes
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 ...
Andrej Bauer's user avatar
  • 8,969
13 votes

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 ...
Couchy's user avatar
  • 2,211
12 votes

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 ...
Andrej Bauer's user avatar
  • 8,969
10 votes
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: ...
Bjørn Kjos-Hanssen's user avatar
10 votes

What is predicativity?

System F allows for function types like $T=\Pi X. X \to X$, where $X$ ranges through all the types. In particular, $T$ is one of them! This means that the usual set-theoretic interpretation of $\Pi (a:...
Trebor's user avatar
  • 3,867
10 votes

What is predicativity?

As I understand it, impredicativity in type theory is unrelated (at least in a formal way) from impredicativity in set theory. The single rule in a type system which makes it impredicative is the ...
Couchy's user avatar
  • 2,211
10 votes
Accepted

Construction of inductive types "the hard way"

In the HOLish settings, these types (starting with the natural numbers) are indeed constructed from first principles; they're certainly not axiomatised. Harrison had an early (1995) paper on how to ...
Michael Norrish's user avatar
9 votes

Can a proof engine be built based on graphs?

Your question is quite vague, but can be answered positively when taken literally. Indeed, most implementations of a deductive system are actually already using graphs internally. When phrased ...
Pierre-Marie Pédrot's user avatar
9 votes
Accepted

Attempts to accommodate theories of different consistency strength in single assistant

You could address your goals by using a generic proof assistant, one that supports user-definable theories, such as Isabelle and Metamath, and I am sure there are others. These allow you to define ...
Andrej Bauer's user avatar
  • 8,969
8 votes

Integration of proof assistants and Wikipedia-like websites?

Metamath has a Proof Explorer; here is one entry. This is mostly a visualization of the proof database set.mm. Because of the nature of the Metamath proof assistant, any new theorems or derived ...
Greg Nisbet's user avatar
  • 2,741
8 votes

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

I am not asking that much! If there is one thing I would like mathematician to get from the use of dependent type theory, this is the revolutionary notion of bound variables. For some mysterious ...
Pierre-Marie Pédrot's user avatar
7 votes
Accepted

What is the trade-off to accepting impredicative propositions?

I think this is mainly not a question about usability, but rather a form of discomfort so as to the foundational status of theories incorporating impredicativity. Indeed, as you mentioned, ...
Meven Lennon-Bertrand's user avatar
7 votes

What is the computational complexity of theorem proving?

As an addition: proof checking (rather than search) already can be very hard. For instance, proof checking in type theory relies on conversion checking, which itself needs to evaluate arbitrary ...
Meven Lennon-Bertrand's user avatar
6 votes

Are Logics Based on Dependent Types Stronger Than Ones Without?

Pretty much always, it means "this gadget is more annoying to formalise in HOL", not "this gadget is not possible to formalise in HOL." A simple example of this is formalising ...
Neel Krishnaswami's user avatar
6 votes

Construction of inductive types "the hard way"

There are a lot of questions in your question, so I don’t think it’s easy to answer all of them at once, but let me still try and give a picture in the dependently typed setting. First you cannot get &...
Meven Lennon-Bertrand's user avatar
6 votes

What is the trade-off to accepting impredicative propositions?

There's a general principle to keep in mind: Weaker theories have more models Martin Escardo, Paul Taylor or Andrej Bauer will probably be able to supply some cool geometric examples of this, but ...
Neel Krishnaswami's user avatar
5 votes

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

If you're mainly interested in set theories based on FOL, then you don't need to know concrete details of what existing systems do, but rather you only need to know and understand the precise ...
user21820's user avatar
  • 484
5 votes
Accepted

Can a proof engine be built based on graphs?

Well, a proof engine is built atop a proof calculus, right? And natural deduction basically amounts to using a specific set of possible labeled edges in graphs for proofs (namely, introduction and ...
Alex Nelson's user avatar
  • 1,564
4 votes
Accepted

Generating valid statements without a proof goal

This definitely falls under various active research projects to find interesting mathematics from a set of theorems. I can't point to a particular project per say, but let me mention why this is so ...
Jason Rute's user avatar
  • 8,520
4 votes
Accepted

Are Logics Based on Dependent Types Stronger Than Ones Without?

For completeness I'm adding the specific example that the OP is asking for, turning my comment above and Jason Rute's into an answer. One thing that make type theories occurring in most PAs strictly ...
Pedro Sánchez Terraf's user avatar
4 votes

Generic proof assistants/modularity of the proof assistants?

It sounds like you're after a logical framework, i.e., a system which allows you to reason within a given foundations. Isabelle is a bit more than this, it's a so-called "meta-logical framework&...
Alex Nelson's user avatar
  • 1,564
4 votes
Accepted

Does quantification over functions (STLC) increase strength beyond first order logic?

The answer depends on the logic considered. Goodman's theorem states that $\mathsf{HA}^\omega+\mathsf{AC}+\mathsf{DC}$ is conservative over $\mathsf{HA}$. In particular, adding higher-order functions ...
Pierre-Marie Pédrot's user avatar
4 votes
Accepted

Feferman's universes for proof assistants?

The concrete suggestion you make, namely to use ZFC/S, is quite difficult to appraise. The only way to answer it is to actually try formalizing mathematics in it. One possibility is for you (or your ...
Andrej Bauer's user avatar
  • 8,969
4 votes

Lean and inaccessible cardinals

Your question probably needs some clarification. Which theorems make sense in both ZFC and Lean It isn't 100% non-ambiguous what it means for a Lean theorem to "hold in ZFC". Sometimes it ...
Jason Rute's user avatar
  • 8,520

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