Tutorial & Workshop on Computational Metaphysics and Intensionality

A tutorial and workshop on computational metaphysics and intensionality was organised on Tuesday, May 31 and Wednesday, June 1. The schedule was as follows:

(Note: Unfortunately Prof. Peter Fritz had to cancel his visit on short notice; hence, the schedule has been revised).

Tuesday, May 31: Tutorial 14:00 - 18:00

Room: WE5/01.006, An der Weberei 5, 96047 Bamberg

Tutorial: Using Isabelle/HOL in Computational Metaphysics (by Daniel Kirchner, Edward N. Zalta, Christoph Benzmüller)

Wednesday, June 1: Workshop 13:45 - 18:00

Room: WE5/04.003, An der Weberei 5, 96047 Bamberg

Session 1: 

13:45 — 14:00: Christoph Benzmüller (Professor for AI Systems Engineering, University of Bamberg & FU Berlin)

Welcome & Brief Introduction to the AISE Research Group at the University of Bamberg

14:00 — 14:45: Edward N. Zalta (Senior Research Scholar, Philosophy Department, Stanford University)

Resolving Ambiguities in the Data: How to Connect Logic and Deep Learning Methodologies

Abstract: In this talk, I attempt to build a bridge between computer scientists who use deep learning techniques and logicians who develop formal representations.  My test case will be understanding, explanation, and reasoning in mathematics, namely, how to reconcile formal logical analyses and deep learning analyses of these phenomena.  I'll explore some common ground and then highlight some key ambiguities in the data that are resolved by a logical system with two kinds of predication. This has implications for designing and training deep-learning systems for understanding mathematical language -- there are unmarked structural and lexical ambiguities in the training data that, once resolved logically, may lead to better success in building AI systems. 

14:45 — 15:30: Edward N. Zalta & Uri Nodelman (Senior Research Engineer, Stanford University)

   Number Theory Without Mathematics

Abstract: We show that in object theory, no mathematical primitives or axioms are required to derive 2nd-order Peano Arithmetic (PA2) or to prove the existence of an infinite cardinal and an infinite class. In research conducted the past year, we've taken advantage of an object-theoretic theorem by Daniel Kirchner to redefine and recast our Frege-style number theory so that "discernible" objects (whether abstract or ordinary) can be counted. This leads to: (a) a derivation of the Dedekind-Peano axioms following Frege’s plan, but adjusted for a modal setting, (b) a Recursion Theorem, (c) a definition of the primitive recursive functions as relations, (d) a definition of addition and multiplication (which yields the recursive axioms for addition and multiplication as theorems), (d) a derivation of Comprehension for Properties of Numbers, (e) a proof that aleph_0 exists (as the number of the property: being a number), and (f) a proof that the *extension* of the property of being a number is an infinite class.

Break

Session 2:

16:00 — 16:10: Christoph Benzmüller  

Foreword on Universal Logical Reasoning and the LogiKEY Methodology, Infrstructure and Tool Support

16:10 — 16:40: Daniel Kirchner (Doctoral Candidate in Mathematics, FU Berlin & Ethereum Foundation)

Applying Computational Methods to a Foundational Metaphysical Theory.  

Abstract: In this talk, I report on a recent research project in which we effectively implemented a custom theorem proving environment for a foundational metaphysical theory by means of a shallow semantic embedding in classical higher-order logic. I discuss how existing infrastructure for automated and interactive reasoning could be transferred to a theory that is based on fundamentally different logical primitives compared to the meta-logic and how this process could lead to significant advances in the targeted theory.

16:40 — 17:10: Luke Burke (Postdoctoral Researcher in Theoretical Computer Science, University of Bamberg)

Dynamic Approaches to Logical Omniscience and Natural Language Semantics

Abstract: Much work in epistemic logic aims to avoid the strong closure conditions on knowledge and belief modalities  which engender the problem of Logical Omniscience. Some recent approaches to the problem of Logical Omniscience aim to capture the way that agents apply deductive rules, in a stepwise and cumulative manner, unravelling the logical consequences of what they believe bit by bit. Such approaches use the resources of dynamic epistemic modal logic, in which the action of an agent deducing a consequence is captured by a modal operator which shifts the model at which a formula is evaluated. So far such approaches have been elaborated mainly within the context of modal propositional logic. But from the vantage point of natural language semantics, such a setting is not rich enough; in fact, a higher-order setting is preferable, since we need to be able to capture the contribution of determiners such as every and some, which usually treated as functionals. In this talk we elaborate an approach to logical omniscience which incorporates a mechanism accounting for stepwise reasoning process into the simply-typed lambda calculus, the engine of much work in compositional natural language theory. Our account leads to an interesting view on meaning as related to chains of deductive inference. 

17:10 — 17:30: David Fuenmayor (Doctoral Candidate in Computer Science, FU Berlin & University of Luxemburg & University of Bamberg)

On Using Mathematical Proof Assistants for Logico-Philosophical Investigations

Abstract: I discuss how modern mathematical proof assistants based upon Church's simple theory of types (aka. HOL) can be harnessed to allow logical reasoning with modal and other non-classical systems (paraconsistent, paracomplete, substructural, etc.). Previous work on computational philosophy by employing this approach is surveyed and some prospective applications for computational metaphysics are outlined.

 17:30 — 17:50: Michael Mendler (Universität Bamberg)

The Došen Square under construction: A tale of four modalities

Abstract: In classical modal logic, necessity []A, possibility <>A, impossibility []~A and non-necessity <>~A form a Square of Oppositions (SO) whose corners are interdefinable using classical negation. The relationship between these modalities in intuitionistic modal logic is a more delicate matter since negation is weaker. Intuitionistic non-necessity [~] and impossibility <~>, first investigated by Došen, have received less attention and — together with their positive counterparts [] and <> — form a square we call the Došen Square. Unfortunately, the core property of constructive logic, the Disjunction Property (DP), fails when the modalities are combined and, interpreted in birelational Kripke structures à la Došen, the Square partially collapses. We introduce the constructive logic CKD, whose four semantically independent modalities [], <>, [~], <~> prevent the Došen Square from collapsing under the effect of intuitionistic negation while preserving DP. The model theory of CKD involves a constructive Kripke frame interpretation of the modalities. A Hilbert deduction system and an equivalent cut-free sequent calculus are presented. Soundness, completeness and finite model property are proven, implying that CKD is decidable. The logics HK[~], HK[], HK<> and HK<~> of Došen and other known theories of intuitionistic modalities are syntactic fragments or axiomatic extensions of CKD.

(This is joint work with Luke Burke and Stephan Scheele.)

 Evening: Informal get together in town