Christoph Benzmüller - Many Logics, One Methodology

See the video description:

This talk advances the case for logical pluralism at the object logic level within a unifying meta-logical framework. While modern proof assistant systems often enforce a single foundational logic — a tendency we may call logical imperialism — such rigidity impedes the kind of interdisciplinary reuse that robust knowledge representation demands. Our proposed alternative is LogiKEy: a logic-pluralistic methodology for knowledge representation and reasoning in which object logics are treated as first-class, analyzable entities, with applicability across many fields, including but not limited to computational metaphysics and ontology.

The virtues of LogiKEy are illustrated through a concrete case study: Gödel's modal ontological argument and Dana Scott's variant of it. Supported by experimental studies in a proof assistant system for classical higher-order logic, we demonstrate how the framework promotes interdisciplinary research and education on logical foundations and philosophical arguments, while also yielding new formal insights into these landmark arguments, and we address some questions accumulated over the past decade.

This is partly joint work with Dana Scott.

Reference: Notes on Gödel's and Scott's Variants of the Ontological Argument, Christoph Benzmüller, Dana S. Scott · Monatshefte für Mathematik 208, 569–611. Doi: https://doi.org/10.1007/s00605-025-02078-x


The question I would have asked is "What aspects of Higher Order Logic are necessary in the formalization of the Object Logics?" If you look at Church's 1940 paper "A Simple Formulation of the Theory of Types" which is a formulation of Higher Order Logic, then there are only four logical constants: Negation (N), Alternation (A), Universal Quantification over propositions (Π) and selection (ι), and everything else is an abbreviation of these, in some (typed) context of abstraction or application. Can this language not be interpreted in intuitionistic type theory? See Mark Jago on Type Theory in Computer Science, Logic and Linguistics for some quite subtle insights of Vladimir Voevodsky on this. 

Subscribe to Topos Institute.

About Logic did a "Season 1 Recap: Feedback, Highlights & Season 2 Preview" episode:

Support them financially on https://buymeacoffee.com/aboutlogic.

Subscribe to About Logic.

Comments

Post a Comment

Popular posts from this blog

Steven Johnson - So You Think You Know How to Take Derivatives?

Image
A derivative is linearisation, and differential calculus is essentially linear algebra, ...  See  Freya Holmér - Why Can't You Multiply Vectors?  and  Freya Holmér on Continuity of Splines . See also the MIT OCW page:  Matrix Calculus For Machine Learning And Beyond  (Alan Edelman, Steven G. Johnson) Subscribe to The Julia Programming Language . Alan Edelman talking about expressing mathematics as computer code. The idea is that you can use computer languages to communicate mathematical ideas precisely to other people. See my comments about functional programming languages here:  https://prooftoys.org/ian-grant/hm/ Subscribe to TEDx Talks .
Read more

Hitachi HD44780U LCD Display Fonts

Image
I finally got the bit-mapped fonts from the Hitachi "1602" display :  Here's some JavaScript: const HD44780U01ASCII=[ [],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[], [],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ], [4, 4, 4, 4, 0, 0, 4, 0, 0, 0, ], [10, 10, 10, 0, 0, 0, 0, 0, 0, 0, ], [10, 10, 31, 10, 31, 10, 10, 0, 0, 0, ], [4, 15, 20, 14, 5, 30, 4, 0, 0, 0, ], [24, 25, 2, 4, 8, 19, 3, 0, 0, 0, ], [12, 18, 20, 8, 21, 18, 13, 0, 0, 0, ], [12, 4, 8, 0, 0, 0, 0, 0, 0, 0, ], [2, 4, 8, 8, 8, 4, 2, 0, 0, 0, ], [8, 4, 2, 2, 2, 4, 8, 0, 0, 0, ], [0, 4, 21, 14, 21, 4, 0, 0, 0, 0, ], [0, 4, 4, 31, 4, 4, 0, 0, 0, 0, ], [0, 0, 0, 0, 12, 4, 8, 0, 0, 0, ], [0, 0, 0, 31, 0, 0, 0, 0, 0, 0, ], [0, 0, 0, 0, 0, 12, 12, 0, 0, 0, ], [0, 1, 2, 4, 8, 16, 0, 0, 0, 0, ], [14, 17, 19, 21, 25, 17, 14, 0, 0, 0, ], [4, 12, 4, 4, 4, 4, 14, 0, 0, 0, ], [14, 17, 1, 2, 4, 8, 31, 0, 0, 0, ], [31, 2, 4, 2, 1, 17, 14, 0, 0, 0, ], [2, 6, 10, 18, 31, 2, 2, 0, 0,...
Read more

RISC-V Peripheral Idea - A High-Speed LVDS Link for a Modern Transputer

Image
Thinking about the  TinyTapeout RISC-V Peripherals  experiment: That  Pico ICE FPGA Trainer Board  will be able to prototype a high-speed serial bus interconnect which could also be the basis for a RISC-V CPU peripheral that would be the moral equivalent of a Transputer serial-link. Each node could be a RISC-V with four links to its neighbours. LVDS drivers like the Analog Devices ADN4665 and ADN4666 , connected via low-cost SATA cables. The hardware could handle the  8b/10b encoding  and interface to DMA channels, which would be another peripheral that would probably be quite a severe test of the project infrastructure, but for the prototype the FPGA could probably be interfaced with the RP2040's DMA somehow, even if it was just via GPIO pins. There is even a Lattice Reference design for an 8b/10b encoder that you could download and drop-in.   45:31 "Is it still relevant?"  Subscribe to CSS Bristol . Then YouTube turned up this 2018 talk by...
Read more