| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Mereology/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 29.4.2026 mit Größe 1 kB |
|
Quelle GMM.thySprache: Isabelle |
|||||||||||||||
|
section ‹ General Minimal Mereology › (*<*) theory GMM imports GM MM begin (*>*) text ‹ The theory of \emph{general minimal mereology} adds general mereology to m cite‹"casati_parts_1999"› p. 46.} locale GMM = GM + MM begin text ‹ It is natural to assume that just as closed minimal mereology and closed e the same theory, so are general minimal mereology and general extensional mereo mistake see cite‹"simons_parts:_1987"› p. 37 and cite‹"casati_parts_1999"› p. 4 corrected in cite‹"pontow_note_2004"› and cite‹"hovda_what_2009"›. For discussi this issue see, for example, cite‹"varzi_universalism_2009"› and cite‹"cotnoir_ this is not the case, since the proof of strong supplementation in closed minim the product closure axiom. However, in general minimal mereology, the fusion ax the product closure axiom. So neither product closure nor strong supplementatio lemma product_closure: "O x y ==> (∃ z. ∀ v. P v z ⟷ P v x ∧ P v y)" nitpick [expect = genuine] oops lemma strong_supplementation: "¬ P x y ==> (∃ z. P z x ∧ ¬ O z y)" nitpick [expect = genuine] oops end (*<*) end (*>*)
¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09