From b5b141ebe7631c8c57ee54227a5a628471a8e2a5 Mon Sep 17 00:00:00 2001
From: Sankalp Gambhir <sankalp.gambhir47@gmail.com>
Date: Thu, 22 Sep 2022 12:14:13 +0200
Subject: [PATCH] added subset definition axiom
---
.../src/main/scala/lisa/settheory/SetTheoryZAxioms.scala | 2 ++
1 file changed, 2 insertions(+)
diff --git a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
index ecf2c80c..824498f5 100644
--- a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
+++ b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
@@ -17,6 +17,7 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
final val extensionalityAxiom: Formula = forall(x, forall(y, forall(z, in(z, x) <=> in(z, y)) <=> (x === y)))
final val pairAxiom: Formula = forall(x, forall(y, forall(z, in(z, pair(x, y)) <=> (x === z) \/ (y === z))))
final val unionAxiom: Formula = forall(x, forall(z, in(x, union(z)) <=> exists(y, in(x, y) /\ in(y, z))))
+ final val subsetAxiom: Formula = forall(x, forall(y, subset(x, y) <=> forall(z, (in(z, x) ==> in(z, y)))))
final val powerAxiom: Formula = forall(x, forall(y, in(x, powerSet(y)) <=> subset(x, y)))
final val foundationAxiom: Formula = forall(x, !(x === emptySet()) ==> exists(y, in(y, x) /\ forall(z, in(z, x) ==> !in(z, y))))
@@ -27,6 +28,7 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
("extensionalityAxiom", extensionalityAxiom),
("pairAxiom", pairAxiom),
("unionAxiom", unionAxiom),
+ ("subsetAxiom", subsetAxiom),
("powerAxiom", powerAxiom),
("foundationAxiom", foundationAxiom),
("comprehensionSchema", comprehensionSchema)
--
GitLab