From 178f712de33b6518580d0553b3af4f8973489895 Mon Sep 17 00:00:00 2001
From: David Doret <david.doret@me.com>
Date: Sun, 1 Oct 2023 18:20:17 +0200
Subject: [PATCH] documentation #195 + inference validation #126 + support for
 the composition of collection-like formulae

---
 .idea/workspace.xml                           |  52 +++----
 src/punctilious/core.py                       | 147 +++++++++---------
 .../sample_biconditional_introduction.py      |   4 +-
 3 files changed, 101 insertions(+), 102 deletions(-)

diff --git a/.idea/workspace.xml b/.idea/workspace.xml
index 67379c16..20d4c025 100644
--- a/.idea/workspace.xml
+++ b/.idea/workspace.xml
@@ -4,10 +4,10 @@
     <option name="autoReloadType" value="SELECTIVE" />
   </component>
   <component name="ChangeListManager">
-    <list default="true" id="48b609c4-0198-44a9-8f40-0a1e1f4ae31e" name="Changes" comment="documentation #195 + inference validation #126">
+    <list default="true" id="48b609c4-0198-44a9-8f40-0a1e1f4ae31e" name="Changes" comment="documentation #195 + inference validation #126 + support for the composition of collection-like formulae">
       <change beforePath="$PROJECT_DIR$/.idea/workspace.xml" beforeDir="false" afterPath="$PROJECT_DIR$/.idea/workspace.xml" afterDir="false" />
       <change beforePath="$PROJECT_DIR$/src/punctilious/core.py" beforeDir="false" afterPath="$PROJECT_DIR$/src/punctilious/core.py" afterDir="false" />
-      <change beforePath="$PROJECT_DIR$/tests/test_formula.py" beforeDir="false" afterPath="$PROJECT_DIR$/tests/test_formula.py" afterDir="false" />
+      <change beforePath="$PROJECT_DIR$/src/sample/sample_biconditional_introduction.py" beforeDir="false" afterPath="$PROJECT_DIR$/src/sample/sample_biconditional_introduction.py" afterDir="false" />
     </list>
     <option name="SHOW_DIALOG" value="false" />
     <option name="HIGHLIGHT_CONFLICTS" value="true" />
@@ -120,7 +120,7 @@
       <recent name="C:\Users\David\PycharmProjects\punctilious\continuous_integration" />
     </key>
   </component>
-  <component name="RunManager" selected="Python tests.Python tests in test_formula.py">
+  <component name="RunManager" selected="Python.sample_biconditional_introduction">
     <configuration name="build" type="PythonConfigurationType" factoryName="Python" nameIsGenerated="true">
       <module name="2023_05_02_PyCharmProject_Maths" />
       <option name="INTERPRETER_OPTIONS" value="" />
@@ -228,7 +228,7 @@
       <option name="INPUT_FILE" value="" />
       <method v="2" />
     </configuration>
-    <configuration name="sample_biconditional_elimination_2" type="PythonConfigurationType" factoryName="Python" temporary="true" nameIsGenerated="true">
+    <configuration name="sample_biconditional_introduction" type="PythonConfigurationType" factoryName="Python" temporary="true" nameIsGenerated="true">
       <module name="2023_05_02_PyCharmProject_Maths" />
       <option name="INTERPRETER_OPTIONS" value="" />
       <option name="PARENT_ENVS" value="true" />
@@ -240,7 +240,7 @@
       <option name="IS_MODULE_SDK" value="true" />
       <option name="ADD_CONTENT_ROOTS" value="true" />
       <option name="ADD_SOURCE_ROOTS" value="true" />
-      <option name="SCRIPT_NAME" value="$PROJECT_DIR$/src/sample/sample_biconditional_elimination_2.py" />
+      <option name="SCRIPT_NAME" value="$PROJECT_DIR$/src/sample/sample_biconditional_introduction.py" />
       <option name="PARAMETERS" value="" />
       <option name="SHOW_COMMAND_LINE" value="false" />
       <option name="EMULATE_TERMINAL" value="false" />
@@ -324,7 +324,7 @@
       <option name="_new_targetType" value="&quot;PYTHON&quot;" />
       <method v="2" />
     </configuration>
-    <configuration name="Python tests in test_biconditional_elimination_1.py" type="tests" factoryName="Autodetect" temporary="true" nameIsGenerated="true">
+    <configuration name="Python tests in test_absorption.py" type="tests" factoryName="Autodetect" temporary="true" nameIsGenerated="true">
       <module name="2023_05_02_PyCharmProject_Maths" />
       <option name="INTERPRETER_OPTIONS" value="" />
       <option name="PARENT_ENVS" value="true" />
@@ -334,11 +334,11 @@
       <option name="ADD_CONTENT_ROOTS" value="true" />
       <option name="ADD_SOURCE_ROOTS" value="true" />
       <option name="_new_additionalArguments" value="&quot;&quot;" />
-      <option name="_new_target" value="&quot;$PROJECT_DIR$/tests/test_biconditional_elimination_1.py&quot;" />
+      <option name="_new_target" value="&quot;$PROJECT_DIR$/tests/test_absorption.py&quot;" />
       <option name="_new_targetType" value="&quot;PATH&quot;" />
       <method v="2" />
     </configuration>
-    <configuration name="Python tests in test_biconditional_elimination_2.py" type="tests" factoryName="Autodetect" temporary="true" nameIsGenerated="true">
+    <configuration name="Python tests in test_axiom_interpretation.py" type="tests" factoryName="Autodetect" temporary="true" nameIsGenerated="true">
       <module name="2023_05_02_PyCharmProject_Maths" />
       <option name="INTERPRETER_OPTIONS" value="" />
       <option name="PARENT_ENVS" value="true" />
@@ -348,7 +348,7 @@
       <option name="ADD_CONTENT_ROOTS" value="true" />
       <option name="ADD_SOURCE_ROOTS" value="true" />
       <option name="_new_additionalArguments" value="&quot;&quot;" />
-      <option name="_new_target" value="&quot;$PROJECT_DIR$/tests/test_biconditional_elimination_2.py&quot;" />
+      <option name="_new_target" value="&quot;$PROJECT_DIR$/tests/test_axiom_interpretation.py&quot;" />
       <option name="_new_targetType" value="&quot;PATH&quot;" />
       <method v="2" />
     </configuration>
@@ -386,24 +386,24 @@
       <item itemvalue="Python.prebuild_generate_theory_reports" />
       <item itemvalue="Python.build" />
       <item itemvalue="Python.prebuild_generate_sample_outputs" />
-      <item itemvalue="Python.sample_biconditional_elimination_2" />
+      <item itemvalue="Python.sample_biconditional_introduction" />
       <item itemvalue="Python docs.Sphinx HTML" />
       <item itemvalue="Python tests.Python tests in tests" />
       <item itemvalue="Python tests.Python tests for test_formula.TestFormula.test_formula" />
-      <item itemvalue="Python tests.Python tests in test_biconditional_elimination_1.py" />
-      <item itemvalue="Python tests.Python tests in test_biconditional_elimination_2.py" />
+      <item itemvalue="Python tests.Python tests in test_axiom_interpretation.py" />
       <item itemvalue="Python tests.Python tests in test_formula.py" />
+      <item itemvalue="Python tests.Python tests in test_absorption.py" />
       <item itemvalue="Shell Script.pytest tests" />
       <item itemvalue="Shell Script.pytest" />
       <item itemvalue="Shell Script.python -m build" />
     </list>
     <recent_temporary>
       <list>
+        <item itemvalue="Python.sample_biconditional_introduction" />
+        <item itemvalue="Python tests.Python tests in test_absorption.py" />
+        <item itemvalue="Python tests.Python tests in test_axiom_interpretation.py" />
         <item itemvalue="Python tests.Python tests in test_formula.py" />
         <item itemvalue="Python tests.Python tests for test_formula.TestFormula.test_formula" />
-        <item itemvalue="Python tests.Python tests in test_biconditional_elimination_2.py" />
-        <item itemvalue="Python.sample_biconditional_elimination_2" />
-        <item itemvalue="Python tests.Python tests in test_biconditional_elimination_1.py" />
       </list>
     </recent_temporary>
   </component>
@@ -416,14 +416,6 @@
       <option name="presentableId" value="Default" />
       <updated>1687980987309</updated>
     </task>
-    <task id="LOCAL-00281" summary="#201 + #195">
-      <option name="closed" value="true" />
-      <created>1694804958570</created>
-      <option name="number" value="00281" />
-      <option name="presentableId" value="LOCAL-00281" />
-      <option name="project" value="LOCAL" />
-      <updated>1694804958570</updated>
-    </task>
     <task id="LOCAL-00282" summary="#201 + #195">
       <option name="closed" value="true" />
       <created>1694805791183</created>
@@ -808,7 +800,15 @@
       <option name="project" value="LOCAL" />
       <updated>1696161914326</updated>
     </task>
-    <option name="localTasksCounter" value="330" />
+    <task id="LOCAL-00330" summary="documentation #195 + inference validation #126 + support for the composition of collection-like formulae">
+      <option name="closed" value="true" />
+      <created>1696169627440</created>
+      <option name="number" value="00330" />
+      <option name="presentableId" value="LOCAL-00330" />
+      <option name="project" value="LOCAL" />
+      <updated>1696169627440</updated>
+    </task>
+    <option name="localTasksCounter" value="331" />
     <servers />
   </component>
   <component name="Vcs.Log.Tabs.Properties">
@@ -840,7 +840,6 @@
     <option name="CHECK_CODE_CLEANUP_BEFORE_PROJECT_COMMIT" value="true" />
     <option name="CHECK_NEW_TODO" value="false" />
     <option name="ADD_EXTERNAL_FILES_SILENTLY" value="true" />
-    <MESSAGE value="implement #147 + biconditional-introduction + InferenceRuleDeclaration.declaration implemented as a Formula instead of StyledText." />
     <MESSAGE value="implement #154: review of all inference-rules" />
     <MESSAGE value="reorganization of sphinx doc in subfolders" />
     <MESSAGE value="enhance documentation #48" />
@@ -865,7 +864,8 @@
     <MESSAGE value="cleanup" />
     <MESSAGE value="documentation #195" />
     <MESSAGE value="documentation #195 + inference validation #126" />
-    <option name="LAST_COMMIT_MESSAGE" value="documentation #195 + inference validation #126" />
+    <MESSAGE value="documentation #195 + inference validation #126 + support for the composition of collection-like formulae" />
+    <option name="LAST_COMMIT_MESSAGE" value="documentation #195 + inference validation #126 + support for the composition of collection-like formulae" />
     <option name="REFORMAT_BEFORE_PROJECT_COMMIT" value="true" />
   </component>
   <component name="XDebuggerManager">
diff --git a/src/punctilious/core.py b/src/punctilious/core.py
index 9f7943ef..f5c7efb5 100644
--- a/src/punctilious/core.py
+++ b/src/punctilious/core.py
@@ -3807,7 +3807,8 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
         explicit_name = 'absorption inference rule'
         name = 'absorption'
         with u.v(symbol='P') as p, u.v(symbol='Q') as q:
-            definition = (p | u.r.implies | q) | u.r.proves | (p | u.r.implies | (p | u.r.land | q))
+            definition = u.r.sequent_premises(p | u.r.implies | q) | u.r.proves | (
+                    p | u.r.implies | (p | u.r.land | q))
         with u.v(symbol='P') as p, u.v(symbol='Q') as q:
             self.parameter_p_implies_q = p | u.r.implies | q
             self.parameter_p_implies_q_mask = frozenset([p, q])
@@ -3858,7 +3859,7 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
         explicit_name = 'axiom interpretation inference rule'
         name = 'axiom interpretation'
         with u.v(symbol=ScriptNormal('A')) as a, u.v(symbol='P') as p:
-            definition = (a | u.r.sequent_comma | p) | u.r.proves | p
+            definition = u.r.sequent_premises(a, p) | u.r.proves | p
         with u.v(symbol=ScriptNormal('A')) as a:
             self.parameter_a = a
             self.parameter_a_mask = frozenset([a])
@@ -3995,19 +3996,20 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
         explicit_name = 'biconditional introduction inference rule'
         name = 'biconditional introduction'
         with u.v(symbol='P') as p, u.v(symbol='Q') as q:
-            definition = (((p | u.r.implies | q) | u.r.sequent_comma | (
-                    q | u.r.implies | p)) | u.r.proves | (p | u.r.iff | q))
+            definition = u.r.sequent_premises(p | u.r.implies | q,
+                q | u.r.implies | p) | u.r.proves | (p | u.r.iff | q)
         with u.v(symbol='P') as p, u.v(symbol='Q') as q:
             self.parameter_p_implies_q = p | u.r.implies | q
             self.parameter_p_implies_q_mask = frozenset([p, q])
         with u.v(symbol='P') as p, u.v(symbol='Q') as q:
-            self.parameter_q_implies_p = q | u.r.iff | p
+            self.parameter_q_implies_p = q | u.r.implies | p
             self.parameter_q_implies_p_mask = frozenset([p, q])
         super().__init__(definition=definition, universe_of_discourse=universe_of_discourse,
             symbol=symbol, auto_index=auto_index, dashed_name=dashed_name, acronym=acronym,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo)
 
-    def construct_formula(self, p_iff_q: FormulaStatement = None) -> Formula:
+    def construct_formula(self, p_implies_q: FormulaStatement,
+            q_implies_p: FormulaStatement) -> Formula:
         """
         .. include:: ../../include/construct_formula_python_method.rstinc
 
@@ -4023,12 +4025,18 @@ def construct_formula(self, p_iff_q: FormulaStatement = None) -> Formula:
             raise_exception=True)
         q_implies_p: Formula
         p_implies_q__p: Formula = p_implies_q.parameters[0]
-        # TODO: Do not is but use is_syntactically_equivalent instead.
-        verify(assertion=p_implies_q.parameters[0] is p_implies_q.parameters[1], msg='The ⌜p⌝ in ',
-            severity=verification_severities.error, raise_exception=True)
-        p: Formula = p_implies_q.parameters[0]
-        q: Formula = p_implies_q.parameters[1]
-        output = (q | self.u.r.implies | p)
+        p_implies_q__q: Formula = p_implies_q.parameters[1]
+        q_implies_p__q: Formula = q_implies_p.parameters[0]
+        q_implies_p__p: Formula = q_implies_p.parameters[1]
+        verify(assertion=p_implies_q__p.is_formula_syntactically_equivalent_to(q_implies_p__p),
+            msg='The ⌜p⌝ in ⌜p_implies_q⌝ is not syntactically-equivalent to the ⌜p⌝ in  ⌜q_implies_p⌝.',
+            severity=verification_severities.error, raise_exception=True, p_implies_q=p_implies_q,
+            p_implies_q__p=p_implies_q__p, q_implies_p=q_implies_p, q_implies_p__p=q_implies_p__p)
+        verify(assertion=p_implies_q__q.is_formula_syntactically_equivalent_to(q_implies_p__q),
+            msg='The ⌜q⌝ in ⌜p_implies_q⌝ is not syntactically-equivalent to the ⌜q⌝ in  ⌜q_implies_p⌝.',
+            severity=verification_severities.error, raise_exception=True, p_implies_q=p_implies_q,
+            p_implies_q__q=p_implies_q__q, q_implies_p=q_implies_p, q_implies_p__q=q_implies_p__q)
+        output = p_implies_q__p | self.u.r.iff | p_implies_q__q
         return output
 
 
@@ -4123,7 +4131,7 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
         explicit_name = 'conjunction introduction inference rule'
         name = 'conjunction introduction'
         with u.v(symbol='P') as p, u.v(symbol='Q') as q:
-            definition = ((p | u.r.sequent_comma | q) | u.r.proves | (p | u.r.land | q))
+            definition = ((p | u.r.sequent_premises | q) | u.r.proves | (p | u.r.land | q))
         super().__init__(definition=definition, universe_of_discourse=universe_of_discourse,
             symbol=symbol, auto_index=auto_index, dashed_name=dashed_name, acronym=acronym,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo)
@@ -4161,9 +4169,9 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
         name = 'constructive dilemma'
         with u.v(symbol='P') as p, u.v(symbol='Q') as q, u.v(symbol='R') as r, u.v(symbol='S') as s:
             # TODO: FEATURE #216: Review this definition once sequence-comma supports n-ary components.
-            definition = ((p | u.r.implies | q) | u.r.sequent_comma | (
-                    (r | u.r.implies | s) | u.r.sequent_comma | (p | u.r.lor | r))) | u.r.proves | (
-                                 q | u.r.lor | s)
+            definition = ((p | u.r.implies | q) | u.r.sequent_premises | (
+                    (r | u.r.implies | s) | u.r.sequent_premises | (
+                    p | u.r.lor | r))) | u.r.proves | (q | u.r.lor | s)
         super().__init__(definition=definition, universe_of_discourse=universe_of_discourse,
             symbol=symbol, auto_index=auto_index, dashed_name=dashed_name, acronym=acronym,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo)
@@ -4228,7 +4236,7 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
             # Provide support for n-ary relations. First need: sequent-comma, or collection-comma.
             # definition = u.r.sequent_comma(d, x, y) | u.r.proves | (x | u.r.equal | y)
             # Meanwhile, I use combined 2-ary formulae:
-            definition = d | u.r.sequent_comma | (x | u.r.sequent_comma | y) | u.r.proves | (
+            definition = d | u.r.sequent_premises | (x | u.r.sequent_premises | y) | u.r.proves | (
                     x | u.r.equal | y)
         with u.v(symbol=ScriptNormal('D')) as d:
             self.parameter_d = d
@@ -4281,7 +4289,7 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
         explicit_name = 'destructive dilemma inference rule'
         name = 'destructive dilemma'
         with u.v(symbol='P') as p, u.v(symbol='Q') as q:
-            definition = ((p | u.r.sequent_comma | q) | u.r.proves | (p | u.r.land | q))
+            definition = ((p | u.r.sequent_premises | q) | u.r.proves | (p | u.r.land | q))
         super().__init__(definition=definition, universe_of_discourse=universe_of_discourse,
             symbol=symbol, auto_index=auto_index, dashed_name=dashed_name, acronym=acronym,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo)
@@ -4380,7 +4388,7 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
         explicit_name = 'disjunctive resolution inference rule'
         name = 'disjunctive resolution'
         with u.v(symbol='P') as p, u.v(symbol='Q') as q:
-            definition = ((p | u.r.sequent_comma | q) | u.r.proves | (p | u.r.land | q))
+            definition = ((p | u.r.sequent_premises | q) | u.r.proves | (p | u.r.land | q))
         super().__init__(definition=definition, universe_of_discourse=universe_of_discourse,
             symbol=symbol, auto_index=auto_index, dashed_name=dashed_name, acronym=acronym,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo)
@@ -4413,7 +4421,7 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
         explicit_name = 'disjunctive syllogism inference rule'
         name = 'disjunctive syllogism'
         with u.v(symbol='P') as p, u.v(symbol='Q') as q:
-            definition = ((p | u.r.sequent_comma | q) | u.r.proves | (p | u.r.land | q))
+            definition = ((p | u.r.sequent_premises | q) | u.r.proves | (p | u.r.land | q))
         super().__init__(definition=definition, universe_of_discourse=universe_of_discourse,
             symbol=symbol, auto_index=auto_index, dashed_name=dashed_name, acronym=acronym,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo)
@@ -4548,7 +4556,7 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
         explicit_name = 'equal terms substitution inference rule'
         name = 'equal terms substitution'
         with u.v(symbol='P') as p, u.v(symbol='Q') as q, u.v(symbol='x') as x, u.v(symbol='y') as y:
-            definition = (p | u.r.sequent_comma | (x | u.r.equal | y)) | u.r.proves | q
+            definition = (p | u.r.sequent_premises | (x | u.r.equal | y)) | u.r.proves | q
         super().__init__(definition=definition, universe_of_discourse=universe_of_discourse,
             symbol=symbol, auto_index=auto_index, dashed_name=dashed_name, acronym=acronym,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo)
@@ -4588,7 +4596,7 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
         explicit_name = 'hypothetical syllogism inference rule'
         name = 'hypothetical syllogism'
         with u.v(symbol='P') as p, u.v(symbol='Q') as q:
-            definition = ((p | u.r.sequent_comma | q) | u.r.proves | (p | u.r.land | q))
+            definition = ((p | u.r.sequent_premises | q) | u.r.proves | (p | u.r.land | q))
         super().__init__(definition=definition, universe_of_discourse=universe_of_discourse,
             symbol=symbol, auto_index=auto_index, dashed_name=dashed_name, acronym=acronym,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo)
@@ -4714,7 +4722,7 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
         explicit_name = 'modus ponens inference rule'
         name = 'modus ponens'
         with u.v(symbol='P') as p, u.v(symbol='Q') as q:
-            definition = ((p | u.r.implies | p) | u.r.sequent_comma | p) | u.r.proves | q
+            definition = ((p | u.r.implies | p) | u.r.sequent_premises | p) | u.r.proves | q
         super().__init__(definition=definition, universe_of_discourse=universe_of_discourse,
             symbol=symbol, auto_index=auto_index, dashed_name=dashed_name, acronym=acronym,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo)
@@ -4747,7 +4755,7 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
         explicit_name = 'modus tollens inference rule'
         name = 'modus tollens'
         with u.v(symbol='P') as p, u.v(symbol='Q') as q:
-            definition = ((p | u.r.implies | p) | u.r.sequent_comma | p) | u.r.proves | q
+            definition = ((p | u.r.implies | p) | u.r.sequent_premises | p) | u.r.proves | q
         super().__init__(definition=definition, universe_of_discourse=universe_of_discourse,
             symbol=symbol, auto_index=auto_index, dashed_name=dashed_name, acronym=acronym,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo)
@@ -5896,7 +5904,6 @@ def __init__(self, u: UniverseOfDiscourse):
         super().__init__()
         # Well-known objects
         self._biconditional = None
-        self._sequent_comma = None
         self._conjunction = None
         self._disjunction = None
         self._equality = None
@@ -5906,6 +5913,7 @@ def __init__(self, u: UniverseOfDiscourse):
         self._is_a = None
         self._map = None
         self._negation = None
+        self._sequent_premises = None
         self._syntactic_entailment = None
 
     def declare(self, arity: (None, int) = None, symbol: (None, str, StyledText) = None,
@@ -6183,19 +6191,18 @@ def proves(self):
         return self.syntactic_entailment
 
     @property
-    def sequent_comma(self):
-        """Initially needed to express the collection of premises in inference-rule formula definitions.
-
-        For the time being it is sufficient to implement it as a binary relation,
-        because our initial catalog of inference rules have one or two premises.
-        But at a later point, we will need to implement (0-n)-ary relations.
+    def sequent_premises(self):
+        """Expresses the collection of premises in inference-rule formula definitions.
         """
-        if self._sequent_comma is None:
-            self._sequent_comma = self.declare(arity=2, formula_rep=Formula.infix,
-                signal_proposition=True, symbol=SerifItalic(plaintext=',', unicode=',', latex=','),
-                auto_index=False, dashed_name='sequent-comma', name='sequent comma',
-                explicit_name='sequent calculus comma')
-        return self._sequent_comma
+        global text_dict
+        if self._sequent_premises is None:
+            self._sequent_premises = self.declare(formula_rep=Formula.collection,
+                collection_start=text_dict.empty_string, collection_separator=text_dict.comma,
+                collection_end=text_dict.empty_string, signal_proposition=True,
+                symbol=SerifItalic(plaintext=',', unicode=',', latex=','), auto_index=False,
+                dashed_name='sequent-premises', name='sequent premises',
+                explicit_name='sequent calculus premises collection')
+        return self._sequent_premises
 
     @property
     def syntactic_entailment(self):
@@ -6932,61 +6939,53 @@ def __init__(self, t: TheoryElaborationSequence, echo: (None, bool) = None,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo,
             proof=proof)
 
+    def check_premises_validity(self, p_implies_q: FlexibleFormula = None,
+            q_implies_p: FlexibleFormula = None, raise_exception: bool = True) -> bool:
+        """
+        .. include:: ../../include/check_premises_validity_python_method.rstinc
+
+        """
+        # Validate that expected formula-statements are formula-statements in the current theory.
+        formula_ok, _, _ = verify_formula_statement(arg='p_implies_q', t=self.t,
+            input_value=p_implies_q, form=self.i.parameter_p_implies_q,
+            mask=self.i.parameter_p_implies_q_mask, raise_exception=raise_exception)
+        formula_ok, _, _ = verify_formula_statement(arg='q_implies_p', t=self.t,
+            input_value=q_implies_p, form=self.i.parameter_q_implies_p,
+            mask=self.i.parameter_q_implies_p_mask, raise_exception=raise_exception)
+        # The method either raises an exception during validation, or return True.
+        return formula_ok
+
     def compose_paragraph_proof(self, o: InferredStatement) -> collections.abc.Generator[
         Composable, Composable, bool]:
         output = yield from configuration.locale.compose_biconditional_introduction_paragraph_proof(
             o=o)
         return output
 
