From 85fef2f48274d2597c5f940c75a0088f6bfd5030 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 9 Oct 2015 11:57:37 +0200
Subject: [PATCH] =?UTF-8?q?Attempt=20to=20add=20Hilbert=E2=80=99s=20choice?=
 =?UTF-8?q?=20operator?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

and hence the Axiom of Choice to the logic. It seems that this is a way
to make progress towards #68, but the unification fails. Likely, this
needs better control about the instantiation of certain rules.
---
 examples/logics/predicate+choice.yaml | 187 ++++++++++++++++++++++++++
 logic/Propositions.hs                 |  11 +-
 sessions.yaml                         |   8 +-
 3 files changed, 199 insertions(+), 7 deletions(-)
 create mode 100644 examples/logics/predicate+choice.yaml

diff --git a/examples/logics/predicate+choice.yaml b/examples/logics/predicate+choice.yaml
new file mode 100644
index 0000000..ab76759
--- /dev/null
+++ b/examples/logics/predicate+choice.yaml
@@ -0,0 +1,187 @@
+rules:
+- id: allI
+  desc:
+    intro: ∀
+  free: ["P"]
+  local: ["c"]
+  ports:
+    in1:
+      type: assumption
+      proposition: P(c)
+      scoped: ["c"]
+    out2:
+      type: conclusion
+      proposition: ∀x.P(x)
+- id: allE
+  desc:
+    elim: ∀
+  free: ["P","y"]
+  ports:
+    in1:
+      type: assumption
+      proposition: ∀x.P(x)
+    out2:
+      type: conclusion
+      proposition: P(y)
+- id: exI
+  desc:
+    intro: ∃
+  free: ["P", "y"]
+  ports:
+    in1:
+      type: assumption
+      proposition: P(y)
+    out2:
+      type: conclusion
+      proposition: ∃x.P(x)
+- id: exE
+  desc:
+    elim: ∃
+  free: ["P","Q"]
+  local: ["c"]
+  ports:
+    in1:
+      type: assumption
+      proposition: ∃x.P(x)
+    in2:
+      type: assumption
+      proposition: Q
+      scoped: ["c"]
+    hyp:
+      type: local hypothesis
+      proposition: P(c)
+      consumedBy: in2
+    out:
+      type: conclusion
+      proposition: Q
+- id: conjI
+  free: ["A","B"]
+  desc:
+    intro: ∧
+  ports:
+    in1:
+      type: assumption
+      proposition: A
+    in2:
+      type: assumption
+      proposition: B
+    out:
+      type: conclusion
+      proposition: A∧B
+- id: conjE
+  free: ["A","B"]
+  desc:
+    elim: ∧
+  ports:
+    in:
+      type: assumption
+      proposition: A∧B
+    out1:
+      type: conclusion
+      proposition: A
+    out2:
+      type: conclusion
+      proposition: B
+- id: impI
+  desc:
+    intro: →
+  free: ["A","B"]
+  ports:
+    hyp:
+      type: local hypothesis
+      consumedBy: in
+      proposition: A
+    in:
+      type: assumption
+      proposition: B
+    out:
+      type: conclusion
+      proposition: A→B
+- id: impE
+  desc:
+    elim: →
+  free: ["A","B"]
+  ports:
+    in1:
+      type: assumption
+      proposition: A→B
+    in2:
+      type: assumption
+      proposition: A
+    out:
+      type: conclusion
+      proposition: B
+- id: disjI1
+  desc:
+    intro: ·∨
+  free: ["A","B"]
+  ports:
+    in:
+      type: assumption
+      proposition: A
+    out:
+      type: conclusion
+      proposition: A∨B
+- id: disjI2
+  desc:
+    intro: ∨·
+  free: ["A","B"]
+  ports:
+    in:
+      type: assumption
+      proposition: B
+    out:
+      type: conclusion
+      proposition: A∨B
+- id: disjE
+  desc:
+    elim: ∨
+  free: ["A","B","P"]
+  ports:
+    in:
+      type: assumption
+      proposition: A∨B
+    hyp1:
+      type: local hypothesis
+      proposition: A
+      consumedBy: in1
+    in1:
+      type: assumption
+      proposition: P
+    hyp2:
+      type: local hypothesis
+      proposition: B
+      consumedBy: in2
+    in2:
+      type: assumption
+      proposition: P
+    out:
+      type: conclusion
+      proposition: P
+- id: falseE
+  desc:
+    elim: ⊥
+  free: ["P"]
+  ports:
+    in:
+      type: assumption
+      proposition: "⊥"
+    out:
+      type: conclusion
+      proposition: P
+- id: TND
+  free: ["P"]
+  ports:
+    out:
+      type: conclusion
+      proposition: "P∨(P→⊥)"
+- id: AoC
+  free: ["P", "y"]
+  ports:
+    in:
+       type: assumption
+       proposition: "P(y)"
+    out:
+       type: conclusion
+       proposition: "P(ε(P))"
+
diff --git a/logic/Propositions.hs b/logic/Propositions.hs
index 954b26d..21f4b13 100644
--- a/logic/Propositions.hs
+++ b/logic/Propositions.hs
@@ -105,7 +105,7 @@ isInFix "→" = Just (2, R)
 isInFix _   = Nothing
 
 isQuant :: String -> Bool
-isQuant = (`elem` words "∃ ∀")
+isQuant = (`elem` map ((:"") . fst) quantifiers)
 
 isPrefix :: String -> Maybe Int
 isPrefix "¬" = Just 4
@@ -144,6 +144,7 @@ quantifiers :: [(Char, [Char])]
 quantifiers =
     [ ('∀', ['!'])
     , ('∃', ['?'])
+    , ('ε', [])
     , ('λ', ['\\'])
     ]
 
@@ -165,9 +166,11 @@ atomP = choice
         p <- atomP
         return $ s "¬" [p]
     , do
-        q <- quantP
-        vname <- nameP
-        _ <- l $ char '.'
+        (q,vname) <- try $ do -- allow backtracking after the ., for "ε(P)"
+            q <- quantP
+            vname <- nameP
+            _ <- l $ char '.'
+            return (q,vname)
         p <- termP
         return $ mkQuant q vname $ p
     , parenthesized termP
diff --git a/sessions.yaml b/sessions.yaml
index e19d457..7b25acb 100644
--- a/sessions.yaml
+++ b/sessions.yaml
@@ -184,9 +184,6 @@
     conclusions: ["∀x.P(x)→A"]
   - assumptions: ["∀x.(P(x)→Q(x))", "P(a)"]
     conclusions: ["Q(a)"]
-# Das tut noch nicht. Bug?
-#  - assumptions: ["∀x.∃y.P(x,y)"]
-#    conclusions: ["∃f.∀x.P(x,f(x))"]
   - assumptions: ["∀x.∀y.P(x,y)"]
     conclusions: ["∀y.∀x.P(x,y)"]
   - assumptions: ["∃x.∃y.P(x,y)"]
@@ -201,6 +198,11 @@
   - conclusions: ["∃x.t(x)→(∀x.t(x))"]
   - assumptions: ["∀x.(r(x)→⊥)→r(f(x))"]
     conclusions: ["∃x.r(x)∧r(f(f(x)))"]
+- name: Session 8
+  logic: predicate+choice
+  tasks:
+  - assumptions: ["∀x.∃y.P(x,y)"]
+    conclusions: ["∃f.∀x.P(x,f(x))"]
 - name: Hilbert system
   logic: hilbert
   tasks: