{"id":132,"date":"2017-03-22T21:30:28","date_gmt":"2017-03-22T20:30:28","guid":{"rendered":"http:\/\/owlofminerva.net\/kubota\/?page_id=132"},"modified":"2020-10-18T23:23:35","modified_gmt":"2020-10-18T21:23:35","slug":"online-contributions","status":"publish","type":"page","link":"https:\/\/owlofminerva.net\/kubota\/online-contributions\/","title":{"rendered":"Online Contributions"},"content":{"rendered":"\n<h4 class=\"wp-block-heading\">(selection, in reverse chronological order)<\/h4>\n\n\n\n<ul class=\"wp-block-list\"><li><a rel=\"noreferrer noopener\" href=\"https:\/\/groups.io\/g\/marxistphilosophy\/message\/359\" target=\"_blank\">Hegel and the Left: Hegel-Marx (dialectics, method), Hegel-Adorno (identity, non-identity)<\/a>, Oct. 2020.<\/li><li><a rel=\"noreferrer noopener\" href=\"https:\/\/www.marxhegelforum.com\/discussion\/14\/thomas-sekine-and-marxs-approach\" target=\"_blank\">Thomas T. Sekine and Marx&#8217;s Approach (with announcement of <em>The Dialectic of Capital<\/em>)<\/a>, Oct. 2020.<\/li><li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2020-July\/msg00074.html\" target=\"_blank\" rel=\"noreferrer noopener\">Representing type dependencies in Isabelle\/HOL and in dependent type theory<\/a>, Jul. 2020.<\/li><li><a href=\"https:\/\/groups.io\/g\/marxistphilosophy\/message\/143\" target=\"_blank\" rel=\"noreferrer noopener\">Homology between Hegel&#8217;s Logic and Marx&#8217;s Capital<\/a>, Jul. 2020.<\/li><li><a href=\"https:\/\/groups.google.com\/d\/msg\/metamath\/Fgn0qZEzCko\/bvVem1BZCQAJ\" target=\"_blank\" rel=\"noreferrer noopener\">Metamath, Isabelle\/HOL, Coq, Lean (General debate initiated by Kevin Buzzard on formalizing mathematics: Where is the fashionable mathematics?)<\/a>, Feb. 2020. (Other mailing lists: <a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/36930837\/\" target=\"_blank\" rel=\"noreferrer noopener\">HOL<\/a>, <a href=\"https:\/\/sympa.inria.fr\/sympa\/arc\/coq-club\/2020-02\/msg00137.html\" target=\"_blank\" rel=\"noreferrer noopener\">Coq (part 1)<\/a>, <a href=\"https:\/\/sympa.inria.fr\/sympa\/arc\/coq-club\/2020-02\/msg00138.html\" target=\"_blank\" rel=\"noreferrer noopener\">Coq (part 2)<\/a>.)<\/li><li><a href=\"https:\/\/groups.io\/g\/hegel\/message\/45268\" target=\"_blank\" rel=\"noreferrer noopener\">\u017di\u017eek on Hegel and Adorno \u2013 Philosophical Bibliography [2019]<\/a>, Dec. 2019.<\/li><li><a href=\"https:\/\/groups.io\/g\/marxistphilosophy\/message\/32\" target=\"_blank\" rel=\"noreferrer noopener\">Antonio Wolf&#8217;s Hegel blog &#8220;The Empyrean Trail&#8221; and German Daniel Castiglioni&#8217;s Spanish article &#8220;Six Theses for Interpreting &#8216;Capital&#8217; in Light of Hegel\u2019s Logic&#8221;<\/a>, Dec. 2019.<\/li><li><a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel-logic\/conversations\/messages\/42\" target=\"_blank\" rel=\"noreferrer noopener\">Backhaus\/Reichelt and the Uno-Sekine school<\/a>, Apr. 2019.\u00a0(Other mailing lists: <a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel-marx\/conversations\/messages\/2733\" target=\"_blank\" rel=\"noreferrer noopener\">Hegel-Marx<\/a>.)<\/li><li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2018-September\/msg00045.html\" target=\"_blank\" rel=\"noreferrer noopener\">Type abstraction<\/a>, Sep. 2018.<\/li><li><a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/36358180\/\" target=\"_blank\" rel=\"noreferrer noopener\">The Principle of Mathematical Induction<\/a>, Jul. 2018. (Other mailing lists:\u00a0<a href=\"https:\/\/sympa.inria.fr\/sympa\/arc\/coq-club\/2018-07\/msg00012.html\">Coq<\/a>.)<\/li><li><a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel\/conversations\/messages\/41859\" target=\"_blank\" rel=\"noreferrer noopener\">The three levels of analysis in the Uno-Sekine approach, and the critique of the premature reference to labor (Andy Blunden&#8217;s review)<\/a>, Jun. 2018.\u00a0(Other mailing lists: <a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel-logic\/conversations\/messages\/37\" target=\"_blank\" rel=\"noreferrer noopener\">Hegel-Logic<\/a>\u00a0and\u00a0<a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel-marx\/conversations\/messages\/2730\" target=\"_blank\" rel=\"noreferrer noopener\">Hegel-Marx<\/a>.)<\/li><li><a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel-art\/conversations\/messages\/5\" target=\"_blank\" rel=\"noreferrer noopener\">&#8220;Damage Control: Adorno, Los Angeles, and the Dislocation of Culture&#8221; by\u00a0Nico Israel<\/a>, Jun. 2018. (Other mailing lists: <a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel-hegelians\/conversations\/messages\/806\" target=\"_blank\" rel=\"noreferrer noopener\">Hegel-Hegelians<\/a>.)<\/li><li><a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel\/conversations\/messages\/41842\" target=\"_blank\" rel=\"noreferrer noopener\">The structure of Sekine: The Dialectic of Capital [Sekine, 1986]<\/a>, Jun. 2018. (Other mailing lists: <a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel-logic\/conversations\/messages\/36\" target=\"_blank\" rel=\"noreferrer noopener\">Hegel-Logic<\/a>\u00a0and\u00a0<a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel-marx\/conversations\/messages\/2728\" target=\"_blank\" rel=\"noreferrer noopener\">Hegel-Marx<\/a>.)<\/li><li><a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel\/conversations\/messages\/41827\" target=\"_blank\" rel=\"noreferrer noopener\">Mark Edward Meaney \u2013\u00a0Capital as organic unity: The role of Hegel&#8217;s &#8220;Science of Logic&#8221; in Marx&#8217;s &#8220;Grundrisse&#8221;<\/a>, Jun. 2018. (Other mailing lists: <a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel-logic\/conversations\/messages\/34\" target=\"_blank\" rel=\"noreferrer noopener\">Hegel-Logic<\/a>\u00a0and\u00a0<a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel-marx\/conversations\/messages\/2726\" target=\"_blank\" rel=\"noreferrer noopener\">Hegel-Marx<\/a>.)<\/li><li><a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel\/conversations\/messages\/41818\" target=\"_blank\" rel=\"noreferrer noopener\">The prohibition of the contradiction and the imperative (necessity) of the contradiction<\/a>, Jun. 2018. (Other mailing lists: <a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel-logic\/conversations\/messages\/33\" target=\"_blank\" rel=\"noreferrer noopener\">Hegel-Logic<\/a>\u00a0and\u00a0<a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel-marx\/conversations\/messages\/2724\" target=\"_blank\" rel=\"noreferrer noopener\">Hegel-Marx<\/a>.)<\/li><li><a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel\/conversations\/messages\/41816\" target=\"_blank\" rel=\"noreferrer noopener\">The labour theory of value<\/a>, Jun. 2018. (Other mailing lists: <a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel-logic\/conversations\/messages\/32\" target=\"_blank\" rel=\"noreferrer noopener\">Hegel-Logic<\/a>\u00a0and\u00a0<a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel-marx\/conversations\/messages\/2723\" target=\"_blank\" rel=\"noreferrer noopener\">Hegel-Marx<\/a>.)<\/li><li><a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel\/conversations\/messages\/41813\" target=\"_blank\" rel=\"noreferrer noopener\">Literature on Hegel&#8217;s Science of Logic, in particular Hegel&#8217;s Logic of Essence, and on Marx&#8217;s Theory of Value<\/a>, Jun. 2018. (Other mailing lists: <a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel-logic\/conversations\/messages\/29\" target=\"_blank\" rel=\"noreferrer noopener\">Hegel-Logic<\/a>\u00a0and\u00a0<a href=\"https:\/\/groups.yahoo.com\/neo\/groups\/hegel-marx\/conversations\/messages\/2720\" target=\"_blank\" rel=\"noreferrer noopener\">Hegel-Marx<\/a>.)<\/li><li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2018-June\/msg00048.html\" target=\"_blank\" rel=\"noreferrer noopener\">The two characteristics of an antinomy: self-reference and negation<\/a>, Jun. 2018. (Other mailing lists:\u00a0<a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/36336088\/\" target=\"_blank\" rel=\"noreferrer noopener\">HOL<\/a> and <a href=\"https:\/\/groups.google.com\/forum\/#!msg\/metamath\/59maZQxlxyM\/-hHtk7YQBAAJ\" target=\"_blank\" rel=\"noreferrer noopener\">Metamath<\/a>.)<\/li><li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2018-June\/msg00000.html\" target=\"_blank\" rel=\"noreferrer noopener\">Type Theory vs. Set Theory (HOL, Isabelle\/HOL, Q0, and R0 vs. ZFC)<\/a>, Jun. 2018. (Other mailing lists:\u00a0<a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/36333206\/\" target=\"_blank\" rel=\"noreferrer noopener\">HOL<\/a> and\u00a0<a href=\"https:\/\/groups.google.com\/d\/msg\/metamath\/fQUrluTcigM\/KRGoQxPbAgAJ\" target=\"_blank\" rel=\"noreferrer noopener\">Metamath<\/a>.)<\/li><li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2018-May\/msg00013.html\" target=\"_blank\" rel=\"noreferrer noopener\">Logical Frameworks and the Foundations of Mathematics<\/a>, May 2018. (Other mailing lists:\u00a0<a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/36309577\/\" target=\"_blank\" rel=\"noreferrer noopener\">HOL<\/a> and\u00a0<a href=\"https:\/\/groups.google.com\/d\/msg\/metamath\/Qkb8L0Fsc9Q\/H2PqdkogAwAJ\" target=\"_blank\" rel=\"noreferrer noopener\">Metamath<\/a>.)<\/li><li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2018-March\/msg00051.html\" target=\"_blank\" rel=\"noreferrer noopener\">Binding the type variable in the Axiom of Choice<\/a>, Mar. 2018. (Other mailing lists:\u00a0<a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/36261982\/\" target=\"_blank\" rel=\"noreferrer noopener\">HOL<\/a>.)<\/li><li><a href=\"https:\/\/groups.google.com\/d\/msg\/metamath\/zng1z3Lkh3w\/9jrJe2PMBwAJ\" target=\"_blank\" rel=\"noreferrer noopener\">Formalization, semantic and syntactic approach<\/a>, Aug.\u00a02017.<\/li><li><a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/35962259\/\" target=\"_blank\" rel=\"noreferrer noopener\">Coquand on HOL; similarity to Q<\/a>, Jul.\u00a02017.<\/li><li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2017-May\/msg00029.html\" target=\"_blank\" rel=\"noreferrer noopener\">Software Implementation of the Mathematical Logic R<span style=\"font-size: 70%; vertical-align: sub;\">0<\/span> Available for Download<\/a>, May\u00a02017. (Other mailing lists:\u00a0<a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/35834535\/\" target=\"_blank\" rel=\"noreferrer noopener\">HOL<\/a> and\u00a0<a href=\"https:\/\/sympa.inria.fr\/sympa\/arc\/coq-club\/2017-05\/msg00034.html\" target=\"_blank\" rel=\"noreferrer noopener\">Coq<\/a>,\u00a0<a href=\"https:\/\/groups.google.com\/d\/msg\/metamath\/zpXrVh3xQXE\/V-C3f3vRAgAJ\" target=\"_blank\" rel=\"noreferrer noopener\">Metamath<\/a>.)<\/li><li><a href=\"https:\/\/groups.google.com\/d\/msg\/metamath\/s19SSncdtiM\/RAiC-tuWCAAJ\" target=\"_blank\" rel=\"noreferrer noopener\">Comparison of Metamath and Q<span style=\"font-size: 70%; vertical-align: sub;\">0<\/span><\/a>, Apr. 2017.<\/li><li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2017-April\/msg00042.html\" target=\"_blank\" rel=\"noreferrer noopener\">Publication of the Mathematical Logic R<span style=\"font-size: 70%; vertical-align: sub;\">0<\/span>: Mathematical Formulae<\/a>, Apr. 2017. (Other mailing lists:\u00a0<a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/35779686\/\" target=\"_blank\" rel=\"noreferrer noopener\">HOL<\/a> and\u00a0<a href=\"https:\/\/sympa.inria.fr\/sympa\/arc\/coq-club\/2017-04\/msg00037.html\" target=\"_blank\" rel=\"noreferrer noopener\">Coq<\/a>.)<\/li><li><a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/35648326\/\" target=\"_blank\" rel=\"noreferrer noopener\">On the natural language of formal logic and mathematics<\/a>, Feb. 2017.\u00a0(Other mailing lists:\u00a0<a href=\"https:\/\/sympa.inria.fr\/sympa\/arc\/coq-club\/2017-02\/msg00024.html\" target=\"_blank\" rel=\"noreferrer noopener\">Coq<\/a>.)<\/li><li><a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/35458077\/\" target=\"_blank\" rel=\"noreferrer noopener\">Group theory, expressed with type abstraction<\/a>, Nov. 2016.<\/li><li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2016-October\/msg00087.html\" target=\"_blank\" rel=\"noreferrer noopener\">The definitional principles of HOL and equivalent\u00a0mechanisms in Q<span style=\"font-size: 70%; vertical-align: sub;\">0<\/span>\/R<span style=\"font-size: 70%; vertical-align: sub;\">0<\/span><\/a>, Oct. 2016. (Other mailing lists:\u00a0<a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/35448609\/\" target=\"_blank\" rel=\"noreferrer noopener\">HOL<\/a>.)<\/li><li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2016-October\/msg00070.html\" target=\"_blank\" rel=\"noreferrer noopener\">Type abstraction (binding type variables with lambda)<\/a>, Oct. 2016. (Other mailing lists:\u00a0<a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/35446249\/\" target=\"_blank\" rel=\"noreferrer noopener\">HOL<\/a>.)<\/li><li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2016-October\/msg00050.html\" target=\"_blank\" rel=\"noreferrer noopener\">Allowing several types for mathematical entities (and comparison with PVS)<\/a>, Oct. 2016. (Other mailing lists:\u00a0<a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/35437586\/\" target=\"_blank\" rel=\"noreferrer noopener\">HOL<\/a>.)<\/li><li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2016-September\/msg00014.html\" target=\"_blank\" rel=\"noreferrer noopener\">On the question of expressiveness\/reducibility<\/a>, Sep. 2016. (Other mailing lists:\u00a0<a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/35330349\/\" target=\"_blank\" rel=\"noreferrer noopener\">HOL<\/a>.)<\/li><li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2016-August\/msg00069.html\" target=\"_blank\" rel=\"noreferrer noopener\">Lambda-Conversion is a rule; Avoiding non-logical axioms (Axiom of Choice, Axiom of Infinity)<\/a>, Aug. 2016. (Other mailing lists:\u00a0<a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/35280731\/\" target=\"_blank\" rel=\"noreferrer noopener\">HOL<\/a>.)<\/li><li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2016-July\/msg00058.html\" target=\"_blank\" rel=\"noreferrer noopener\">The two properties (self-reference and negativity) of an antinomy (paradox)<\/a>, Jul. 2016.<\/li><li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2016-July\/msg00029.html\" target=\"_blank\" rel=\"noreferrer noopener\">Corrections of and amendments to prior publications on Goedel&#8217;s First Incompleteness Theorem; Russell O&#8217;Connor&#8217;s definitions for its proof in Peter B. Andrews&#8217; logic Q<span style=\"font-size: 70%; vertical-align: sub;\">0<\/span>; Comparison of the proofs by O&#8217;Connor and Paulson<\/a>, Jul. 2016. (Other mailing lists:\u00a0<a href=\"https:\/\/sourceforge.net\/p\/hol\/mailman\/message\/35207290\/\" target=\"_blank\" rel=\"noreferrer noopener\">HOL<\/a> and\u00a0<a href=\"https:\/\/sympa.inria.fr\/sympa\/arc\/coq-club\/2016-07\/msg00035.html\" target=\"_blank\" rel=\"noreferrer noopener\">Coq<\/a>.)<\/li><li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2015-July\/msg00147.html\" target=\"_blank\" rel=\"noreferrer noopener\">Description of the higher-order logic Q<span style=\"font-size: 70%; vertical-align: sub;\">0<\/span>\u00a0(simple type theory)<\/a>, Jul. 2015.<\/li><\/ul>\n","protected":false},"excerpt":{"rendered":"<p>(selection, in reverse chronological order) Hegel and the Left: Hegel-Marx (dialectics, method), Hegel-Adorno (identity, non-identity), Oct. 2020. Thomas T. Sekine and Marx&#8217;s Approach (with announcement of The Dialectic of Capital), Oct. 2020. Representing type dependencies in Isabelle\/HOL and in dependent type theory, Jul. 2020. Homology between Hegel&#8217;s Logic and Marx&#8217;s Capital, Jul. 2020. Metamath, Isabelle\/HOL, [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":21,"comment_status":"closed","ping_status":"closed","template":"","meta":{"sfsi_plus_gutenberg_text_before_share":"","sfsi_plus_gutenberg_show_text_before_share":"","sfsi_plus_gutenberg_icon_type":"","sfsi_plus_gutenberg_icon_alignemt":"","sfsi_plus_gutenburg_max_per_row":"","footnotes":""},"class_list":["post-132","page","type-page","status-publish","hentry","post-preview"],"_links":{"self":[{"href":"https:\/\/owlofminerva.net\/kubota\/wp-json\/wp\/v2\/pages\/132","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/owlofminerva.net\/kubota\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/owlofminerva.net\/kubota\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/owlofminerva.net\/kubota\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/owlofminerva.net\/kubota\/wp-json\/wp\/v2\/comments?post=132"}],"version-history":[{"count":39,"href":"https:\/\/owlofminerva.net\/kubota\/wp-json\/wp\/v2\/pages\/132\/revisions"}],"predecessor-version":[{"id":701,"href":"https:\/\/owlofminerva.net\/kubota\/wp-json\/wp\/v2\/pages\/132\/revisions\/701"}],"wp:attachment":[{"href":"https:\/\/owlofminerva.net\/kubota\/wp-json\/wp\/v2\/media?parent=132"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}