-    def check_inference_validity(self, p_implies_q: FormulaStatement = None,
-            q_implies_p: FormulaStatement = None, t: TheoryElaborationSequence = None) -> bool:
-        p_implies_q = verify_formula_statement(t=t, arity=2, input_value=p_implies_q)
-        verify(t.contains_theoretical_objct(p_implies_q),
-            'Statement ⌜p_implies_q⌝ must be contained in theory ⌜t⌝.', p_implies_q=p_implies_q,
-            t=t, slf=self)
-        q_implies_p = verify_formula_statement(t=t, arity=2, input_value=q_implies_p)
-        verify(t.contains_theoretical_objct(q_implies_p),
-            'Statement ⌜q_implies_p⌝ must be contained in theory ⌜t⌝.', q_implies_p=q_implies_p,
-            t=t, slf=self)
-        p_implies_q: Formula = verify_formula(u=t.u, arity=2, input_value=p_implies_q)
-        q_implies_p: Formula = verify_formula(u=t.u, arity=2, input_value=q_implies_p)
-        verify(p_implies_q.relation is t.u.r.implication,
-            'The relation of formula ⌜p_implies_q⌝ must be an implication.',
-            p_implies_q_relation=p_implies_q.relation, p_implies_q=p_implies_q, t=t, slf=self)
-        verify(q_implies_p.relation is t.u.r.implication,
-            'The relation of formula ⌜q_implies_p⌝ must be an implication.',
-            q_implies_p_relation=p_implies_q.relation, q_implies_p=q_implies_p, t=t, slf=self)
-
-        verify(p_implies_q.parameters[0].is_formula_syntactically_equivalent_to(
-            q_implies_p.parameters[1]),
-            'The p of the ⌜p_implies_q⌝ formula must be formula-syntactically-equivalent to the p of '
-            '⌜q_implies_p⌝ formula.', p_implies_q=p_implies_q, q_implies_p=q_implies_p, t=t,
-            slf=self)
-        verify(p_implies_q.parameters[1].is_formula_syntactically_equivalent_to(
-            q_implies_p.parameters[0]),
-            'The q of the ⌜p_implies_q⌝ formula must be formula-syntactically-equivalent to the q of '
-            '⌜q_implies_p⌝ formula.', p_implies_q=p_implies_q, q_implies_p=q_implies_p, t=t,
-            slf=self)
-        return True
+    @property
+    def i(self) -> BiconditionalIntroductionDeclaration:
+        """Override the base class i property with a specialized inherited class type."""
+        i: BiconditionalIntroductionDeclaration = super().i
+        return i
 
