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

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

Sample code

Code output

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

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

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

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

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

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

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

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

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

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

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

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

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (ℋ₁.𝑃₅): (𝑓₁(𝑜₁, 𝑜₂) ∧ 𝑓₁(𝑜₂, 𝑜₃)). 𝗣𝗿𝗼𝗼𝗳: 𝑓₁(𝑜₁, 𝑜₂), 𝗈𝖿 𝗍𝗁𝖾 𝖿𝗈𝗋𝗆 𝐏₁, 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝖿𝗋𝗈𝗆 𝗽𝗿𝗼𝗽. (𝑃₁). 𝑓₁(𝑜₂, 𝑜₃), 𝗈𝖿 𝗍𝗁𝖾 𝖿𝗈𝗋𝗆 𝐐₁, 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝖿𝗋𝗈𝗆 𝗽𝗿𝗼𝗽. (𝑃₂).  𝖳𝗁𝖾𝗋𝖾𝖿𝗈𝗋𝖾, 𝖻𝗒 𝗍𝗁𝖾 𝑐𝑜𝑛𝑗𝑢𝑛𝑐𝑡𝑖𝑜𝑛-𝑖𝑛𝑡𝑟𝑜𝑑𝑢𝑐𝑡𝑖𝑜𝑛 𝗂𝗇𝖿𝖾𝗋𝖾𝗇𝖼𝖾 𝗋𝗎𝗅𝖾: (𝐏₁, 𝐐₁ ⊢ (𝐏₁ ∧ 𝐐₁)), 𝗂𝗍 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝗍𝗁𝖺𝗍 (𝑓₁(𝑜₁, 𝑜₂) ∧ 𝑓₁(𝑜₂, 𝑜₃)). ∎

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

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

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

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

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

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

𝗜𝗻𝗳𝗲𝗿𝗲𝗻𝗰𝗲 𝗿𝘂𝗹𝗲 (𝑝𝑟𝑜𝑜𝑓-𝑏𝑦-𝑟𝑒𝑓𝑢𝑡𝑎𝑡𝑖𝑜𝑛-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.create_universe_of_discourse(echo=True)
a1 = u.a.declare(natural_language='Dummy axiom to establish some ground propositions.')
o1 = u.o.declare()
o2 = u.o.declare()
o3 = u.o.declare()
f = u.r.declare(arity=2, symbol='f', signal_proposition=True)
t1 = u.t(echo=True)

# Elaborate a dummy theory with a set of propositions necessary for our demonstration
a = t1.include_axiom(a=a1)
t1.i.axiom_interpretation.infer_formula_statement(a=a, p=f(o1, o2), lock=False)
t1.i.axiom_interpretation.infer_formula_statement(a=a, p=f(o2, o3), lock=False)
with u.with_variable('x') as x, u.with_variable('y') as y, u.with_variable('z') as z:
    implication = t1.i.axiom_interpretation.infer_formula_statement(a=a,
        p=(f(x, y) | u.r.land | f(y, z)) | u.r.implies | u.r.lnot(f(x, z)), lock=True)
t1.stabilize()

# Pose the negation hypothesis
h = t1.pose_hypothesis(hypothesis_formula=f(o1, o3), subtitle='We pose the positive hypothesis')
conjunction_introduction = h.child_theory.i.conjunction_introduction.infer_formula_statement(
    p=f(o1, o2), q=f(o2, o3))
variable_substitution = h.child_theory.i.variable_substitution.infer_formula_statement(
    p=implication, phi=u.r.tupl(o1, o2, o3))
modus_ponens = h.child_theory.i.modus_ponens.infer_formula_statement(
    p_implies_q=variable_substitution, p=conjunction_introduction)

# Prove hypothesis inconsistency
h_inconsistency = t1.i.inconsistency_introduction_1.infer_formula_statement(p=h.child_statement,
    not_p=modus_ponens, t=h.child_theory, subtitle='Proof of the hypothesis inconsistency')

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

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

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

Axiom (T1.A1): Let axiom A1 "Dummy axiom to establish some ground propositions." 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, o2). Proof: "Dummy axiom to establish some ground propositions." is postulated by axiom (A1). f1(o1, o2) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that f1(o1, o2). QED

Proposition (T1.P2): f1(o2, o3). Proof: "Dummy axiom to establish some ground propositions." is postulated by axiom (A1). f1(o2, o3) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that f1(o2, o3). QED

Proposition (T1.P3): ((f1(x1, y1) and f1(y1, z1)) ==> not(f1(x1, z1))). Proof: "Dummy axiom to establish some ground propositions." is postulated by axiom (A1). ((f1(x1, y1) and f1(y1, z1)) ==> not(f1(x1, z1))) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that ((f1(x1, y1) and f1(y1, z1)) ==> not(f1(x1, z1))). QED

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

Hypothesis (T1.H1) - We pose the positive hypothesis: f1(o1, o3). This hypothesis is elaborated in theory H1.

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

Proposition (H1.P5): (f1(o1, o2) and f1(o2, o3)). Proof: f1(o1, o2), of the form P1, follows from prop. (P1). f1(o2, o3), of the form Q1, follows from prop. (P2).  Therefore, by the conjunction-introduction inference rule: (P1, Q1 |- (P1 and Q1)), it follows that (f1(o1, o2) and f1(o2, o3)). QED

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

Proposition (H1.P6): ((f1(o1, o2) and f1(o2, o3)) ==> not(f1(o1, o3))). Proof: ((f1(x1, y1) and f1(y1, z1)) ==> not(f1(x1, z1))) follows from prop. (P3). Let x1 = o1, y1 = o2, z1 = o3. Therefore, by the variable-substitution inference rule: (P2, O1 |- Q2), it follows that ((f1(o1, o2) and f1(o2, o3)) ==> not(f1(o1, o3))). QED

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

Proposition (H1.P7): not(f1(o1, o3)). Proof: ((f1(o1, o2) and f1(o2, o3)) ==> not(f1(o1, o3))) follows from prop. (P6).(f1(o1, o2) and f1(o2, o3)) follows from prop. (P5). Therefore, by the modus-ponens inference rule: ((P4 ==> Q3), P4 |- Q3), it follows that not(f1(o1, o3)). QED

Inference rule (inconsistency-introduction-1): Let inference-rule inconsistency-introduction-1 defined as "(P7, not(P7) |- Inc(T1))" be included and considered valid in T1.

Proposition (T1.P8) - Proof of the hypothesis inconsistency: Inc(H1). Proof: Let P := f1(o1, o3), which follows from prop. (P4). Let not(P) := not(f1(o1, o3)), which follows from prop. (P7).  Therefore, by the inconsistency-introduction-1 inference rule: (P7, not(P7) |- Inc(T1)), it follows that Inc(H1). QED

Inference rule (proof-by-refutation-1): Let inference-rule proof-by-refutation-1 defined as "((H1 formulate P10), Inc(H1) |- not(P10))" be included and considered valid in T1.

Proposition (T1.P9) - The proposition of interest: not(f1(o1, o3)). Proof: Let hyp. (H1) be the hypothesis f1(o1, o3). Inc(H1) follows from prop. (P8). Therefore, by the proof-by-refutation-1 inference rule: ((H1 formulate P10), Inc(H1) |- not(P10)), it follows that not(f1(o1, o3)). QED