disjunctive-syllogism-1 (python sample)

Tags: disjunctive-syllogism-1 python sample

Usage

Call the infer_statement method from the inference-rule inclusion class listed in the i (unabridged inference_rules ) property of the theory-derivation :

u = pu.create_universe()
t = u.t()
...
# some theory elaboration code
...
t.i.disjunctive_syllogism_1.infer_statement(...)

Sample code

Code output

𝖫𝖾𝗍 ⌜𝒰₃₀⌝ 𝖻𝖾 𝖺 𝑢𝑛𝑖𝑣𝑒𝑟𝑠𝑒-𝑜𝑓-𝑑𝑖𝑠𝑐𝑜𝑢𝑟𝑠𝑒.

𝖫𝖾𝗍 ⌜𝒯₁⌝ 𝖻𝖾 𝖺 𝑡ℎ𝑒𝑜𝑟𝑦-𝑑𝑒𝑟𝑖𝑣𝑎𝑡𝑖𝑜𝑛 𝗂𝗇 𝒰₃₀.

𝗔𝘅𝗶𝗼𝗺 (𝒯₁.𝐴₁): 𝖫𝖾𝗍 𝑎𝑥𝑖𝑜𝑚 𝒜₁ ⌜𝘋𝘶𝘮𝘮𝘺 𝘢𝘹𝘪𝘰𝘮 𝘧𝘰𝘳 𝘥𝘦𝘮𝘰𝘯𝘴𝘵𝘳𝘢𝘵𝘪𝘰𝘯 𝘱𝘶𝘳𝘱𝘰𝘴𝘦𝘴⌝ 𝖻𝖾 𝗂𝗇𝖼𝗅𝗎𝖽𝖾𝖽 (𝗉𝗈𝗌𝗍𝗎𝗅𝖺𝗍𝖾𝖽) 𝗂𝗇 𝒯₁.

𝗜𝗻𝗳𝗲𝗿𝗲𝗻𝗰𝗲 𝗿𝘂𝗹𝗲 (𝑎𝑥𝑖𝑜𝑚-𝑖𝑛𝑡𝑒𝑟𝑝𝑟𝑒𝑡𝑎𝑡𝑖𝑜𝑛): 𝖫𝖾𝗍 𝑖𝑛𝑓𝑒𝑟𝑒𝑛𝑐𝑒-𝑟𝑢𝑙𝑒 𝑎𝑥𝑖𝑜𝑚-𝑖𝑛𝑡𝑒𝑟𝑝𝑟𝑒𝑡𝑎𝑡𝑖𝑜𝑛 𝖽𝖾𝖿𝗂𝗇𝖾𝖽 𝖺𝗌 ⌜(𝓐, 𝐏 ⊢ 𝐏)⌝ 𝖻𝖾 𝗂𝗇𝖼𝗅𝗎𝖽𝖾𝖽 𝖺𝗇𝖽 𝖼𝗈𝗇𝗌𝗂𝖽𝖾𝗋𝖾𝖽 𝗏𝖺𝗅𝗂𝖽 𝗂𝗇 𝒯₁.

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (𝒯₁.𝑃₁): ((𝑜₁ ⟹ 𝑜₃) ∨ (𝑜₁ ⟹ 𝑜₄)). 𝗣𝗿𝗼𝗼𝗳: ⌜𝘋𝘶𝘮𝘮𝘺 𝘢𝘹𝘪𝘰𝘮 𝘧𝘰𝘳 𝘥𝘦𝘮𝘰𝘯𝘴𝘵𝘳𝘢𝘵𝘪𝘰𝘯 𝘱𝘶𝘳𝘱𝘰𝘴𝘦𝘴⌝ 𝗂𝗌 𝗉𝗈𝗌𝗍𝗎𝗅𝖺𝗍𝖾𝖽 𝖻𝗒 𝗮𝘅𝗶𝗼𝗺 (𝐴₁). ((𝑜₁ ⟹ 𝑜₃) ∨ (𝑜₁ ⟹ 𝑜₄)) 𝗂𝗌 𝖺 𝗉𝗋𝗈𝗉𝗈𝗌𝗂𝗍𝗂𝗈𝗇𝖺𝗅 𝖿𝗈𝗋𝗆𝗎𝗅𝖺 𝗂𝗇𝗍𝖾𝗋𝗉𝗋𝖾𝗍𝖾𝖽 𝖿𝗋𝗈𝗆 𝗍𝗁𝖺𝗍 𝖺𝗑𝗂𝗈𝗆. 𝖳𝗁𝖾𝗋𝖾𝖿𝗈𝗋𝖾, 𝖻𝗒 𝗍𝗁𝖾 𝑎𝑥𝑖𝑜𝑚-𝑖𝑛𝑡𝑒𝑟𝑝𝑟𝑒𝑡𝑎𝑡𝑖𝑜𝑛 𝗂𝗇𝖿𝖾𝗋𝖾𝗇𝖼𝖾 𝗋𝗎𝗅𝖾: (𝓐, 𝐏 ⊢ 𝐏), 𝗂𝗍 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝗍𝗁𝖺𝗍 ((𝑜₁ ⟹ 𝑜₃) ∨ (𝑜₁ ⟹ 𝑜₄)). ∎

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (𝒯₁.𝑃₂): ¬((𝑜₁ ⟹ 𝑜₃)). 𝗣𝗿𝗼𝗼𝗳: ⌜𝘋𝘶𝘮𝘮𝘺 𝘢𝘹𝘪𝘰𝘮 𝘧𝘰𝘳 𝘥𝘦𝘮𝘰𝘯𝘴𝘵𝘳𝘢𝘵𝘪𝘰𝘯 𝘱𝘶𝘳𝘱𝘰𝘴𝘦𝘴⌝ 𝗂𝗌 𝗉𝗈𝗌𝗍𝗎𝗅𝖺𝗍𝖾𝖽 𝖻𝗒 𝗮𝘅𝗶𝗼𝗺 (𝐴₁). ¬((𝑜₁ ⟹ 𝑜₃)) 𝗂𝗌 𝖺 𝗉𝗋𝗈𝗉𝗈𝗌𝗂𝗍𝗂𝗈𝗇𝖺𝗅 𝖿𝗈𝗋𝗆𝗎𝗅𝖺 𝗂𝗇𝗍𝖾𝗋𝗉𝗋𝖾𝗍𝖾𝖽 𝖿𝗋𝗈𝗆 𝗍𝗁𝖺𝗍 𝖺𝗑𝗂𝗈𝗆. 𝖳𝗁𝖾𝗋𝖾𝖿𝗈𝗋𝖾, 𝖻𝗒 𝗍𝗁𝖾 𝑎𝑥𝑖𝑜𝑚-𝑖𝑛𝑡𝑒𝑟𝑝𝑟𝑒𝑡𝑎𝑡𝑖𝑜𝑛 𝗂𝗇𝖿𝖾𝗋𝖾𝗇𝖼𝖾 𝗋𝗎𝗅𝖾: (𝓐, 𝐏 ⊢ 𝐏), 𝗂𝗍 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝗍𝗁𝖺𝗍 ¬((𝑜₁ ⟹ 𝑜₃)). ∎

𝗜𝗻𝗳𝗲𝗿𝗲𝗻𝗰𝗲 𝗿𝘂𝗹𝗲 (𝑑𝑖𝑠𝑗𝑢𝑛𝑐𝑡𝑖𝑣𝑒-𝑠𝑦𝑙𝑙𝑜𝑔𝑖𝑠𝑚-1): 𝖫𝖾𝗍 𝑖𝑛𝑓𝑒𝑟𝑒𝑛𝑐𝑒-𝑟𝑢𝑙𝑒 𝑑𝑖𝑠𝑗𝑢𝑛𝑐𝑡𝑖𝑣𝑒-𝑠𝑦𝑙𝑙𝑜𝑔𝑖𝑠𝑚-1 𝖽𝖾𝖿𝗂𝗇𝖾𝖽 𝖺𝗌 ⌜((𝐏₁ ∨ 𝐐₁), ¬(𝐏₁) ⊢ 𝐐₁)⌝ 𝖻𝖾 𝗂𝗇𝖼𝗅𝗎𝖽𝖾𝖽 𝖺𝗇𝖽 𝖼𝗈𝗇𝗌𝗂𝖽𝖾𝗋𝖾𝖽 𝗏𝖺𝗅𝗂𝖽 𝗂𝗇 𝒯₁.

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (𝒯₁.𝑃₃) - The proposition of interest: (𝑜₁ ⟹ 𝑜₄). 𝗣𝗿𝗼𝗼𝗳: ((𝑜₁ ⟹ 𝑜₃) ∨ (𝑜₁ ⟹ 𝑜₄)), 𝗈𝖿 𝗍𝗁𝖾 𝖿𝗈𝗋𝗆 (𝐏₁ ∨ 𝐐₁), 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝖿𝗋𝗈𝗆 𝗽𝗿𝗼𝗽. (𝑃₁). 𝑃₂, 𝗈𝖿 𝗍𝗁𝖾 𝖿𝗈𝗋𝗆 ¬(𝐏₁), 𝗂𝗌 𝗀𝗂𝗏𝖾𝗇.  𝖳𝗁𝖾𝗋𝖾𝖿𝗈𝗋𝖾, 𝖻𝗒 𝗍𝗁𝖾 𝑑𝑖𝑠𝑗𝑢𝑛𝑐𝑡𝑖𝑣𝑒-𝑠𝑦𝑙𝑙𝑜𝑔𝑖𝑠𝑚-1 𝗂𝗇𝖿𝖾𝗋𝖾𝗇𝖼𝖾 𝗋𝗎𝗅𝖾: ((𝐏₁ ∨ 𝐐₁), ¬(𝐏₁) ⊢ 𝐐₁), 𝗂𝗍 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝗍𝗁𝖺𝗍 (𝑜₁ ⟹ 𝑜₄). ∎

import punctilious as pu

# Create a universe-of-discourse with basic objects for the sake of this example.
u = pu.UniverseOfDiscourse(echo=True)
o1 = u.o.declare()
o2 = u.o.declare()
o3 = u.o.declare()
o4 = u.o.declare()
axiom = u.a.declare(natural_language='Dummy axiom for demonstration purposes')

# Elaborate a dummy theory with a set of propositions necessary for our demonstration
t1 = u.t(echo=True)
theory_axiom = t1.include_axiom(a=axiom)
phi1 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
    p=(o1 | u.r.implies | o3) | u.r.lor | (o1 | u.r.implies | o4), lock=False)
phi2 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
    p=u.r.lnot((o1 | u.r.implies | o3)), lock=True)

# And finally, use the conjunction-introduction inference-rule:
proposition_of_interest = t1.i.disjunctive_syllogism_1.infer_formula_statement(p_or_q=phi1,
    not_p=phi2, subtitle='The proposition of interest')

Let "U29" be a universe-of-discourse.

Let "T1" be a theory-derivation in U29.

Axiom (T1.A1): Let axiom A1 "Dummy axiom for demonstration purposes" be included (postulated) in T1.

Inference rule (axiom-interpretation): Let inference-rule axiom-interpretation defined as "(A, P |- P)" be included and considered valid in T1.

Proposition (T1.P1): ((o1 ==> o3) or (o1 ==> o4)). Proof: "Dummy axiom for demonstration purposes" is postulated by axiom (A1). ((o1 ==> o3) or (o1 ==> o4)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that ((o1 ==> o3) or (o1 ==> o4)). QED

Proposition (T1.P2): not((o1 ==> o3)). Proof: "Dummy axiom for demonstration purposes" is postulated by axiom (A1). not((o1 ==> o3)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that not((o1 ==> o3)). QED

Inference rule (disjunctive-syllogism-1): Let inference-rule disjunctive-syllogism-1 defined as "((P1 or Q1), not(P1) |- Q1)" be included and considered valid in T1.

Proposition (T1.P3) - The proposition of interest: (o1 ==> o4). Proof: ((o1 ==> o3) or (o1 ==> o4)), of the form (P1 or Q1), follows from prop. (P1). P2, of the form not(P1), is given.  Therefore, by the disjunctive-syllogism-1 inference rule: ((P1 or Q1), not(P1) |- Q1), it follows that (o1 ==> o4). QED