Richard Penner#CondensedDetachment example
Axiom 1: β’ (π β (π β π))
Axiom 2: β’ ((π β (π β π)) β ((π β π) β (π β π)))
Rule of Modus Ponens:
β’ Major hypothesis: β’ (π β π)
β’ Minor hypothesis: β’ π
β’ Resulting Assertion: β’ π
ββ
D<major><minor> applies the Rule of Modus Ponens treating the two given tautologies as having metavariables living in different namespaces and returning the normalized result. We extend by using underscore as a placeholder, so D__ recovers the rule of modus ponens.
ββ
"D2_" is proof of the rule:
β’ Hypothesis: β’ (π β (π β π))
β’ Resulting assertion: β’ ((π β π) β (π β π))
ββ
"D21" is a proof which unifies "1" β’ (πβ² β (πβ² β πβ²)) with the hypothesis of "D2_" giving the substitution map π: {πβ² β¦ π, πβ² β¦ π, π β¦ π} resulting in the tautology: β’ ((π β π) β (π β π))
(Note that unification can map variables from either side, but when faced with a variable matching a term has to match the variable to that term.)
ββ
"DD21_" is proof of the rule:
β’ Hypothesis: β’ (π β π)
β’ Resulting assertion: β’ ((π β π)
ββ
"DD211" is a proof which unifies "1" β’ (πβ³ β (πβ³ β πβ³)) with the hypothesis of "DD21_" giving the substitution map π: {πβ³ β¦ π, π β¦ (πβ³ β π)} resulting in the tautology: β’ (π β π)
This has been adapted and expanded from a run of my symbolic-mgu pre-release crate. https://crates.io/crates/symbolic-mgu
cargo run -r --bin compact -- --wide D__ 1 2 D2_ D21 DD21_ DD211
Dyne
Iron MSE
ASX Mkt. Sensitive
bicyclegrΓΌn