First, I’m not (yet) an expert in formalized mathematics. I know Isabelle/ZF better, but have only overall view of Isabelle/HOL. Nevertheless I want to tell my opinion on typed (such as HOL) vs. untyped (such as Isabelle/ZF) systems. Slawomir Kolodynski converted me…
read moreIn the past I considered my purpose to exactly and directly follow commandments of Bible. I had some purposes hardly set as the aim of my life. My life was driven by these purposes not by my wish or my heart. I…
read moreI proved the following (not very hard) theorem: Theorem $latex f|^{\mathsf{RLD}}_{\{ \alpha \}} = \{ \alpha \} \times^{\mathsf{RLD}} \mathrm{im} \left( f|^{\mathsf{RLD}}_{\{ \alpha \}} \right)$ for every reloid $latex f$ and $latex \alpha \in \mho$. See the online article about funcoids and reloids.
read moreI’m sick with the following: I repeatedly formulate conjectures which have trivial counterexamples and am stuck attempting to prove these true not seeing counterexamples. I should less rely on my ideas what is a true conjecture. I just need to become humbler…
read moreFilters on Posets and Generalizations online article updated as an accomplishment of this plan. This is important primarily to extend the category of pointfree funcoids with objects being arbitrary posets (even without least element). That way this category would become more “complete”….
read moreI wrote short article “Generalization in ZF” accompanied with Isabelle/ZF sources. This is a draft and alpha. I await your comments on both the article and Isabelle sources. I’m sure my Isabelle sources may be substantially improved (and I plan to work…
read moreI corrected a small error in “Filters on Posets and Generalizations” article. The error was in Appendix B in the proof of the theorem stating $latex (t;x)\not\in S$ (I messed $latex t$ and $latex \{t\}$.)
read moreI decided to dedicate my free (of working as a programmer) time to write a book about religion (What book? It will be a surprise.) So in a few nearby months I am going to not continue my math research. I am…
read moreMy problem whether weak partitioning and strong partitioning of a complete lattice are the same was solved by counter-example by François G. Dorais. Remains open whether strong and weak partitioning of a filter object is the same.
read moreI have proved this conjecture: Theorem 1 If $latex {\mathfrak{F}}&fg=000000$ is the set of filter objects on a set $latex {U}&fg=000000$ then $latex {U}&fg=000000$ is the center of the lattice $latex {\mathfrak{F}}&fg=000000$. (Or equivalently: The set of principal filters on a set…
read more