proof-by-contradiction-2 (python sample)

Tags: proof-by-contradiction-2 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 derivation code
...
t.i.proof_by_contradiction_2.infer_statement(...)

Sample code

Code output

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

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

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

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

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (𝒯₁.𝑃₁): (𝑓(𝑜₁) = 𝑓(𝑜₂)).

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (𝒯₁.𝑃₂): ((𝑓(𝐱₁) = 𝑓(𝐲₁)) ⟹ (𝐱₁ = 𝐲₁)).

𝗔𝘅𝗶𝗼𝗺 (ℋ₁.𝐴₂): 𝖫𝖾𝗍 𝑎𝑥𝑖𝑜𝑚 𝒜₂ ⌜𝘉𝘺 𝘩𝘺𝘱𝘰𝘵𝘩𝘦𝘴𝘪𝘴, 𝘢𝘴𝘴𝘶𝘮𝘦 (𝑜₁ ≠ 𝑜₂) 𝘪𝘴 𝘵𝘳𝘶𝘦.⌝ 𝖻𝖾 𝗂𝗇𝖼𝗅𝗎𝖽𝖾𝖽 (𝗉𝗈𝗌𝗍𝗎𝗅𝖺𝗍𝖾𝖽) 𝗂𝗇 ℋ₁.

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

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (ℋ₁.𝑃₃): (𝑜₁ ≠ 𝑜₂).

𝗛𝘆𝗽𝗼𝘁𝗵𝗲𝘀𝗶𝘀 (𝒯₁.𝐻₁) - We pose the negation hypothesis: (𝑜₁ ≠ 𝑜₂). 𝖳𝗁𝗂𝗌 𝗁𝗒𝗉𝗈𝗍𝗁𝖾𝗌𝗂𝗌 𝗂𝗌 𝖾𝗅𝖺𝖻𝗈𝗋𝖺𝗍𝖾𝖽 𝗂𝗇 𝗍𝗁𝖾𝗈𝗋𝗒 ℋ₁.

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

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (ℋ₁.𝑃₄): ((𝑓(𝑜₁) = 𝑓(𝑜₂)) ⟹ (𝑜₁ = 𝑜₂)).

𝗜𝗻𝗳𝗲𝗿𝗲𝗻𝗰𝗲 𝗿𝘂𝗹𝗲 (𝑚𝑜𝑑𝑢𝑠-𝑝𝑜𝑛𝑒𝑛𝑠): 𝖫𝖾𝗍 𝑖𝑛𝑓𝑒𝑟𝑒𝑛𝑐𝑒-𝑟𝑢𝑙𝑒 𝑚𝑜𝑑𝑢𝑠-𝑝𝑜𝑛𝑒𝑛𝑠 𝖽𝖾𝖿𝗂𝗇𝖾𝖽 𝖺𝗌 ⌜((𝐏₃ ⟹ 𝐐₂), 𝐏₃ ⊢ 𝐐₂)⌝ 𝖻𝖾 𝗂𝗇𝖼𝗅𝗎𝖽𝖾𝖽 𝖺𝗇𝖽 𝖼𝗈𝗇𝗌𝗂𝖽𝖾𝗋𝖾𝖽 𝗏𝖺𝗅𝗂𝖽 𝗂𝗇 ℋ₁.

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (ℋ₁.𝑃₅): (𝑜₁ = 𝑜₂).

