Skip to content

Commit 2b9f2ba

Browse files
v--v--
committed
Fix handling of eigenvariables in the code
1 parent 538912c commit 2b9f2ba

File tree

5 files changed

+151
-23
lines changed

5 files changed

+151
-23
lines changed

‎src/notebook/math/logic/deduction/proof_tree.py‎

Lines changed: 14 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@
88
InferenceTreeRenderer,
99
RuleApplicationRenderer,
1010
)
11+
from ....support.unicode import to_superscript
1112
from ..formulas import Formula, FormulaWithSubstitution
1213
from ..instantiation import (
1314
FormalLogicSchemaInstantiation,
@@ -204,11 +205,11 @@ def get_assumption_map(self) -> Mapping[Marker, Formula]:
204205

205206
def get_marker_context(self) -> Iterable[Marker]:
206207
return sorted(
207-
(marker for marker, formula in self._filter_assumptions(discharged_at_current_step=True)),
208+
{marker for marker, formula in self._filter_assumptions(discharged_at_current_step=True)},
208209
key=str
209210
)
210211

211-
def _iter_free_eigenvariables(self) -> Iterable[Eigenvariable]:
212+
def _iter_dischargeable_eigenvariables(self) -> Iterable[Eigenvariable]:
212213
for rule_premise, application_premise in zip(self.rule.premises, self.premises, strict=True):
213214
free = application_premise.tree.get_free_variables()
214215

@@ -219,7 +220,7 @@ def _iter_free_eigenvariables(self) -> Iterable[Eigenvariable]:
219220
yield eigen
220221

221222
def get_eigenvariable_context(self) -> Iterable[Eigenvariable]:
222-
return sorted(set(self._iter_free_eigenvariables()), key=str)
223+
return sorted(set(self._iter_dischargeable_eigenvariables()), key=str)
223224

224225
@override
225226
def build_renderer(self, *, conclusion: FormulaWithSubstitution | None = None) -> RuleApplicationRenderer:
@@ -233,7 +234,7 @@ def build_renderer(self, *, conclusion: FormulaWithSubstitution | None = None) -
233234

234235
return RuleApplicationRenderer(
235236
line,
236-
[str(marker) for marker in self.get_marker_context()] + [eigen.with_star() for eigen in self.get_eigenvariable_context()],
237+
[str(marker) for marker in self.get_marker_context()],
237238
self.rule.name,
238239
[premise.build_renderer() for premise in self.premises]
239240
)
@@ -281,7 +282,7 @@ def apply( # noqa: C901
281282
# Check if there is an eigenvariable in the main formula
282283
if eigen := get_main_eigenvariable(rule_premise, application_premise):
283284
if eigen.is_renamed() and eigen.var in get_free_variables(eigen.formula):
284-
raise RuleApplicationError(f'The renamed eigenvariable {eigen.get_sub()} of the premise {eigen.formula} cannot be free in it')
285+
raise RuleApplicationError(f'The renamed eigenvariable {eigen.get_sub()} of the premise conclusion {eigen.formula} cannot be free in it')
285286

286287
if eigen.var in application_premise.tree.get_free_variables():
287288
raise RuleApplicationError(f'The eigenvariable {eigen} cannot be free in the derivation of {application_premise.tree.conclusion}')
@@ -293,13 +294,16 @@ def apply( # noqa: C901
293294
# Check if there is an eigenvariable in the discharge formula
294295
if eigen := get_discharge_eigenvariable(rule_premise, application_premise):
295296
if eigen.is_renamed() and eigen.var in get_free_variables(eigen.formula):
296-
raise RuleApplicationError(f'The renamed discharge formula eigenvariable {eigen} cannot be free in {eigen.formula}')
297+
raise RuleApplicationError(f'The renamed eigenvariable {eigen.get_sub()} of the dischargeable formula {eigen.formula} cannot be free in it')
297298

298-
if eigen in application_premise.tree.get_free_variables():
299-
raise RuleApplicationError(f'The eigenvariable {eigen} for the discharge formula {application_premise.discharge} cannot be free in it')
299+
if any(mvar.var == eigen.var and mvar.marker != application_premise.marker for mvar in application_premise.tree.get_marked_free_variables()):
300+
if application_premise.marker:
301+
raise RuleApplicationError(f'The eigenvariable {eigen} cannot be free in the derivation of {application_premise.tree.conclusion}, except possibly in [{application_premise.discharge}]{to_superscript(str(application_premise.marker))}')
300302

301-
if eigen in get_free_variables(evaluate_substitution_spec(application_premise.tree.conclusion)):
302-
raise RuleApplicationError(f'The discharge formula eigenvariable {eigen} cannot be free in the conclusion {application_premise.tree.conclusion} of the premise')
303+
raise RuleApplicationError(f'The eigenvariable {eigen} cannot be free in the derivation of {application_premise.tree.conclusion}')
304+
305+
if eigen.var in get_free_variables(evaluate_substitution_spec(application_premise.tree.conclusion)):
306+
raise RuleApplicationError(f'The discharge formula eigenvariable {eigen} cannot be free in the conclusion {application_premise.tree.conclusion} of premise number {i}')
303307

304308
# Update instantiation
305309
instantiation |= infer_instantiation_from_formula_substitution_spec(

‎src/notebook/math/logic/deduction/test_proof_tree.py‎

Lines changed: 126 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,7 @@ def test_efq() -> None:
117117
)
118118

119119

120+
# thm:minimal_implicational_logic_axioms_nd_proof
120121
def test_implication_distributivity_axiom_tree() -> None:
121122
tree = apply(
122123
CLASSICAL_NATURAL_DEDUCTION_SYSTEM['→₊'],
@@ -170,6 +171,29 @@ def test_implication_distributivity_axiom_tree() -> None:
170171
)
171172

172173

174+
# inf:thm:propositional_admissible_rules/self_biconditional
175+
def test_self_biconditional() -> None:
176+
premise = prop_premise(
177+
marker='u',
178+
discharge='p',
179+
tree=prop_assume('p', 'u')
180+
)
181+
182+
tree = apply(
183+
CLASSICAL_NATURAL_DEDUCTION_SYSTEM['↔₊'],
184+
premise,
185+
premise
186+
)
187+
188+
assert str_assumptions(tree) == {}
189+
assert str(tree) == dedent('''\
190+
[p]ᵘ [p]ᵘ
191+
u ____________ ↔₊
192+
(p ↔ p)
193+
'''
194+
)
195+
196+
173197
def test_invalid_application_arity() -> None:
174198
with pytest.raises(RuleApplicationError, match='The rule ∧₊ has 2 premises, but the application has 1'):
175199
apply(
@@ -380,7 +404,7 @@ def test_forall_negation(dummy_signature: FormalLogicSignature) -> None:
380404

381405

382406
def test_forall_introduction_eigenvariable_failure_free_in_self(dummy_signature: FormalLogicSignature) -> None:
383-
with pytest.raises(RuleApplicationError, match=re.escape('The renamed eigenvariable x ↦ y of the premise p₂(x, y) cannot be free in it')):
407+
with pytest.raises(RuleApplicationError, match=re.escape('The renamed eigenvariable x ↦ y of the premise conclusion p₂(x, y) cannot be free in it')):
384408
apply(
385409
CLASSICAL_NATURAL_DEDUCTION_SYSTEM['∀₊'],
386410
premise(
@@ -409,7 +433,7 @@ def test_forall_introduction_eigenvariable_failure_free_in_derivation(dummy_sign
409433

410434
def test_exists_elimination(dummy_signature: FormalLogicSignature) -> None:
411435
u = parse_formula('∃x.p₁(x)', dummy_signature)
412-
v = parse_formula('(p₁(y) → q₁(f₀))', dummy_signature)
436+
v = parse_formula('∀y.(p₁(y) → q₁(f₀))', dummy_signature)
413437
w = parse_formula('p₁(y)', dummy_signature)
414438

415439
tree = apply(
@@ -418,20 +442,113 @@ def test_exists_elimination(dummy_signature: FormalLogicSignature) -> None:
418442
premise(
419443
tree=apply(
420444
CLASSICAL_NATURAL_DEDUCTION_SYSTEM['→₋'],
421-
assume(v, parse_marker('v')),
445+
apply(
446+
CLASSICAL_NATURAL_DEDUCTION_SYSTEM['∀₋'],
447+
assume(v, parse_marker('v')),
448+
conclusion_sub=parse_term_substitution_spec('y ↦ y')
449+
),
422450
assume(w, parse_marker('w')), # We avoid discharging w here
423451
),
424452
discharge=parse_formula_with_substitution('p₁(x)[x ↦ y]', dummy_signature), # So that we can discharge it here
425453
marker=parse_marker('w')
426454
),
427455
)
428456

429-
assert str_free_variables(tree) == set()
430457
assert str(tree) == dedent('''\
431-
[(p₁(y) → q₁(f₀))]ᵛ [p₁(y)]ʷ
432-
_______________________________ →₋
433-
[∃x.p₁(x)]ᵘ q₁(f₀)
434-
w, y* ______________________________________________ ∃₋
435-
q₁(f₀)
458+
[∀y.(p₁(y) → q₁(f₀))]ᵛ
459+
______________________ ∀₋
460+
(p₁(y) → q₁(f₀)) [p₁(y)]ʷ
461+
_____________________________________ →₋
462+
[∃x.p₁(x)]ᵘ q₁(f₀)
463+
w ____________________________________________________ ∃₋
464+
q₁(f₀)
436465
'''
437466
)
467+
468+
469+
def test_simple_invalid_exists_elimination(dummy_signature: FormalLogicSignature) -> None:
470+
u = parse_formula('∃x.p₁(x)', dummy_signature)
471+
v = parse_formula('p₁(y)', dummy_signature)
472+
473+
# If not for its invalidity, the tree would look as follows:
474+
#
475+
# [∃x.p₁(x)]ᵘ [p₁(y)]ᵛ
476+
# v _______________________ ∃₋
477+
# p₁(y)
478+
479+
with pytest.raises(RuleApplicationError, match=re.escape('The discharge formula eigenvariable y cannot be free in the conclusion p₁(y) of premise number 2')):
480+
apply(
481+
CLASSICAL_NATURAL_DEDUCTION_SYSTEM['∃₋'],
482+
assume(u, parse_marker('u')),
483+
premise(
484+
tree=assume(v, parse_marker('v')),
485+
discharge=parse_formula_with_substitution('p₁(x)[x ↦ y]', dummy_signature), # So that we can discharge it here
486+
marker=parse_marker('v')
487+
),
488+
)
489+
490+
491+
def test_invalid_exists_elimination_with_leftover_variable(dummy_signature: FormalLogicSignature) -> None:
492+
# A variation of test_exists_elimination with the constant f₀ replaced by the variable y
493+
u = parse_formula('∃x.p₁(x)', dummy_signature)
494+
v = parse_formula('∀y.(p₁(y) → q₁(y))', dummy_signature)
495+
w = parse_formula('p₁(y)', dummy_signature)
496+
497+
# If not for its invalidity, the tree would look as follows:
498+
#
499+
# [∀y.(p₁(y) → q₁(y))]ᵛ
500+
# _____________________ ∀₋
501+
# (p₁(y) → q₁(y)) [p₁(y)]ʷ
502+
# ____________________________________ →₋
503+
# [∃x.p₁(x)]ᵘ q₁(y)
504+
# w ___________________________________________________ ∃₋
505+
# q₁(y)
506+
507+
with pytest.raises(RuleApplicationError, match=re.escape('The discharge formula eigenvariable y cannot be free in the conclusion q₁(y) of premise number 2')):
508+
apply(
509+
CLASSICAL_NATURAL_DEDUCTION_SYSTEM['∃₋'],
510+
assume(u, parse_marker('u')),
511+
premise(
512+
tree=apply(
513+
CLASSICAL_NATURAL_DEDUCTION_SYSTEM['→₋'],
514+
apply(
515+
CLASSICAL_NATURAL_DEDUCTION_SYSTEM['∀₋'],
516+
assume(v, parse_marker('v')),
517+
conclusion_sub=parse_term_substitution_spec('y ↦ y')
518+
),
519+
assume(w, parse_marker('w')), # We avoid discharging w here
520+
),
521+
discharge=parse_formula_with_substitution('p₁(x)[x ↦ y]', dummy_signature), # So that we can discharge it here
522+
marker=parse_marker('w')
523+
),
524+
)
525+
526+
527+
def test_invalid_exists_elimination_with_imprecise_quantification(dummy_signature: FormalLogicSignature) -> None:
528+
# A variation of test_exists_elimination without universal quantification
529+
u = parse_formula('∃x.p₁(x)', dummy_signature)
530+
v = parse_formula('(p₁(y) → q₁(f₀))', dummy_signature)
531+
w = parse_formula('p₁(y)', dummy_signature)
532+
533+
# If not for its invalidity, the tree would look as follows:
534+
#
535+
# [(p₁(y) → q₁(f₀))]ᵛ [p₁(y)]ʷ
536+
# _______________________________ →₋
537+
# [∃x.p₁(x)]ᵘ q₁(f₀)
538+
# w ______________________________________________ ∃₋
539+
# q₁(f₀)
540+
541+
with pytest.raises(RuleApplicationError, match=re.escape('The eigenvariable y cannot be free in the derivation of q₁(f₀), except possibly in [p₁(x)[x ↦ y]]ʷ')):
542+
apply(
543+
CLASSICAL_NATURAL_DEDUCTION_SYSTEM['∃₋'],
544+
assume(u, parse_marker('u')),
545+
premise(
546+
tree=apply(
547+
CLASSICAL_NATURAL_DEDUCTION_SYSTEM['→₋'],
548+
assume(v, parse_marker('v')),
549+
assume(w, parse_marker('w')), # We avoid discharging w here
550+
),
551+
discharge=parse_formula_with_substitution('p₁(x)[x ↦ y]', dummy_signature), # So that we can discharge it here
552+
marker=parse_marker('w')
553+
),
554+
)

‎src/notebook/math/logic/substitution/__init__.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
1-
from .formula_visitor import evaluate_substitution_spec, substitute_in_formula
1+
from .formula_visitor import evaluate_substitution_spec, substitute_in_formula, unwrap_substitution_spec
22
from .term_visitor import substitute_in_term

‎src/notebook/math/logic/substitution/formula_visitor.py‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,3 +59,10 @@ def evaluate_substitution_spec(spec: FormulaWithSubstitution) -> Formula:
5959
return spec.formula
6060

6161
return substitute_in_formula(spec.formula, spec.sub.src, spec.sub.dest)
62+
63+
64+
def unwrap_substitution_spec(spec: FormulaWithSubstitution) -> Formula:
65+
if spec.sub is None:
66+
return spec.formula
67+
68+
return spec.formula

‎text/higher_order_logic.tex‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -618,7 +618,7 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
618618
\begin{itemize}
619619
\item Its type context \( T_P \) is the implicit context of \( \varphi \).
620620
\item Its free variable set \( F_P \) is the set of free variables of \( \varphi \):
621-
\begin{equation}\label{eq:def:hol_natural_deduction_proof_tree/assumption/eigenvariables}
621+
\begin{equation}\label{eq:def:hol_natural_deduction_proof_tree/assumption/free_variables}
622622
F_P \coloneqq \op*{Free}(\varphi).
623623
\end{equation}
624624
\end{itemize}
@@ -627,7 +627,7 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
627627
\begin{itemize}
628628
\item Its type context \( T_P \) is the union of the contexts \( T_{P_1}, \ldots, T_{P_n} \) of the premises.
629629
\item Its free variable set \( F_P \) is more complicated:
630-
\begin{equation}\label{eq:def:hol_natural_deduction_proof_tree/application/eigenvariables}
630+
\begin{equation}\label{eq:def:hol_natural_deduction_proof_tree/application/free_variables}
631631
F_P \coloneqq \bigcup_{i=1}^n \set{ (v: m) \in F_{P_i} \given m \not\in D \T{and} v \not\in E },
632632
\end{equation}
633633
where
@@ -645,7 +645,7 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
645645
\end{thmenum}
646646
\end{definition}
647647
\begin{comments}
648-
\item The details of how we define the set of free variables is based on the analogous considerations for first-order logic from \cite[37]{TroelstraSchwichtenberg2000BasicProofTheory}.
648+
\item The details of how we define the set of free variables is based on the analogous considerations for first-order logic from \cite[37]{TroelstraSchwichtenberg2000BasicProofTheory}, also implemented programmatically in the module \identifier{math.logic.deduction.proof_tree} in \cite{notebook:code}.
649649

650650
The type context is only here for compatibility with our peculiar definition of logical formulas.
651651
\end{comments}

0 commit comments

Comments
 (0)