From ebd283cbee9a17df0516cb7b31c029e978fbde56 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 2 Dec 2025 14:40:04 +0100 Subject: [PATCH] FOL: eta expand exist quantifier --- FOL.lp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/FOL.lp b/FOL.lp index 71b040a..865568a 100644 --- a/FOL.lp +++ b/FOL.lp @@ -20,15 +20,15 @@ builtin "ex" ≔ ∃; notation ∃ quantifier; -constant symbol ∃ᵢ [a p] (x:τ a) : π (p x) → π (∃ p); +constant symbol ∃ᵢ [a p] (x:τ a) : π (p x) → π (`∃ x, p x); -symbol ∃ₑ [a p] : π (∃ p) → Π [q], (Π x:τ a, π (p x) → π q) → π q; +symbol ∃ₑ [a p] : π (`∃ x, p x) → Π [q], (Π x:τ a, π (p x) → π q) → π q; rule ∃ₑ (∃ᵢ $x $px) $f ↪ $f $x $px; // properties -opaque symbol ¬∃ [a] p : π (¬ (∃ p) ⇒ `∀ x : τ a, ¬ (p x)) ≔ +opaque symbol ¬∃ [a] p : π (¬ (`∃ x, p x) ⇒ `∀ x : τ a, ¬ (p x)) ≔ begin assume a p not_ex_p x px; apply not_ex_p; apply ∃ᵢ x px end;