Skip to main content
30 votes
Accepted

What set-theoretic definitions can't easily be formalized in a type theory?

Almost no pen-and-paper mathematics is written in ZFC. The vast majority of mathematical texts is actually written in something that resembles structural set theory and is closer to type theory than ...
Andrej Bauer's user avatar
  • 9,154
26 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 ...
Loïc Pujet's user avatar
  • 1,469
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 ...
Andrej Bauer's user avatar
  • 9,154
14 votes

Open source proof assistants for first order logic with equality and set theory

How about Isabelle's FOL (PDF version) and ZF? It's a serious tool, people formalized forcing with it, for example.
Andrej Bauer's user avatar
  • 9,154
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 ...
Andrej Bauer's user avatar
  • 9,154
11 votes

What set-theoretic definitions can't easily be formalized in a type theory?

Andrej's answer that "Almost no pen-and-paper mathematics is written in ZFC" is correct. But it's perhaps also worth noting that some pen-and-paper mathematics is written in ZFC (or, at ...
Mike Shulman's user avatar
  • 3,060
10 votes
Accepted

Is it possible to make a proof assistant program based on ZFC?

There are three major foundations to theorem provers. First order logic with set theory (usually something close to ZFC but maybe with inaccessible cardinals and/or better support for proper classes)....
Jason Rute's user avatar
  • 8,685
10 votes

Open source proof assistants for first order logic with equality and set theory

We have been working on a deep embedding of first-order logic in Coq for quite a while now, which could be relevant depending on what you plan to do. For instance, in a project on undecidability and ...
Dominik Kirst's user avatar
10 votes

Is there a "standard" encoding or model of material set theory in type theory?

Depends on which type theory :-) ZF set theory has been formalised in Isabelle as Isabelle/ZF by directly assuming the ZF axioms (and optionally AC). For those who prefer higher-order logic (also ...
Lawrence Paulson's user avatar
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 ...
Pierre-Marie Pédrot's user avatar
7 votes
Accepted

Kunen's inconsistency axiom-free proof on Metamath

The answer to this question is a tentative "yes", but it depends on how you interpret the resulting statement. From my understanding, there isn't anything about "elementary embedding&...
Mario Carneiro's user avatar
7 votes
Accepted

Is there a "standard" encoding or model of material set theory in type theory?

(Building on comments by Pedro Sánchez Terraf) As for encoding ZFC in dependent type theory their seems to be the following progression of work Aczel's encoding of ZFC into DTT as an inductive ...
Jason Rute's user avatar
  • 8,685
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 ...
user21820's user avatar
  • 484
5 votes

Open source proof assistants for first order logic with equality and set theory

Mizar is now open source, and the code is available at https://github.com/MizarProject/system under a GPLv3 license. Further, there is also an ongoing project to reimplement Mizar in Rust.
Jason Rute's user avatar
  • 8,685
5 votes

Open source proof assistants for first order logic with equality and set theory

You may want to look at LISA https://github.com/epfl-lara/lisa It is a new proof assistant based on First Order Logic with schematic symbols, equality and set theory. Its kernel is based on a proof ...
Simon Guilloud's user avatar
5 votes
Accepted

Cardinality of Type in a given universe

Equality is not provable. Indeed, it is consistent that univ.{u u+1} < #(Type u) at every level u. Recall that the universe ...
François G. Dorais's user avatar
5 votes
Accepted

How to show in type theory (like in a proof assistant) that finite sets of different cardinalities are not isomorphic?

This is called the Pigeonhole Principle. In a weak form it says that there is no injection from Fin (n+1) to Fin n. In a ...
François G. Dorais's user avatar
5 votes
Accepted

What is the meta-language of ZFC?

Does this mean that the axioms of ZFC are just expressions obtainable from the grammar of first order logic? As SEP tells us, ZFC is an axiom system formulated in first-order logic with equality and ...
Alex Chichigin's user avatar
4 votes

What is the meta-language of ZFC?

First, in a standard logic textbook (or at least a standard set theory textbook), yes, ZFC as a foundation takes place in first order logic (FOL). Each axiom of ZFC is written in the language of FOL. ...
Jason Rute's user avatar
  • 8,685
4 votes

Is it possible to make a proof assistant program based on ZFC?

You could just add the ZFC axioms to Coq. I've done quite a bit of work in this system. ...
djao's user avatar
  • 434
4 votes

Is there a multiway system which is equivalent to taking ZFC as axioms?

Wolfram's multi-way systems are expressive enough to accommodate generation of any computably enumerable set. Thus they are powerful enough to generate all theorems of a computably enumerable formal ...
Andrej Bauer's user avatar
  • 9,154
3 votes

How to show in type theory (like in a proof assistant) that finite sets of different cardinalities are not isomorphic?

This is essentially the pigeonhole principle. If $m < n$, then $f : \mathsf{Fin}\ n → \mathsf{Fin}\ m$ takes two distinct values to the same value, meaning it cannot be an equivalence. This can ...
Dan Doel's user avatar
  • 982
3 votes
Accepted

Negating universal/existential quantifier in type theory, propositions on elements of the empty type

The universal/existential quantifiers and their negations In type theory, negation is defined as a shortcut for "implying falsity", in other words ~ P is *...
Meven Lennon-Bertrand's user avatar
2 votes
Accepted

How do I prove that an element is a within a set in Lean?

rfl should do the trick: inductive Test : Type | T1 | T2 example : Test.T1 ∈ { t: Test | t = Test.T1 } := rfl
Mario Carneiro's user avatar
1 vote

Is there a multiway system which is equivalent to taking ZFC as axioms?

For a long time I have been interested in the idea of computationally enumerating every possible expression of a formal theory. Who hasn't! :) As one with a background in linguistics, I am sure you ...
Julio Di Egidio - inactive's user avatar
1 vote

Do you need a Hilbert style Epsilon operator for definitions in set theory?

As Andrej mentioned you can define a little meta-language which compiles to first order logic. I've been experimenting with this approach and it's simpler and better than you might expect but just not ...
Ms. Molly Stewart-Gallus's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible