Skip to main content

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.

Filter by
Sorted by
Tagged with
6 votes
2 answers
271 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,...
Potato's user avatar
  • 161
0 votes
0 answers
118 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 ...
Russoul's user avatar
  • 345
8 votes
1 answer
203 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 ...
Timothy Chow's user avatar
0 votes
2 answers
171 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 ...
Bruce Adams's user avatar
3 votes
0 answers
126 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, ...
Ilk's user avatar
  • 547
5 votes
0 answers
225 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-...
Ilk's user avatar
  • 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 ...
Ms. Molly Stewart-Gallus's user avatar
9 votes
2 answers
810 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 ...
Ms. Molly Stewart-Gallus's user avatar
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. \...
Ms. Molly Stewart-Gallus's user avatar
13 votes
0 answers
366 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-...
user21820's user avatar
  • 484
11 votes
1 answer
608 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 ...
Couchy's user avatar
  • 2,221
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 ...
user21820's user avatar
  • 484
9 votes
1 answer
177 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 ...
Reubend's user avatar
  • 519
18 votes
2 answers
544 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 ...
James Martin's user avatar
  • 1,025
4 votes
2 answers
191 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 ...
Guy Coder's user avatar
  • 2,846
15 votes
2 answers
360 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 ...
Wno-all's user avatar
  • 1,108
14 votes
2 answers
308 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 ...
Greg Nisbet's user avatar
  • 2,761
8 votes
2 answers
216 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 ...
tinlyx's user avatar
  • 2,034
13 votes
1 answer
181 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 ...
user9716869 - supports Ukraine's user avatar
8 votes
2 answers
256 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/...
ACL's user avatar
  • 233
13 votes
1 answer
163 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 ...
Pedro Sánchez Terraf's user avatar
9 votes
3 answers
204 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. ...
user9716869 - supports Ukraine's user avatar
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'...
Greg Nisbet's user avatar
  • 2,761
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 ...
Guy Coder's user avatar
  • 2,846