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
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
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
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
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
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
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
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