From 3b1762d7dfaf3adc56888109718b93066d994a2f Mon Sep 17 00:00:00 2001
From: daviddoret <david.doret@me.com>
Date: Sat, 27 Jul 2024 18:49:56 +0200
Subject: [PATCH] version 2.0: re-starting from scratch with a new data model.

---
 .idea/workspace.xml              | 35 ++++++++++++++------------------
 src/punctilious/meta_theory_1.py | 11 +++++-----
 2 files changed, 21 insertions(+), 25 deletions(-)

diff --git a/.idea/workspace.xml b/.idea/workspace.xml
index c479bbf6..ab01ef83 100644
--- a/.idea/workspace.xml
+++ b/.idea/workspace.xml
@@ -6,12 +6,7 @@
   <component name="ChangeListManager">
     <list default="true" id="48b609c4-0198-44a9-8f40-0a1e1f4ae31e" name="Changes" comment="version 2.0: re-starting from scratch with a new data model.">
       <change beforePath="$PROJECT_DIR$/.idea/workspace.xml" beforeDir="false" afterPath="$PROJECT_DIR$/.idea/workspace.xml" afterDir="false" />
-      <change beforePath="$PROJECT_DIR$/src/punctilious/__init__.py" beforeDir="false" afterPath="$PROJECT_DIR$/src/punctilious/__init__.py" afterDir="false" />
-      <change beforePath="$PROJECT_DIR$/src/punctilious/axiomatic_system_1.py" beforeDir="false" afterPath="$PROJECT_DIR$/src/punctilious/axiomatic_system_1.py" afterDir="false" />
-      <change beforePath="$PROJECT_DIR$/src/punctilious/connectives_standard_library_1.py" beforeDir="false" afterPath="$PROJECT_DIR$/src/punctilious/connectives_standard_library_1.py" afterDir="false" />
       <change beforePath="$PROJECT_DIR$/src/punctilious/meta_theory_1.py" beforeDir="false" afterPath="$PROJECT_DIR$/src/punctilious/meta_theory_1.py" afterDir="false" />
-      <change beforePath="$PROJECT_DIR$/tests/test_axiomatic_system_1.py" beforeDir="false" afterPath="$PROJECT_DIR$/tests/test_axiomatic_system_1.py" afterDir="false" />
-      <change beforePath="$PROJECT_DIR$/tests/test_meta_theory_1.py" beforeDir="false" afterPath="$PROJECT_DIR$/tests/test_meta_theory_1.py" afterDir="false" />
     </list>
     <option name="SHOW_DIALOG" value="false" />
     <option name="HIGHLIGHT_CONFLICTS" value="true" />
@@ -258,7 +253,7 @@
     "Python tests.pytest for tests.test_axiomatic_system_1.top_level_collect.executor": "Run",
     "Python tests.pytest for tests.test_fl1.TestFormalObject.test_formal_object.executor": "Run",
     "Python tests.pytest for tests.test_fl1.executor": "Run",
-    "Python tests.pytest for tests.test_meta_theory_1.TestTProvesP.test_t_proves_p.executor": "Run",
+    "Python tests.pytest for tests.test_meta_theory_1.TestTProvesP.test_t_proves_p.executor": "Debug",
     "Python tests.pytest for tests.test_minimal_logic_1.TestPL1.test_pl1.executor": "Run",
     "Python tests.pytest for tests.test_pl1.TestPL1.test_declare_binary_formula.executor": "Run",
     "Python tests.pytest for tests.test_pl1.TestPL1.test_formulas.executor": "Run",
@@ -737,14 +732,6 @@
       <option name="presentableId" value="Default" />
       <updated>1687980987309</updated>
     </task>
-    <task id="LOCAL-00918" summary="version 2.0: re-starting from scratch with a new data model.">
-      <option name="closed" value="true" />
-      <created>1721457844846</created>
-      <option name="number" value="00918" />
-      <option name="presentableId" value="LOCAL-00918" />
-      <option name="project" value="LOCAL" />
-      <updated>1721457844846</updated>
-    </task>
     <task id="LOCAL-00919" summary="version 2.0: re-starting from scratch with a new data model.">
       <option name="closed" value="true" />
       <created>1721458131399</created>
@@ -1129,7 +1116,15 @@
       <option name="project" value="LOCAL" />
       <updated>1722082558618</updated>
     </task>
-    <option name="localTasksCounter" value="967" />
+    <task id="LOCAL-00967" summary="version 2.0: re-starting from scratch with a new data model.">
+      <option name="closed" value="true" />
+      <created>1722090186440</created>
+      <option name="number" value="00967" />
+      <option name="presentableId" value="LOCAL-00967" />
+      <option name="project" value="LOCAL" />
+      <updated>1722090186440</updated>
+    </task>
+    <option name="localTasksCounter" value="968" />
     <servers>
       <YouTrack url="https://punctilious.youtrack.cloud">
         <username>random</username>
@@ -1241,16 +1236,16 @@
           <line>3902</line>
           <option name="timeStamp" value="135" />
         </line-breakpoint>
-        <line-breakpoint enabled="true" suspend="THREAD" type="python-line">
-          <url>file://$PROJECT_DIR$/src/punctilious/meta_theory_1.py</url>
-          <line>313</line>
-          <option name="timeStamp" value="138" />
-        </line-breakpoint>
         <line-breakpoint enabled="true" suspend="THREAD" type="python-line">
           <url>file://$PROJECT_DIR$/src/punctilious/axiomatic_system_1.py</url>
           <line>2353</line>
           <option name="timeStamp" value="139" />
         </line-breakpoint>
+        <line-breakpoint enabled="true" suspend="THREAD" type="python-line">
+          <url>file://$PROJECT_DIR$/src/punctilious/axiomatic_system_1.py</url>
+          <line>3876</line>
+          <option name="timeStamp" value="140" />
+        </line-breakpoint>
       </breakpoints>
     </breakpoint-manager>
   </component>
diff --git a/src/punctilious/meta_theory_1.py b/src/punctilious/meta_theory_1.py
index 7068b72c..e9a4b227 100644
--- a/src/punctilious/meta_theory_1.py
+++ b/src/punctilious/meta_theory_1.py
@@ -266,16 +266,17 @@ def theory_proves_proposition_external_algorithm(p: as1.Tupl | None = None, a: a
     t: as1.Theory = as1.coerce_theory(t=a[0], interpret_none_as_empty=False, canonical_conversion=False)
     p2: as1.Formula = as1.coerce_formula(phi=a[1])
     if as1.is_valid_proposition_in_theory_1(p=p2, t=t):
-        phi: as1.Formula = t | as1.get_connectives().proves | p
+        phi: as1.Formula = t | as1.get_connectives().proves | p2
         return phi
     else:
         raise u1.ApplicativeError(
-            msg='Blablabla',
+            msg='Proposition `p2` is not valid in theory `t`. '
+                'It follows that `t ⊢ p` cannot be derived.',
             code=None,
-            p=p,
-            a=a,
+            p2=p2,
             t=t,
-            p2=p2
+            a=a,
+            p=p
         )