Skip to content

Commit

Permalink
version 2.0: re-starting from scratch with a new data model.
Browse files Browse the repository at this point in the history
  • Loading branch information
@daviddoret
daviddoret committed Jul 21, 2024
1 parent 689b8d1 commit 9caa68d
Show file tree
Hide file tree
Showing 5 changed files with 88 additions and 93 deletions.
23 changes: 9 additions & 14 deletions .idea/workspace.xml
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

28 changes: 14 additions & 14 deletions src/punctilious/minimal_logic_1.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -375,21 +375,21 @@ def extend_theory_with_mancosu_2021_page_20(t: as1.FlexibleTheory) -> as1.Theory
i=pls1.i5, t=t, raise_error_if_false=True)
t, success, _, = as1.derive_2(c=is_a_proposition(p2 | lor | p1),
i=pls1.i5, t=t, raise_error_if_false=True)
t, success, _, = as1.derive_2(c=(p2 | land | p2) | is_a | is_a_proposition,
t, success, _, = as1.derive_2(c=is_a_proposition(p2 | land | p2),
i=pls1.i3, t=t, raise_error_if_false=True)
t, success, _, = as1.derive_2(c=(p1 | land | p2) | is_a | is_a_proposition,
t, success, _, = as1.derive_2(c=is_a_proposition(p1 | land | p2),
i=pls1.i3, t=t, raise_error_if_false=True)
t, success, _, = as1.derive_2(c=((p2 | land | p2) | implies | (p1 | land | p2)) | is_a | is_a_proposition,
t, success, _, = as1.derive_2(c=is_a_proposition((p2 | land | p2) | implies | (p1 | land | p2)),
i=pls1.i4, t=t, raise_error_if_false=True)
t, success, _, = as1.derive_2(c=((p1 | lor | p2) | implies | (p2 | lor | p1)) | is_a | is_a_proposition,
t, success, _, = as1.derive_2(c=is_a_proposition((p1 | lor | p2) | implies | (p2 | lor | p1)),
i=pls1.i4, t=t, raise_error_if_false=True)
t, success, _, = as1.derive_2(
c=(p1 | implies | (p1 | lor | p2)) | is_a | is_a_proposition,
c=is_a_proposition(p1 | implies | (p1 | lor | p2)),
i=pls1.i4, t=t)
t, success, _, = as1.derive_2(
c=(((p1 | lor | p2) | implies | (p2 | lor | p1)) |
implies |
(p1 | implies | (p1 | lor | p2))) | is_a | is_a_proposition,
c=is_a_proposition(((p1 | lor | p2) | implies | (p2 | lor | p1)) |
implies |
(p1 | implies | (p1 | lor | p2))),
i=pls1.i4, t=t)

# 1. ⊢ 𝑝1 ⊃ (𝑝1 ∨ 𝑝2) (axiom PL7)
Expand Down Expand Up @@ -441,17 +441,17 @@ def extend_theory_with_mancosu_2021_page_21(t: as1.FlexibleTheory) -> as1.Theory
t, d = pls1.let_x_be_a_propositional_variable(t=t, formula_ts='D')
t, success, _ = as1.derive_2(c=is_a_proposition(c),
i=pls1.i1, t=t)
t, success, _ = as1.derive_2(c=d | is_a | is_a_proposition,
t, success, _ = as1.derive_2(c=is_a_proposition(d),
i=pls1.i1, t=t)
t, success, _ = as1.derive_2(c=(c | implies | d) | is_a | is_a_proposition,
t, success, _ = as1.derive_2(c=is_a_proposition(c | implies | d),
i=pls1.i4, t=t)
t, success, _ = as1.derive_2(c=(d | implies | c) | is_a | is_a_proposition,
t, success, _ = as1.derive_2(c=is_a_proposition(d | implies | c),
i=pls1.i4, t=t)
t, success, _ = as1.derive_2(c=(d | land | d) | is_a | is_a_proposition,
t, success, _ = as1.derive_2(c=is_a_proposition(d | land | d),
i=pls1.i3, t=t)
t, success, _ = as1.derive_2(c=(c | land | d) | is_a | is_a_proposition,
t, success, _ = as1.derive_2(c=is_a_proposition(c | land | d),
i=pls1.i3, t=t)
t, success, _ = as1.derive_2(c=((d | land | d) | implies | (c | land | d)) | is_a | is_a_proposition,
t, success, _ = as1.derive_2(c=is_a_proposition((d | land | d) | implies | (c | land | d)),
i=pls1.i4, t=t)
# 1. ⊢ 𝐶(hypothesis)
# TODO: Implement this as a proper hypothesis
Expand Down
40 changes: 20 additions & 20 deletions src/punctilious/propositional_logic_syntax_1.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@
i2: as1.InferenceRule = as1.InferenceRule(
t=as1.NaturalTransformation(
p=(is_a_proposition(a),),
c=lnot(a) | is_a | is_a_proposition,
c=is_a_proposition(lnot(a)),
v=(a,)),
ref_ts=pl1.Monospace(text='PLS2'))
"""Axiom schema: A is-a proposition ⊃ ¬A is a proposition.
Expand All @@ -111,7 +111,7 @@
t=as1.NaturalTransformation(
p=(is_a_proposition(a),
is_a_proposition(b)),
c=(a | land | b) | is_a | is_a_proposition,
c=is_a_proposition(a | land | b),
v=(a, b,)),
ref_ts=pl1.Monospace(text='PLS3'))
"""Axiom schema: (A is-a proposition, B is-a proposition) ⊃ ((A ∧ B) is a proposition).
Expand All @@ -136,7 +136,7 @@
t=as1.NaturalTransformation(
p=(is_a_proposition(a),
is_a_proposition(b)),
c=(a | implies | b) | is_a | is_a_proposition,
c=is_a_proposition(a | implies | b),
v=(a, b,)),
ref_ts=pl1.Monospace(text='PLS4'))
"""Axiom schema: (A is-a proposition, B is-a proposition) ⊃ ((A ⊃ B) is a proposition).
Expand All @@ -161,7 +161,7 @@
t=as1.NaturalTransformation(
p=(is_a_proposition(a),
is_a_proposition(b)),
c=(a | lor | b) | is_a | is_a_proposition,
c=is_a_proposition(a | lor | b),
v=(a, b,)),
ref_ts=pl1.Monospace(text='PLS5'))
"""Axiom schema: (A is-a proposition, B is-a proposition) ⊃ ((A ∨ B) is a proposition).
Expand Down Expand Up @@ -340,7 +340,7 @@ def process_conjecture(self, conjecture: as1.FlexibleFormula, t: as1.FlexibleThe
# If P is a propositional-variable:
# We can safely derive proposition(p)
t, _ = as1.derive_1(
c=p_value | is_a | is_a_proposition,
c=is_a_proposition(p_value),
p=(is_a_propositional_variable(p_value),),
i=i1, t=t)

Expand All @@ -358,9 +358,9 @@ def process_conjecture(self, conjecture: as1.FlexibleFormula, t: as1.FlexibleThe
# (Q is-a proposition) is proved.
# We can safely derive ((¬Q) is-a proposition).
t, _ = as1.derive_1(
c=lnot(q_value) | is_a | is_a_proposition,
c=is_a_proposition(lnot(q_value)),
p=(
q_value | is_a | is_a_proposition,),
is_a_proposition(q_value),),
i=i2, t=t)
return t, True
else:
Expand All @@ -385,10 +385,10 @@ def process_conjecture(self, conjecture: as1.FlexibleFormula, t: as1.FlexibleThe
# (R is-a proposition) is proved.
# We can safely derive ((Q ∧ R) is-a proposition).
t, _ = as1.derive_1(
c=(q_value | land | r_value) | is_a | is_a_proposition,
c=is_a_proposition(q_value | land | r_value),
p=(
q_value | is_a | is_a_proposition,
r_value | is_a | is_a_proposition,),
is_a_proposition(q_value),
is_a_proposition(r_value),),
i=i3, t=t)
return t, True
else:
Expand All @@ -408,18 +408,18 @@ def process_conjecture(self, conjecture: as1.FlexibleFormula, t: as1.FlexibleThe
q_value: as1.Formula = as1.get_image_from_map(m=m, preimage=q)
r_value: as1.Formula = as1.get_image_from_map(m=m, preimage=r)
# Recursively try to derive (Q is-a proposition).
t, success = self.process_conjecture(conjecture=q_value | is_a | is_a_proposition, t=t)
t, success = self.process_conjecture(conjecture=is_a_proposition(q_value), t=t)
if success:
# (Q is-a proposition) is proved.
t, success = self.process_conjecture(conjecture=r_value | is_a | is_a_proposition, t=t)
t, success = self.process_conjecture(conjecture=is_a_proposition(r_value), t=t)
if success:
# (R is-a proposition) is proved.
# We can safely derive ((Q ⊃ R) is-a proposition).
t, _ = as1.derive_1(
c=(q_value | implies | r_value) | is_a | is_a_proposition,
c=is_a_proposition(q_value | implies | r_value),
p=(
q_value | is_a | is_a_proposition,
r_value | is_a | is_a_proposition,),
is_a_proposition(q_value),
is_a_proposition(r_value),),
i=i4, t=t)
return t, True
else:
Expand All @@ -439,18 +439,18 @@ def process_conjecture(self, conjecture: as1.FlexibleFormula, t: as1.FlexibleThe
q_value: as1.Formula = as1.get_image_from_map(m=m, preimage=q)
r_value: as1.Formula = as1.get_image_from_map(m=m, preimage=r)
# Recursively try to derive (Q is-a proposition).
t, success = self.process_conjecture(conjecture=q_value | is_a | is_a_proposition, t=t)
t, success = self.process_conjecture(conjecture=is_a_proposition(q_value), t=t)
if success:
# (Q is-a proposition) is proved.
t, success = self.process_conjecture(conjecture=r_value | is_a | is_a_proposition, t=t)
t, success = self.process_conjecture(conjecture=is_a_proposition(r_value), t=t)
if success:
# (R is-a proposition) is proved.
# We can safely derive ((Q ∨ R) is-a proposition).
t, _ = as1.derive_1(
c=(q_value | lor | r_value) | is_a | is_a_proposition,
c=is_a_proposition(q_value | lor | r_value),
p=(
q_value | is_a | is_a_proposition,
r_value | is_a | is_a_proposition,),
is_a_proposition(q_value),
is_a_proposition(r_value),),
i=i5, t=t)
return t, True
else:
Expand Down
Loading

0 comments on commit 9caa68d

Please sign in to comment.