Richard PennerNov 21

#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

#math #logic #theoremProving #rust #mostGeneralUnifier #mgu

Show threadRichard PennerNov 21

An abbreviated run for examining sub-proofs of propositional logic from Russell and Whitehead, and proving that they are all tautologies:

```
% cargo test --features serde,bigint -r --test pmproofs_validation -- --include-ignored --no-capture

running 1 test
Validating PM subproofs...
Variable limit: unlimited (bigint feature enabled)
Total subproofs in database: 2997
Processed 100/2997 subproofs...
Processed 200/2997 subproofs...

...

Processed 2800/2997 subproofs...
Processed 2900/2997 subproofs...

========================================
PM SUBPROOF VALIDATION RESULTS
========================================
Total subproofs: 2997
Parse failures: 0
Skipped (too many variables): 0
Validation errors: 0
Not tautologies: 0
Successfully validated: 2997

โœ“ Successfully validated 2997 subproofs!
test all_pm_subproofs_are_tautologies ... ok

test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 2.60s

```

#Rust #logic #math #theoremProving #condensedDetachment #mostGeneralUnifier #mgu

Richard PennerNov 21

I'm writing an open source math library in #Rust to do symbolic unification. (following Meredith, Robinson, Megill) It's in pre-release (v0.1.0-alpha.13) now but I'm nearly feature-complete and I'm beginning to write interesting demonstrations with it.

I thought now would be a time to solicit feedback before the API stabilizes as per semantic versioning best practices.

Like many compilers built on top of the LLVM architecture, un-optimized Rust is about 10 times slower than the optimized code produced with the --release flag. You can really notice this with the test that sets out to exhaustively produce all expressions on sets of limited operators until all 16 Boolean functions are produced. https://docs.rs/crate/symbolic-mgu/latest/source/tests/functional_completeness.rs

Also I run through Norm Megill's archive of shortest known proofs of propositional logic statements from Whitehead and Russell's Prinicipia Mathematica and test that they and all subproofs produce tautologies. https://docs.rs/crate/symbolic-mgu/latest/source/tests/pmproofs_validation.rs

Documentation: https://docs.rs/symbolic-mgu/latest/symbolic_mgu/
Distribution: https://crates.io/crates/symbolic-mgu
Repository: https://github.com/arpie-steele/symbolic-mgu

#logic #theoremProving #condensedDetachment #mostGeneralUnifier #mgu #math

symbolic-mgu 0.1.0-alpha.13 - Docs.rs

Show threadRichard PennerJan 22, 2023

@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

Home Page - Metamath

Show threadRichard PennerJan 2, 2023

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

Richard PennerJan 2, 2023

#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