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

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

Sample code

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.c1.declare(arity=2, symbol='f', signal_proposition=True)
t1 = u.t.declare(echo=True)

# Elaborate a dummy theory with a set of propositions necessary for our demonstration
a = t1.include_axiom(a=a1)
pu.configuration.echo_proof = False
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.c1.land | f(y, z)) | u.c1.implies | f(x, z), lock=True)
t1.stabilize()

# Pose the negation hypothesis
h = t1.pose_hypothesis(hypothesis_formula=u.c1.lnot(f(o1, o3)), subtitle='We pose the negation hypothesis')

for i in h.child_theory.iterate_statements_in_theory_chain():
    print(i)

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.c1.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
pu.configuration.echo_proof = True
h_inconsistency = t1.i.inconsistency_introduction_1.infer_formula_statement(p=modus_ponens, not_p=h.child_statement,
    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_contradiction_1.infer_formula_statement(h=h, inc_h=h_inconsistency,
    subtitle='The proposition of interest')

Code output

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

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

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

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

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

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

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (𝒯₁.𝑃₃): ((𝑓₁(𝐱₁, 𝐲₁) ∧ 𝑓₁(𝐲₁, 𝐳₁)) ⟹ 𝑓₁(𝐱₁, 𝐳₁)).

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

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

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (ℋ₁.𝑃₄): ¬(𝑓₁(𝑜₁, 𝑜₃)).

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

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

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (ℋ₁.𝑃₅): (𝑓₁(𝑜₁, 𝑜₂) ∧ 𝑓₁(𝑜₂, 𝑜₃)).

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

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (ℋ₁.𝑃₆): ((𝑓₁(𝑜₁, 𝑜₂) ∧ 𝑓₁(𝑜₂, 𝑜₃)) ⟹ 𝑓₁(𝑜₁, 𝑜₃)).

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

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (ℋ₁.𝑃₇): 𝑓₁(𝑜₁, 𝑜₃).

𝗜𝗻𝗳𝗲𝗿𝗲𝗻𝗰𝗲 𝗿𝘂𝗹𝗲 (𝑖𝑛𝑐𝑜𝑛𝑠𝑖𝑠𝑡𝑒𝑛𝑐𝑦-𝑖𝑛𝑡𝑟𝑜𝑑𝑢𝑐𝑡𝑖𝑜𝑛-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)
pu.configuration.echo_proof = False
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 | f(x, z), lock=True)
t1.stabilize()

# Pose the negation hypothesis
h = t1.pose_hypothesis(hypothesis_formula=u.r.lnot(f(o1, o3)),
    subtitle='We pose the negation hypothesis')

for i in h.child_theory.iterate_statements_in_theory_chain():
    print(i)

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
pu.configuration.echo_proof = True
h_inconsistency = t1.i.inconsistency_introduction_1.infer_formula_statement(p=modus_ponens,
    not_p=h.child_statement, 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_contradiction_1.infer_formula_statement(h=h,
    inc_h=h_inconsistency, subtitle='The proposition of interest')

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

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

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).

Proposition (T1.P2): f1(o2, o3).

Proposition (T1.P3): ((f1(x1, y1) and f1(y1, z1)) ==> f1(x1, z1)).

Axiom (H1.A2): Let axiom A2 "By hypothesis, assume not(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): not(f1(o1, o3)).

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

A2
I2
not(f1(o1, o3))
A1
I1
f1(o1, o2)
f1(o2, o3)
((f1(x1, y1) and f1(y1, z1)) ==> f1(x1, z1))
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)).

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)) ==> f1(o1, o3)).

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): f1(o1, o3).

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. (P7). Let not(P) := not(f1(o1, o3)), which follows from prop. (P4).  Therefore, by the inconsistency-introduction-1 inference rule: (P7, not(P7) |- Inc(T1)), it follows that Inc(H1). QED

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

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