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
8
votes
2
answers
221
views
What is the computational complexity of theorem proving?
I heard theorem proving is a hard problem, hard enough that it contributed to an early AI winter. But how hard?
While reading about proof assistants, I have come to realize that there are many types ...
- 2,220
8
votes
1
answer
208
views
Feferman's universes for proof assistants?
I asked this question on MathOverflow a few months ago, but received no answers.
There are some mathematicians who are comfortable with ZFC but uneasy with large cardinals. For them, it may be ...
- 505
7
votes
3
answers
201
views
Why is $\Bbb Z = \Bbb N$ independent of Lean?
In this answer, it is noted
For a silly example, in ZFC with the usual encoding, $\mathbb{Z} \neq \mathbb{N}$, but in Lean it is well-known that this is independent. Of course in both ZFC or Lean, ...
- 173
6
votes
2
answers
316
views
Lean and inaccessible cardinals
It seems well known that Lean's type theory is equiconsistent with ZFC + the existence of $n$ inaccessible cardinals for every $n>0$.
Suppose I want to ensure that my lean proofs depend only on ZFC,...
- 161
5
votes
0
answers
231
views
Proof-theoretic strength of HOL compared to predicative dependent types
By HOL I mean something like inference rules of HOL Light with the 3 axioms of infinity, extensionality and choice ($\varepsilon$ operator).
By predicative dependent types, I am thinking of MLTT + W-...
- 547
4
votes
2
answers
195
views
Can a proof engine be built based on graphs?
One of the more common ways to do proofs is using a deductive system.
Can proofs instead be done using graphs?
I am seeking papers that outline from the ground up how such a system works. If example ...
- 2,846
3
votes
0
answers
129
views
Uniform notions of pattern matching at dependent types with impredicative proof strength
I am looking for axioms/inference rules that satisfy the following 3 conditions:
can be added to predicative intensional Martin-Löf type theory, so $\Pi$, $\Sigma$, equality type, with W-types, ...
- 547
1
vote
2
answers
173
views
Does quantification over functions (STLC) increase strength beyond first order logic?
Does quantification over functions (STLC) increase strength beyond first order logic?
I want to add support for binders in my little constructive first order logic formalism I'm working on but I'm ...
- 2,868
0
votes
2
answers
175
views
Does a proof assistant have to be interactive?
I have thought of systems like Coq & Isabelle as programming languages specialised for writing proofs.
A programming language might or might not have a REPL making it interactive but the REPL is ...
- 151
0
votes
0
answers
119
views
MLTT with first-order reasoning and equality-reasoning information preservation
Terms in Extensional MLTT don't contain equality-reasoning information (implicit transports), effectively meaning data is lost, which is bad. But at the same time, higher-order reasoning (reasoning ...
- 345