variable-substitution (python sample)

Tags: variable-substitution 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.variable_substitution.infer_statement(...)

Sample code

Code output

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

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

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

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

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

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

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

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

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)
with u.with_variable('x') as x, u.with_variable('y') as y:
    implication = t1.i.axiom_interpretation.infer_formula_statement(a=a,
        p=f(x, y) | u.r.implies | f(y, x), lock=True)
t1.stabilize()

proposition_of_interest = t1.i.variable_substitution.infer_formula_statement(p=implication,
    phi=u.r.tupl(o1, o2))

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

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

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

Proposition (T1.P): (f(x, y) ==> f(y, x)). Proof: "Dummy axiom to establish some ground propositions." is postulated by axiom (A). (f(x, y) ==> f(y, x)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that (f(x, y) ==> f(y, x)). QED

Inference rule (variable-substitution): Let inference-rule variable-substitution defined as "(P, O |- Q)" be included and considered valid in T1.

Proposition (T1.P): (f(o, o) ==> f(o, o)). Proof: (f(x, y) ==> f(y, x)) follows from prop. (P). Let x = o, y = o. Therefore, by the variable-substitution inference rule: (P, O |- Q), it follows that (f(o, o) ==> f(o, o)). QED