From 997fdf0e45e90a7face1a36e21e5188dc1164b84 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 9 Jan 2025 18:26:15 +0100 Subject: [PATCH 1/2] Set: add axiom saying that sets are non-empty --- Set.lp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Set.lp b/Set.lp index 086e526..891ba8c 100644 --- 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 From 91306a65b793058836823c2495a9a382e5c016f1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 9 Jan 2025 18:29:15 +0100 Subject: [PATCH 2/2] update CHANGES --- CHANGES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGES.md b/CHANGES.md index 7d73836..2693c76 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -11,7 +11,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/). HOL: Set constructor ⤳ for quantifying over function types Impred: Set constructor o for quantifying over propositions Epsilon: Hilbert's ε operator -- Set: add ι:Set +- Set: add ι:Set and an axiom el:Π a,τ a saying that every set is non-empty - Bool: declare istrue as injective ## 1.1.0 (2024-06-21)