Questions tagged [foundations]
Use this tag for questions about mathematical or logical foundations of proof assistants. Questions should be related in some way to proof assistants. Possible topics might include mathematical modelling, consistency and computability, universes, etc.
25
questions
38
votes
3
answers
1k
views
What is predicativity?
Type systems, and the proof assistants based on them, are frequently divided into predicative and impredicative.
What exactly does this mean? I've heard the slogan "impredicativity means you can'...
- 3,095
32
votes
3
answers
1k
views
What are the bases for different Proof Assistants?
From the Wikipedia article on Proof Assistant it shows some Proof Assistants are based on Higher Order Logic, (HOL Light) and some are based on Dependent Types, (Coq).
Are there any other means upon ...
- 2,846
21
votes
1
answer
1k
views
Proof-theoretic comparison table?
I read this CSTheory SE post, which suggests that it is often not clear what variant of MLTT or CIC is being referred to. But I would like to know the proof-theoretic strengths of the various ...
- 484
18
votes
2
answers
573
views
What is the trade-off to accepting impredicative propositions?
Impredicativity greatly increases the logical strength of a formal system, and impredicative propositions are also a consequence of various axioms including LEM and Zorn's Lemma. An impredicative sort ...
- 1,035
16
votes
3
answers
1k
views
Do you need a Hilbert style Epsilon operator for definitions in set theory?
I've started to play with mechanizing some set theory stuff. I'm not sure if I want a constructive flavor or not yet.
Anyhow you can do stuff like axiomize the empty set
$$ \top \vdash \exists P. \...
- 2,868
15
votes
2
answers
380
views
Are Logics Based on Dependent Types Stronger Than Ones Without?
There have been several times during I came across statements like Isabelle/HOL's logic is not rich enough to formalize X on various places online and in during personal discussions. Or similar ...
- 1,128
14
votes
2
answers
332
views
Tools for checking the consistency of a type theory
My question is twofold:
How do you define consistency (analogously to the concept in first-order logic) in the context of a type theory?
Are there any tools that can check consistency?
I have seen a ...
- 3,095
13
votes
1
answer
169
views
Attempts to accommodate theories of different consistency strength in single assistant
TL;DR: How / where to formalize results concerning the logical strength of systems? Are proof assistants having a weak base theory but also enough infrastructure to make it feasible?
I'll start by ...
- 1,013
13
votes
1
answer
185
views
Integration of proof assistants and Wikipedia-like websites?
I noticed that some of the Wikipedia.org entries that describe proofs of theorems also contain links to proofs of these theorems formalized in the Mizar proof assistant (example). There was one ...
13
votes
0
answers
369
views
Unintentionally proven false theorem with type-in-type outside logic and foundations?
We are all familiar with Russell's paradox, and it is known that Per Martin-Löf proved that type-in-type is normalizing and consistent (which is false), by accidentally using an assumption in his meta-...
- 484
11
votes
1
answer
614
views
What is the role of impredicativity in program extraction?
Is impredicativity useful for program extraction in Coq? For example is there some kind of realizability argument that depends on impredicativity?
Of course it doesn't seem to be necessary for program ...
- 2,290
9
votes
2
answers
822
views
Construction of inductive types "the hard way"
Most theorem provers simply axiomize inductive types (or equivalently W types) in the abstract which is fine.
But I'm curious about explicit constructions of inductive types within the theory.
I ...
- 2,868
9
votes
3
answers
208
views
Generic proof assistants/modularity of the proof assistants?
One notable feature of Isabelle is that it allows for the definition and in-built integrated support of alternative object logics via the interface of Isabelle/Pure in combination with Isabelle/Isar. ...
9
votes
1
answer
181
views
Generating valid statements without a proof goal
Given some initial list of assumptions, I'd like to generate some true statements which follow from them without seeking a specific proof goal. I only need a small number of consequences from those ...
- 519
8
votes
2
answers
264
views
Can the development of proof assistants make mathematicians switch their framework?
The Stack Exchange bot reminded me that I had committed myself to asking some questions, but please allow a possibly naive question, possibly of a philosophical nature rather than mathematical/...
- 233