Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.
Sign up to join this community
I heard that many proof assistant programs are made based on the type theory.
For me, as a mathematician, when I met Coq at first, it is difficult to accustomed with it.
So I have a question.
Is it possible to make a proof assistant program based on ZFC?
Or Can we make a setting on Coq so that we can do set theoretical approach on Coq?
If it is possible, then I think that many undergraduate mathematicians can use it easily and get many benefits from it.
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). Higher order logic (a form of type theory). Dependent type theory. Mizar, Metamath (set.mm), Isabelle/ZFC all use the first. HOL-light, HOL4, and Isabelle/HOL use HOL. Coq, Lean, and Agda use DTT.
So this answers your first question. Yes, it is possible to base a theorem prover on something like ZFC. Also see Open source proof assistants for first order logic with equality and set theory.
As for taking a set theoretical approach in one of the later theorem provers, I am not sure I see the point. But nonetheless, let me explain how I see the connections. Pure HOL is the theory of a topos, so instead of the theory having set based models, it has topos based models. But once one adds in the axiom of choice (which all HOL based provers do), then you can think of all the types as sets. The rules of HOL plus the axiom of choice and the axiom of infinity are basically just another fairly natural way to describe set theory. It may be a bit more like the category Set in category theory more than the models of ZFC in set theory, but still a form of set theory nonetheless. (If I remember correctly, I think one also needs replacement to get equivalence with ZFC.) In HOL (plus the various axioms), it is easy to write many theorems of set theory.
As for dependent type theory, again the base logic is more categorical (maybe describing various types of infinity categories or infinity topoi if I remember correctly). It also works well as a syntax for a programming language and it has a nice computational interpretation. Again if you add in the axiom of choice (as is common in Lean), your types behave like sets and you can think of it as a different form of set theory. Mario Carniero’s master’s thesis for example shows that Lean’s logic is equi-consistent with ZFC plus countably many inaccessible cardinals. It is certainly possible to do (meta) set theory in DTT like proving the independence the continuum hypothesis in ZFC. (Also see https://proofassistants.stackexchange.com/a/1533/122.)
Also, if you are interested in the meta theoretic aspects of these three logics, see Jeremy Avigad’s article on the Foundations of proof assistants.
Edit: as for making it more accessible to mathematicians, I would argue that mathematicians rarely think about foundations (with the exceptions of some with more of a logical bent). The biggest practical aspects are (1) usability of the systems and (2) being able to describe the mathematical objects and reasoning that one wants. As for (1), that doesn’t have much to do with foundations. As for (2), I think a lot of mathematicians who got into proof assistants actually find type theory, especially dependent type theory, to be a very natural way to encode the mathematical objects they work with. The biggest sticking point with foundations is the need for the axiom of choice. In Coq it is common to avoid it if possible, but many mathematicians, in say Lean, use it freely. That way one doesn’t have to worry about constructive math, which while interesting and important, is very foreign to the working mathematician.
You could just add the ZFC axioms to Coq. I've done quite a bit of work in this system.
From Coq Require Import Utf8 ClassicalEpsilon ssreflect ssrbool ssrfun.
Parameter set : Type.
Parameter IN: set → set → Prop.
Infix "∈" := IN (at level 75).
Notation "a ∉ b" := (¬ a ∈ b) (at level 75).
(* Axiom list from https://math.stackexchange.com/questions/916072/ *)
Axiom Extensionality : ∀ x y, (∀ z, z ∈ x ↔ z ∈ y) → x = y.
Axiom Regularity : ∀ x, (∃ a, a ∈ x) → ∃ y, y ∈ x ∧ ¬ ∃ z, (z ∈ y ∧ z ∈ x).
Axiom Replacement : ∀ A R, (∀ x, x ∈ A → exists ! y, R x y) →
∃ B, ∀ y, y ∈ B ↔ ∃ x, x ∈ A ∧ R x y.
Axiom Union : ∀ F, ∃ A, ∀ x y, x ∈ y ∧ y ∈ F → x ∈ A.
Axiom Powerset : ∀ x, ∃ y, ∀ z, (∀ u, u ∈ z → u ∈ x) → z ∈ y.
Axiom Infinity : ∃ X, (∃ y, (∀ z, z ∉ y) ∧ y ∈ X) ∧ ∀ x,
x ∈ X → ∃ y, y ∈ X ∧ ∀ z, z ∈ y ↔ z ∈ x ∨ z = x.
(* End of axioms. *)
Theorem Empty_Set : ∃ w, ∀ x, x ∉ w.
Proof.
move: Infinity => [x [[w [H _]] _]]; eauto.
Qed.
Definition empty_set :=
let (w, _) := (constructive_indefinite_description _ Empty_Set) in w.
Notation "∅" := empty_set.
Theorem Empty_set_classification : ∀ w, w ∉ ∅.
Proof.
rewrite /empty_set; by elim: constructive_indefinite_description.
Qed.
Theorem Nonempty_classification : ∀ y, y ≠ ∅ ↔ ∃ x, x ∈ y.
Proof.
split => [H | [x] /[swap] -> /Empty_set_classification] //.
apply NNPP => H0; apply H, Extensionality => z.
split => [H1 | /Empty_set_classification] //; contradict H0; eauto.
Qed.
Theorem Specification : ∀ z p, ∃ y, ∀ x, x ∈ y ↔ x ∈ z ∧ p x.
Proof.
move=> z p; case (classic (∃ x, x ∈ z ∧ p x)) => [[e [H H0]] | H].
- elim (Replacement z (λ x y, p x ∧ x = y ∨ ¬ p x ∧ e = y)) => x H1.
+ exists x; split => [ /H1 [w [H2 [ [H3 <-] | [H3 <-] ]]] | ] //.
rewrite H1; intuition eauto.
+ case (classic (p x)); [ exists x | exists e ]; split; intuition tauto.
- exists ∅; split => [/Empty_set_classification | H0] //.
contradict H; eauto.
Qed.
Definition specify : set → (set → Prop) → set.
Proof.
move=> A p.
elim (constructive_indefinite_description _ (Specification A p)) => [S] //.
Defined.
Notation "{ x 'in' A | P }" := (specify A (λ x, P)).
Theorem Specify_classification : ∀ A P x, x ∈ {x in A | P x} ↔ x ∈ A ∧ P x.
Proof.
rewrite /specify => A p x.
repeat elim constructive_indefinite_description => //.
Qed.
Definition subset a b := ∀ x, x ∈ a → x ∈ b.
Infix "⊂" := subset (at level 70).
Definition P x := let (y, H) := (constructive_indefinite_description _
(Powerset x)) in {s in y | s ⊂ x}.
Theorem Powerset_classification : ∀ X x, x ∈ P X ↔ x ⊂ X.
Proof.
rewrite /P /specify => X x.
repeat (elim constructive_indefinite_description => /= ?).
split; rewrite p; firstorder.
Qed.
Theorem Empty_set_is_subset : ∀ X, ∅ ⊂ X.
Proof.
move=> X z /Empty_set_classification //.
Qed.
Theorem Empty_set_in_powerset : ∀ X, ∅ ∈ P X.
Proof.
firstorder using Powerset_classification, Empty_set_is_subset.
Qed.
Theorem Set_is_subset : ∀ X, X ⊂ X.
Proof.
firstorder.
Qed.
Theorem Set_in_powerset : ∀ X, X ∈ P X.
Proof.
firstorder using Powerset_classification, Set_is_subset.
Qed.
Theorem Subset_equality : ∀ A B, A ⊂ B → B ⊂ A → A = B.
Proof.
move=> A B H H0; apply Extensionality; intuition.
Qed.
Theorem Subset_equality_iff : ∀ A B, A ⊂ B ∧ B ⊂ A ↔ A = B.
Proof.
split => H; subst; firstorder using Subset_equality, Set_is_subset.
Qed.
Lemma Subset_of_subsets_of_emptyset : ∀ a, a ∈ P (P ∅) → a = ∅ ∨ a = P ∅.
Proof.
move=> a.
(case (classic (a = ∅)); try tauto) => H /Powerset_classification => H0.
apply or_intror, Subset_equality_iff, conj;
auto => z /Powerset_classification H1.
suff -> : z = ∅.
- move: H H0 => /Nonempty_classification => [[x H]].
move: (H) => /[swap] /[apply] /Powerset_classification => H0.
suff -> : ∅ = x => //.
apply Subset_equality_iff, conj; auto using Empty_set_is_subset.
- apply Subset_equality_iff, conj; auto using Empty_set_is_subset.
Qed.
Theorem Powerset_nonempty : ∀ x, ∅ ≠ P x.
Proof.
move: Empty_set_classification => /[swap] x /[swap] -> /(_ x) => H.
apply H, Set_in_powerset.
Qed.
Theorem Pairing : ∀ x y, ∃ z, x ∈ z ∧ y ∈ z.
Proof.
move=> x y.
elim (Replacement (P (P ∅)) (λ a b, ∅ = a ∧ x = b ∨ P ∅ = a ∧ y = b)) => z.
- eexists; split; apply H; eauto using Empty_set_in_powerset, Set_in_powerset.
- move => /Subset_of_subsets_of_emptyset; elim; [ exists x | exists y ];
split; intuition; subst; by contradiction (Powerset_nonempty ∅).
Qed.
Definition pair x y :=
let (z, H) := (constructive_indefinite_description _ (Pairing x y))
in {t in z | t = x ∨ t = y}.
Notation " { x , y } " := (pair x y).
Notation " { x } " := (pair x x).
Lemma Pairing_classification : ∀ x y z, z ∈ {x, y} ↔ z = x ∨ z = y.
Proof.
rewrite /pair /specify => x y z.
(repeat elim constructive_indefinite_description => ? /=) =>
->; intuition congruence.
Qed.
As you can see, although ZFC traditionally includes the axiom of pairing and the axiom schema of specification, these statements can be proved from the others. The axiom of choice can also be proved using the above -- in particular, constructive_indefinite_description, which I assumed as an axiom, implies choice.
