definition-interpretation (python sample)

Tags: definition-interpretation 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.definition_interpretation.infer_statement(...)

Sample code

Code output

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

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

𝗗𝗲𝗳𝗶𝗻𝗶𝘁𝗶𝗼𝗻 (𝒯₁.𝐷₁): 𝖫𝖾𝗍 𝑑𝑒𝑓𝑖𝑛𝑖𝑡𝑖𝑜𝑛 𝒟₁ ⌜𝘋𝘶𝘮𝘮𝘺 𝘥𝘦𝘧𝘪𝘯𝘪𝘵𝘪𝘰𝘯 𝘧𝘰𝘳 𝘥𝘦𝘮𝘰𝘯𝘴𝘵𝘳𝘢𝘵𝘪𝘰𝘯 𝘱𝘶𝘳𝘱𝘰𝘴𝘦𝘴⌝ 𝖻𝖾 𝗂𝗇𝖼𝗅𝗎𝖽𝖾𝖽 (𝗉𝗈𝗌𝗍𝗎𝗅𝖺𝗍𝖾𝖽) 𝗂𝗇 𝒯₁.

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

𝗣𝗿𝗼𝗽𝗼𝘀𝗶𝘁𝗶𝗼𝗻 (𝒯₁.𝑃₁) - The proposition of interest: (𝑟₁(𝑜₁, 𝑜₂) = 𝑟₂(𝑜₃)). 𝗣𝗿𝗼𝗼𝗳: ⌜𝘋𝘶𝘮𝘮𝘺 𝘥𝘦𝘧𝘪𝘯𝘪𝘵𝘪𝘰𝘯 𝘧𝘰𝘳 𝘥𝘦𝘮𝘰𝘯𝘴𝘵𝘳𝘢𝘵𝘪𝘰𝘯 𝘱𝘶𝘳𝘱𝘰𝘴𝘦𝘴⌝ 𝗂𝗌 𝗉𝗈𝗌𝗍𝗎𝗅𝖺𝗍𝖾𝖽 𝖻𝗒 𝗱𝗲𝗳. (𝐷₁). 𝑟₁(𝑜₁, 𝑜₂) 𝗂𝗌 𝖺𝗇 𝗂𝗇𝗍𝖾𝗋𝗉𝗋𝖾𝗍𝖺𝗍𝗂𝗈𝗇 𝗈𝖿 𝗍𝗁𝖺𝗍 𝖽𝖾𝖿𝗂𝗇𝗂𝗍𝗂𝗈𝗇. 𝖳𝗁𝖾𝗋𝖾𝖿𝗈𝗋𝖾, 𝖻𝗒 𝗍𝗁𝖾 𝑑𝑒𝑓𝑖𝑛𝑖𝑡𝑖𝑜𝑛-𝑖𝑛𝑡𝑒𝑟𝑝𝑟𝑒𝑡𝑎𝑡𝑖𝑜𝑛 𝗂𝗇𝖿𝖾𝗋𝖾𝗇𝖼𝖾 𝗋𝗎𝗅𝖾: (𝓓, 𝐱, 𝐲 ⊢ (𝐱 = 𝐲)), 𝗂𝗍 𝖿𝗈𝗅𝗅𝗈𝗐𝗌 𝗍𝗁𝖺𝗍 (𝑟₁(𝑜₁, 𝑜₂) = 𝑟₂(𝑜₃)). ∎

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()
o3 = u.o.declare()
r1 = u.r.declare(2, signal_proposition=True)
r2 = u.r.declare(1, signal_proposition=True)
definition = u.d.declare(natural_language='Dummy definition for demonstration purposes')

# Elaborate a dummy theory with a set of propositions necessary for our demonstration
t1 = u.t(echo=True)
theory_definition = t1.include_definition(d=definition)

# And finally, use the absorption inference-rule:
proposition_of_interest = t1.i.definition_interpretation.infer_formula_statement(
    d=theory_definition, x=r1(o1, o2), y=r2(o3), subtitle='The proposition of interest')

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

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

Definition (T1.D1): Let definition D1 "Dummy definition for demonstration purposes" be included (postulated) in T1.

Inference rule (definition-interpretation): Let inference-rule definition-interpretation defined as "(D, x, y |- (x = y))" be included and considered valid in T1.

Proposition (T1.P1) - The proposition of interest: (r1(o1, o2) = r2(o3)). Proof: "Dummy definition for demonstration purposes" is postulated by def. (D1). r1(o1, o2) is an interpretation of that definition. Therefore, by the definition-interpretation inference rule: (D, x, y |- (x = y)), it follows that (r1(o1, o2) = r2(o3)). QED