@seano @amy

Also, Gottlob Frege, Begriffsschrift (1879).
Also, https://us.metamath.org/index.html
Also, https://web.ics.purdue.edu/~dulrich/Description-of-condensed-detachment.htm

#CondensedDetachment #metamath #Logic

If D2D13 ⊢((𝜑→(¬𝜓→¬𝜒))→(𝜑→(𝜒→𝜓))) is the major premise and 1 ⊢(𝜑→(𝜓→𝜑)) is the minor premise how does #CondensedDetachment work?

1. Rewrite to have distinct metavariables
M′ ⊢((a→(¬b→¬c))→(a→(c→b)))
m′ ⊢(d→(e→d))

2. Walk the trees of the antecedent to major premise and the minor premise and build the substitutions required to map to a common unification
• a with d
• ¬b with e
• ¬c with d (and therefore with a)

M″ ⊢((¬c→(¬b→¬c))→(¬c→(c→b)))
m″ ⊢(¬c→(¬b→¬c))

3. Apply modus ponens and relabel

#CondensedDetachment examples in #Logic

Axioms:
1 ⊢(𝜑→(𝜓→𝜑))
2 ⊢((𝜑→(𝜓→𝜒))→((𝜑→𝜓)→(𝜑→𝜒)))
3 ⊢((¬𝜑→¬𝜓)→(𝜓→𝜑))

Theorems:

Here, the notation DMm means we applied Condensed Detachment to M as the major premise and m as the minor premise.

D12 ⊢(𝜑→((𝜓→(𝜒→𝜃))→((𝜓→𝜒)→(𝜓→𝜃))))
D13 ⊢(𝜑→((¬𝜓→¬𝜒)→(𝜒→𝜓)))
D21 ⊢((𝜑→𝜓)→(𝜑→𝜑))
DD211 ⊢(𝜑→𝜑) ; identity
D2D12 ⊢((𝜑→(𝜓→(𝜒→𝜃)))→(𝜑→((𝜓→𝜒)→(𝜓→𝜃))))
D2D13 ⊢((𝜑→(¬𝜓→¬𝜒))→(𝜑→(𝜒→𝜓)))
DD2D121 ⊢((𝜑→𝜓)→((𝜒→𝜑)→(𝜒→𝜓))) ; syllogism
DD2D131 ⊢(¬𝜑→(𝜑→𝜓)) ; explosion

Alternative graphic layout which I didn't like because GraphViz didn't respect the left-to-right ordering of the syntax trees, which makes it confusing. #Logic #Math #CondensedDetachment #Algorithm #graphviz