𝗜𝗻𝗳𝗲𝗿𝗲𝗻𝗰𝗲 𝗿𝘂𝗹𝗲 (𝑖𝑛𝑐𝑜𝑛𝑠𝑖𝑠𝑡𝑒𝑛𝑐𝑦-𝑖𝑛𝑡𝑟𝑜𝑑𝑢𝑐𝑡𝑖𝑜𝑛-2): 𝖫𝖾𝗍 𝑖𝑛𝑓𝑒𝑟𝑒𝑛𝑐𝑒-𝑟𝑢𝑙𝑒 𝑖𝑛𝑐𝑜𝑛𝑠𝑖𝑠𝑡𝑒𝑛𝑐𝑦-𝑖𝑛𝑡𝑟𝑜𝑑𝑢𝑐𝑡𝑖𝑜𝑛-2 𝖽𝖾𝖿𝗂𝗇𝖾𝖽 𝖺𝗌 ⌜((𝐏₆ = 𝐐₄), (𝐏₆ ≠ 𝐐₄) ⊢ 𝐼𝑛𝑐(𝒯₁))⌝ 𝖻𝖾 𝗂𝗇𝖼𝗅𝗎𝖽𝖾𝖽 𝖺𝗇𝖽 𝖼𝗈𝗇𝗌𝗂𝖽𝖾𝗋𝖾𝖽 𝗏𝖺𝗅𝗂𝖽 𝗂𝗇 𝒯₁.

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (𝒯₁.𝑃₆) - Proof of hypothesis inconsistency: 𝐼𝑛𝑐(ℋ₁). 𝗣𝗿𝗼𝗼𝗳: 𝖫𝖾𝗍 (𝑷 = 𝑸) := (𝑜₁ = 𝑜₂) 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝖿𝗋𝗈𝗆 𝗽𝗿𝗼𝗽. (𝑃₅). 𝖫𝖾𝗍 (𝑷 ≠ 𝑸) := (𝑜₁ ≠ 𝑜₂) 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝖿𝗋𝗈𝗆 𝗽𝗿𝗼𝗽. (𝑃₃).  𝖳𝗁𝖾𝗋𝖾𝖿𝗈𝗋𝖾, 𝖻𝗒 𝗍𝗁𝖾 𝑖𝑛𝑐𝑜𝑛𝑠𝑖𝑠𝑡𝑒𝑛𝑐𝑦-𝑖𝑛𝑡𝑟𝑜𝑑𝑢𝑐𝑡𝑖𝑜𝑛-2 𝗂𝗇𝖿𝖾𝗋𝖾𝗇𝖼𝖾 𝗋𝗎𝗅𝖾: ((𝐏₆ = 𝐐₄), (𝐏₆ ≠ 𝐐₄) ⊢ 𝐼𝑛𝑐(𝒯₁)), 𝗂𝗍 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝗍𝗁𝖺𝗍 𝐼𝑛𝑐(ℋ₁). ∎

𝗜𝗻𝗳𝗲𝗿𝗲𝗻𝗰𝗲 𝗿𝘂𝗹𝗲 (𝑝𝑟𝑜𝑜𝑓-𝑏𝑦-𝑐𝑜𝑛𝑡𝑟𝑎𝑑𝑖𝑐𝑡𝑖𝑜𝑛-2): 𝖫𝖾𝗍 𝑖𝑛𝑓𝑒𝑟𝑒𝑛𝑐𝑒-𝑟𝑢𝑙𝑒 𝑝𝑟𝑜𝑜𝑓-𝑏𝑦-𝑐𝑜𝑛𝑡𝑟𝑎𝑑𝑖𝑐𝑡𝑖𝑜𝑛-2 𝖽𝖾𝖿𝗂𝗇𝖾𝖽 𝖺𝗌 ⌜((𝐇₁ 𝑓𝑜𝑟𝑚𝑢𝑙𝑎𝑡𝑒 (𝐱₄ ≠ 𝐲₄)), 𝐼𝑛𝑐(𝐇₁) ⊢ (𝐱₄ = 𝐲₄))⌝ 𝖻𝖾 𝗂𝗇𝖼𝗅𝗎𝖽𝖾𝖽 𝖺𝗇𝖽 𝖼𝗈𝗇𝗌𝗂𝖽𝖾𝗋𝖾𝖽 𝗏𝖺𝗅𝗂𝖽 𝗂𝗇 𝒯₁.

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (𝒯₁.𝑃₇) - The proposition of interest: (𝑜₁ = 𝑜₂). 𝗣𝗿𝗼𝗼𝗳: 𝖫𝖾𝗍 𝗵𝘆𝗽. (𝐻₁) 𝖻𝖾 𝗍𝗁𝖾 𝗁𝗒𝗉𝗈𝗍𝗁𝖾𝗌𝗂𝗌 (𝑜₁ ≠ 𝑜₂). 𝐼𝑛𝑐(ℋ₁) 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝖿𝗋𝗈𝗆 𝗽𝗿𝗼𝗽. (𝑃₆). 𝖳𝗁𝖾𝗋𝖾𝖿𝗈𝗋𝖾, 𝖻𝗒 𝗍𝗁𝖾 𝑝𝑟𝑜𝑜𝑓-𝑏𝑦-𝑐𝑜𝑛𝑡𝑟𝑎𝑑𝑖𝑐𝑡𝑖𝑜𝑛-2 𝗂𝗇𝖿𝖾𝗋𝖾𝗇𝖼𝖾 𝗋𝗎𝗅𝖾: ((𝐇₁ 𝑓𝑜𝑟𝑚𝑢𝑙𝑎𝑡𝑒 (𝐱₄ ≠ 𝐲₄)), 𝐼𝑛𝑐(𝐇₁) ⊢ (𝐱₄ = 𝐲₄)), 𝗂𝗍 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝗍𝗁𝖺𝗍 (𝑜₁ = 𝑜₂). ∎

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()
f = u.r.declare(arity=1, symbol='f', auto_index=False)
t1 = u.t(echo=True)
axiom = u.a.declare(natural_language='Dummy axiom for demonstration purposes')

