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

Tags: proof-by-refutation-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_refutation_2.infer_statement(...)

Sample code

Code output

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

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

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

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

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

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

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

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

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

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

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

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (ℋ₁.𝑃₄): ((𝑓₁(𝑜₁) = 𝑓₁(𝑜₂)) ⟹ (𝑜₁ ≠ 𝑜₂)). 𝗣𝗿𝗼𝗼𝗳: ((𝑓₁(𝐱₁) = 𝑓₁(𝐲₁)) ⟹ (𝐱₁ ≠ 𝐲₁)) 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝖿𝗋𝗈𝗆 𝗽𝗿𝗼𝗽. (𝑃₂). 𝖫𝖾𝗍 𝐱₁ = 𝑜₁, 𝐲₁ = 𝑜₂. 𝖳𝗁𝖾𝗋𝖾𝖿𝗈𝗋𝖾, 𝖻𝗒 𝗍𝗁𝖾 𝑣𝑎𝑟𝑖𝑎𝑏𝑙𝑒-𝑠𝑢𝑏𝑠𝑡𝑖𝑡𝑢𝑡𝑖𝑜𝑛 𝗂𝗇𝖿𝖾𝗋𝖾𝗇𝖼𝖾 𝗋𝗎𝗅𝖾: (𝐏₁, 𝐎₁ ⊢ 𝐐₁), 𝗂𝗍 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝗍𝗁𝖺𝗍 ((𝑓₁(𝑜₁) = 𝑓₁(𝑜₂)) ⟹ (𝑜₁ ≠ 𝑜₂)). ∎

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

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (ℋ₁.𝑃₅): (𝑜₁ ≠ 𝑜₂). 𝗣𝗿𝗼𝗼𝗳: ((𝑓₁(𝑜₁) = 𝑓₁(𝑜₂)) ⟹ (𝑜₁ ≠ 𝑜₂)) 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝖿𝗋𝗈𝗆 𝗽𝗿𝗼𝗽. (𝑃₄).(𝑓₁(𝑜₁) = 𝑓₁(𝑜₂)) 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝖿𝗋𝗈𝗆 𝗽𝗿𝗼𝗽. (𝑃₁). 𝖳𝗁𝖾𝗋𝖾𝖿𝗈𝗋𝖾, 𝖻𝗒 𝗍𝗁𝖾 𝑚𝑜𝑑𝑢𝑠-𝑝𝑜𝑛𝑒𝑛𝑠 𝗂𝗇𝖿𝖾𝗋𝖾𝗇𝖼𝖾 𝗋𝗎𝗅𝖾: ((𝐏₃ ⟹ 𝐐₂), 𝐏₃ ⊢ 𝐐₂), 𝗂𝗍 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝗍𝗁𝖺𝗍 (𝑜₁ ≠ 𝑜₂). ∎

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

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (𝒯₁.𝑃₆) - The proposition of interest: 𝐼𝑛𝑐(ℋ₁). 𝗣𝗿𝗼𝗼𝗳: 𝖫𝖾𝗍 (𝑷 = 𝑸) := (𝑜₁ = 𝑜₂) 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝖿𝗋𝗈𝗆 𝗽𝗿𝗼𝗽. (𝑃₃). 𝖫𝖾𝗍 (𝑷 ≠ 𝑸) := (𝑜₁ ≠ 𝑜₂) 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝖿𝗋𝗈𝗆 𝗽𝗿𝗼𝗽. (𝑃₅).  𝖳𝗁𝖾𝗋𝖾𝖿𝗈𝗋𝖾, 𝖻𝗒 𝗍𝗁𝖾 𝑖𝑛𝑐𝑜𝑛𝑠𝑖𝑠𝑡𝑒𝑛𝑐𝑦-𝑖𝑛𝑡𝑟𝑜𝑑𝑢𝑐𝑡𝑖𝑜𝑛-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')
t1 = u.t(echo=True)
axiom = u.a.declare(natural_language='Dummy axiom for demonstration purposes')

# Elaborate a dummy theory with inconsistent propositions
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.neq | y), lock=True)
t1.stabilize()

# Pose the inequality hypothesis
h = t1.pose_hypothesis(hypothesis_formula=o1 | u.r.eq | o2,
    subtitle='We pose the positive hypothesis')
substitution = h.child_theory.i.variable_substitution.infer_formula_statement(p=implication,
    phi=u.r.tupl(o1, o2))
inequality = h.child_theory.i.modus_ponens.infer_formula_statement(p_implies_q=substitution,
    p=f_o1_eq_f_02)

# Prove hypothesis inconsistency
h_inconsistency = t1.i.inconsistency_introduction_2.infer_formula_statement(
    x_equal_y=h.child_statement, x_unequal_y=inequality, t=h.child_theory,
    subtitle='The proposition of interest')

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

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

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

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): (f1(o1) = f1(o2)). Proof: "Dummy axiom for demonstration purposes" is postulated by axiom (A1). (f1(o1) = f1(o2)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that (f1(o1) = f1(o2)). QED

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

Axiom (H1.A2): Let axiom A2 "By hypothesis, assume (o1 = 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 = o2). Proof: "By hypothesis, assume (o1 = o2) is true." is postulated by axiom (A2). (o1 = o2) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that (o1 = o2). QED

Hypothesis (T1.H1) - We pose the positive hypothesis: (o1 = 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): ((f1(o1) = f1(o2)) ==> (o1 neq o2)). Proof: ((f1(x1) = f1(y1)) ==> (x1 neq y1)) follows from prop. (P2). Let x1 = o1, y1 = o2. Therefore, by the variable-substitution inference rule: (P1, O1 |- Q1), it follows that ((f1(o1) = f1(o2)) ==> (o1 neq o2)). QED

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 neq o2). Proof: ((f1(o1) = f1(o2)) ==> (o1 neq o2)) follows from prop. (P4).(f1(o1) = f1(o2)) follows from prop. (P1). Therefore, by the modus-ponens inference rule: ((P3 ==> Q2), P3 |- Q2), it follows that (o1 neq o2). QED

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) - The proposition of interest: Inc(H1). Proof: Let (P = Q) := (o1 = o2) follows from prop. (P3). Let (P neq Q)) := (o1 neq o2) follows from prop. (P5).  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-refutation-2): Let inference-rule proof-by-refutation-2 defined as "((H1 formulate (x4 = y4)), Inc(H1) |- (x4 neq y4))" be included and considered valid in T1.

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