Set: add axiom saying that sets are non-empty (#27)

Deducteam · Jan 31, 2025 · 2a4794a · 2a4794a
1 parent 1fff6f4
commit 2a4794a
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/CHANGES.md b/CHANGES.md
@@ -11,7 +11,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Impred: Set constructor o for quantifying over propositions
 - Epsilon: Hilbert's ε operator
 - List: add iota and indexes
-- Set: add ι:Set
+- Set: add ι:Set and an axiom el:Π a,τ a saying that every set is non-empty 
 - Pos, Z: add printing to decimal notation
 
 ### Changed

diff --git a/Set.lp b/Set.lp
@@ -10,6 +10,10 @@ injective symbol τ : Set → TYPE; // `t or \tau
 
 builtin "T" ≔ τ;
 
+// We assume that sets are non-empty
+
+symbol el a : τ a;
+
 // Cartesian product
 
 constant symbol × : Set → Set → Set; notation × infix right 10; // \times