# Elaborate a dummy theory with inconsistent propositions
pu.configuration.echo_proof = False
theory_axiom = t1.include_axiom(axiom)
f_o1_eq_f_02 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
    p=f(o1) | u.r.eq | f(o2), lock=False)
with u.with_variable('x') as x, u.with_variable('y') as y:
    implication = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
        p=(f(x) | u.r.eq | f(y)) | u.r.implies | (x | u.r.eq | y), lock=True)
t1.stabilize()

# Pose the inequality hypothesis
h = t1.pose_hypothesis(hypothesis_formula=o1 | u.r.neq | o2,
    subtitle='We pose the negation hypothesis')

# Elaborate on the hypothesis to uncover its inconsistency
substitution = h.child_theory.i.variable_substitution.infer_formula_statement(p=implication,
    phi=u.r.tupl(o1, o2))
equality = h.child_theory.i.modus_ponens.infer_formula_statement(p_implies_q=substitution,
    p=f_o1_eq_f_02)

# Prove hypothesis inconsistency
pu.configuration.echo_proof = True
h_inconsistency = t1.i.inconsistency_introduction_2.infer_formula_statement(x_equal_y=equality,
    x_unequal_y=h.child_statement, t=h.child_theory, subtitle='Proof of hypothesis inconsistency')

# And finally, use the proof-by-contradiction-2 inference-rule:
proposition_of_interest = t1.i.proof_by_contradiction_2.infer_formula_statement(h=h,
    inc_h=h_inconsistency, subtitle='The proposition of interest')

pass

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

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

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): (f(o1) = f(o2)).

Proposition (T1.P2): ((f(x1) = f(y1)) ==> (x1 = y1)).

Axiom (H1.A2): Let axiom A2 "By hypothesis, assume (o1 neq o2) is true." be included (postulated) in H1.

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

Proposition (H1.P3): (o1 neq o2).

Hypothesis (T1.H1) - We pose the negation hypothesis: (o1 neq o2). This hypothesis is elaborated in theory H1.

Inference rule (variable-substitution): Let inference-rule variable-substitution defined as "(P1, O1 |- Q1)" be included and considered valid in H1.

Proposition (H1.P4): ((f(o1) = f(o2)) ==> (o1 = o2)).

Inference rule (modus-ponens): Let inference-rule modus-ponens defined as "((P3 ==> Q2), P3 |- Q2)" be included and considered valid in H1.

Proposition (H1.P5): (o1 = o2).

Inference rule (inconsistency-introduction-2): Let inference-rule inconsistency-introduction-2 defined as "((P6 = Q4), (P6 neq Q4) |- Inc(T1))" be included and considered valid in T1.

Proposition (T1.P6) - Proof of hypothesis inconsistency: Inc(H1). Proof: Let (P = Q) := (o1 = o2) follows from prop. (P5). Let (P neq Q)) := (o1 neq o2) follows from prop. (P3).  Therefore, by the inconsistency-introduction-2 inference rule: ((P6 = Q4), (P6 neq Q4) |- Inc(T1)), it follows that Inc(H1). QED

Inference rule (proof-by-contradiction-2): Let inference-rule proof-by-contradiction-2 defined as "((H1 formulate (x4 neq y4)), Inc(H1) |- (x4 = y4))" be included and considered valid in T1.

Proposition (T1.P7) - The proposition of interest: (o1 = o2). Proof: Let hyp. (H1) be the hypothesis (o1 neq o2). Inc(H1) follows from prop. (P6). Therefore, by the proof-by-contradiction-2 inference rule: ((H1 formulate (x4 neq y4)), Inc(H1) |- (x4 = y4)), it follows that (o1 = o2). QED