-    def infer_formula(self, p_implies_q: (tuple, Formula, FormulaStatement) = None,
-            q_implies_p: (tuple, Formula, FormulaStatement) = None, echo: (None, bool) = None):
+    def construct_formula(self, p_implies_q: FlexibleFormula = None,
+            q_implies_p: FlexibleFormula = None) -> Formula:
         """
         .. include:: ../../include/construct_formula_python_method.rstinc
 
         """
-        return super().infer_formula(p_iff_q, echo=echo)
+        # Call back the infer_formula method on the inference-rule declaration class.
+        return self.i.construct_formula(p_implies_q=p_implies_q, q_implies_p=q_implies_p)
 
-    def infer_formula_statement(self, p_implies_q: (tuple, Formula, FormulaStatement) = None,
-            q_implies_p: (tuple, Formula, FormulaStatement) = None,
-            nameset: (None, str, NameSet) = None, ref: (None, str) = None,
+    def infer_formula_statement(self, p_implies_q: FlexibleFormula = None,
+            q_implies_p: FlexibleFormula = None, ref: (None, str) = None,
             paragraph_header: (None, ParagraphHeader) = None, subtitle: (None, str) = None,
             echo: (None, bool) = None) -> InferredStatement:
         """
         .. include:: ../../include/infer_formula_statement_python_method.rstinc
 
         """
-        return super().infer_formula_statement(p_implies_q, q_implies_p, nameset=nameset, ref=ref,
+        premises = self.i.Premises(p_implies_q=p_implies_q, q_implies_p=q_implies_p)
+        return InferredStatement(i=self, premises=premises, ref=ref,
             paragraph_header=paragraph_header, subtitle=subtitle, echo=echo)
 
 
diff --git a/src/sample/sample_biconditional_introduction.py b/src/sample/sample_biconditional_introduction.py
index 910dedf3..1d5a2344 100644
--- a/src/sample/sample_biconditional_introduction.py
+++ b/src/sample/sample_biconditional_introduction.py
@@ -13,9 +13,9 @@
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(a=axiom)
 phi1 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
-    formula=r1(o1, o2) | u.r.implies | r2(o3))
+    p=r1(o1, o2) | u.r.implies | r2(o3))
 phi2 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
-    formula=r2(o3) | u.r.implies | r1(o1, o2))
+    p=r2(o3) | u.r.implies | r1(o1, o2))
 
 # And finally, use the biconditional-introduction inference-rule:
 biconditional_inference = t1.i.bi.infer_formula_statement(p_implies_q=phi1, q_implies_p=phi2,