38
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, ...
- 11k
29
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 ...
- 1,499
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 (...
- 1,307
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-...
- 1,607
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 ...
- 11k
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 ...
- 11k
15
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 ...
- 11k
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 ...
- 2,330
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 ...
- 11k
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: ...
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:...
- 4,344
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 ...
- 2,330
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 ...
- 1,142
9
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, ...
- 6,008
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 ...
- 2,393
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 ...
- 11k
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 ...
- 3,571
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 ...
- 2,393
8
votes
Why is $\Bbb Z = \Bbb N$ independent of Lean?
It suffices to give two models of Lean's type theory, one in which $\mathbb{Z} = \mathbb{N}$ and another in which $\mathbb{Z} \ne \mathbb{N}$.
We shall use the interpretation of Lean type theory in ...
- 11k
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 ...
- 6,008
7
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 ...
- 2,083
6
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 ...
- 1,033
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 &...
- 6,008
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 ...
- 2,083
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 ...
- 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 ...
- 1,749
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 ...
- 10.3k
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&...
- 1,749
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 ...
- 2,393
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 ...
- 11k
Only top scored, non community-wiki answers of a minimum length are eligible