Topics in Free Logic

Idea and Motivation

This event is the closing workshop for the DFG funded project Free logics: variants, unification, and some applications.

Speakers

• Sara Negri, Genova
• Eugenio Orlandelli, Bologna
• Edi Pavlović, MCMP
• Greg Restall, St. Andrews
• Marcus Rossberg, Uconn (via Zoom)
• Helmut Schwichtenberg, LMU

Program

Time	Event
08.45 - 09:00	Welcome & Coffee
09:00 - 10:00	Sara Negri
10:00 - 10:30	Coffee Break
10:30 - 11:30	Edi Pavlović
11:45 - 12:45	Eugenio Orlandelli
12:45 - 14:00	Lunch
14:00 - 15:00	Helmut Schwichtenberg
15:00 - 15:30	Coffee Break
15:30 - 16:30	Marcus Rossberg
16:30- 17:00	Coffee Break
17:00 - 18:00	Greg Restall
18:45	Conference Dinner

 Abstracts

Sara Negri: Proof analysis in predicative second-order logic.

(Joint work with Matteo Tesi.)

The expressive capabilities of first-order logic are significantly expanded by second-order logic, which allows quantification over sets and properties. This extension addresses the natural demand in mathematics of expressing properties that involve quantification over all subsets or families of subsets of a given structure. Despite these advantages, full second-order logic lacks essential metalogical properties due to its impredicativity, which presents challenges in the development of proof systems.

Our study tackles these challenges by introducing a G3-style calculus that admits the predicative comprehension schema, enabling a constructive cut elimination proof.

The calculi are extended to explore the proof theory of mathematical theories, with methods from first-order calculi being adapted, and structural results being established for both classical and intuitionistic calculi. Additionally, extensional equality and apartness are defined in second-order logic, showcasing the reduction of mathematical notions to pure logic. As an example, the theory of predicative second-order arithmetic is presented, and a variant of Herbrand’s theorem tailored for predicative second-order intuitionistic logic is established, leading to the conservativity of predicative second-order Heyting arithmetic over its first-order counterpart. Furthermore, the interpolation theorem and the modal embedding of intuitionistic logic are extended to predicative second-order logic.

Edi Pavlović: Proof theory of free logics.

Free logics are a family of first-order logics which came about as a re- sult of examining the existence assumptions of classical logic. What those assumptions are varies, but the central ones are that (i) the domain of interpretation is not empty, (ii) every name denotes exactly one object in the domain and (iii) the quantifiers have existen- tial import. Free logics reject the claim that names need to denote in (ii), and positive free logic concedes that some atomic formulas containing non-denoting names (including at least self-identity) are true, negative free logic treats them as uniformly false, and neutral free logic as taking a third value.

These various logics also have complex and varied axiomatiza- tions and semantics, and the present work is a part of an ongoing project to offer, using proof-theoretic means, an orderly examination of the various systems and their mutual relations. We refine the presentations of positive and negative free logics, offer one for neutral free logic, and then finally examine further extensions of the framework.

Eugenio Orlandelli: Nested sequents for quantified modal logics with definite descriptions.

(based on j.w.w. Tim Lyon)

This talks introduces nested sequents for quantified modal logics. In particular, it considers extensions of the propositional modal logics definable by path conditions and seriality with varying, increasing, decreasing, and constant domains. Each calculus has good structural properties: weakening and contraction are height-preserving admissible and cut is (syntactically) admissible. Each calculus is sound and complete w.r.t. its intended semantics. Moreover, the calculi are internal—i.e., each sequent has a formula interpretation—whenever the existence predicate is expressible in the language. Finally, we’ll sketch how to extend the calculi to cover logics with non-rigid and non-denoting designators such as definite descriptions.

Helmut Schwichtenberg: A theory of computable functionals.

We work in a constructive extension of classical logic, where in addition to the classical existential quantifier (not – forall – not) we have a constructive one which requires an example. In this setting we sketch a theory of computable functionals (TCF) which extends Heyting’s arithmetic in all simple types. TCF includes Kreisel’s (modified) realizability predicates and has invariance axioms stating that ”to assert is to realize” (Feferman 1978) for realizability-free formulas. Using these TCF proves a soundness theorem: the term extracted from a realizability-free proof of A is a realizer of A. We conclude with some examples in constructive analysis implemented in the Minlog proof assistant.

Marcus Rossberg: Unveiling the unspoken: Using free logic to teach AI to keep silent.

The massive and rapid leaps forward in the recent development in large language models (LLMs) have been matched by an equally massive and rapid increase in their commercial deployment. The current architecture of such LLM-type AIs suffers from a principled inability to distinguish between things that are merely accidentally not said (perhaps because they are not pertinent to the topic) and things that interlocutors are or should be intentionally silent about. We diagnose this failure to be the source of a variety of (severe) harms caused by AI in the past and present, and anticipated for the future. The LLM industry reacts to any of these problems with a “more data” strategy, resulting in some superficial success. This is veneer over a rotten core. The real problem is that the logic the LLMs are build on is too coarse-grained. We draw together recent research in a variety of different areas in logic and semantics to show how to build a better logical foundation that can handle deliberate silences in a contextually sensitive manner. Adopting this basis would allow preventing harms that current models are structurally incapable of avoiding.

The crucial logical basis for the project is Neutral Free Logic.

This talk will focus mainly on this aspect. We present a sequent calculus for Neutral Free Logic (based on previous work with Dave Ripley, Norbert Gratzl, and Andrew Parisi), expanded to Second-Order Logic. We give the calculus a new “trilateralist” bounds- semantic interpretation to allow it to easily interface with discourse- representation theory, and, in particular, the question-under-discussion framework, and the semantics for monstrous contents.

Greg Restall: Defining quantifiers.

Suppose we have a language involving non-denoting singular terms. (The language of everyday mathematics provides one example. Terms like n/m and lim_x→∞ f(x) do not denote, for appropriate choices of m and of f.) It is not too difficult to define inference rules for an appropriately free logic that incorporates non-denoting terms. If t does not denote, then ϕ(t) need not entail ∃xϕ(x), and neither is ϕ(t) entailed by ∀xϕ(x). We now have a very good understanding of well-behaved cut-free sequent calculi for a variety of different free
logics, appropriate for languages with non-denoting singular terms. There is a tradition, in proof-theoretic semantics, of thinking of well-behaved inference rules for some concept as defining that concept.
If the rules are well-enough behaved (whatever that notion of good behaviour might be—whether a notion of harmony, or conservative extension and unique definability, or something else—then we are tempted to take the concept that can be introduced by such
rules to be defined by them, and hence to be apt for introduction to our vocabulary.
In this talk, I will show how, in a simple negative free logic, we are nonetheless able to—in some sense—define ”outer” quantifiers Π and Σ where ϕ(t) entails Σxϕ(x), and is entailed by Πxϕ(x), since the rules for such quantifiers meet all the strictures for defining concepts in proof-theoretic semantics mentioned above. I will discuss the significance of this result for proof-theoretic semantics and our understanding of how inference rules might be
used in definitions.

 Organizer

Registration

Please register by November 13 sending an email to Office.Leitgeb@lrz.uni-muenchen.de.

New Venue

Geschwister-Scholl-Platz 1, main building, room A014

Please note that we are not allowed to offer coffee and snacks in the seminar room. Coffee and tea will be served in office D113.