Programme
09 Sep 2021. Times are CEST = UTC+2
10:00 – 10:15 

Introduction 
10:15 – 11:00 
Gratzl & Pavlović 
Proof Theory of Modal Quantified Argument Calculus 
11:00 – 11:15 
break 

11:15 – 12:00 
Lanzet 
Quantification, Ontology, and Quarc 
12:00 – 12:45 
Yin 
Quarc and a Decidable Fragment of Predicate Logic 
12:45 – 14:30 
lunch break 

14:30 – 15:30 
Pascucci & Raab 
A Geometrical Analysis of Modalities in Quarc 
15:30 – 15:45 
break 

15:45 – 16:30 
BenYami 
On ‘There Is’: Logical Investigations into Instantial Sentences 
16:30 – 17:15 
La Rosa & Pavlović 
A Nested Sequent Calculus for Quarc 
Abstracts
Norbert Gratzl (MCMP, LMU Munich)
Edi Pavlović (MCMP, LMU Munich)
Proof Theory of Modal Quantified Argument Calculus
In this paper we build upon recent developments in proof theory of the Quantified argument calculus from (Pavlović and Gratzl 2019a, 2021b), and following the template for free logic (which itself has been shown to be connected to Quarc in (Pavlović and Gratzl 2019b)) presented in (Pavlović and Gratzl 2021a), offer a modal extension of the base (G3style) sequent calculus of Quarc.
The extension is modular and allows for additions of various frame properties without the loss of desirable structural properties, such as admissibility of contraction and cut. Moreover, heightpreserving invertibility of all the rules means that a counterexample to the premise(s) of a rule also constitutes one for the conclusion. This facilitates the metatheoretic proofs of soundness and completeness and is of particular use for the latter.
After presenting the modal sequent calculus of Quarc and its properties, we turn our attention to some applications, where we discuss decidability of Quarc, as well as its connection to Aristotle's (modal) syllogistic.
===================
Ran Lanzet (The University of Haifa; Edelstein Center, Hebrew University of Jerusalem)
Quantification, Ontology, and Quarc
It is often held that ontological questions, such as
(*) Do numbers (really) exist?
have to do with quantifiers: The notion of existence with which such questions are concerned is, allegedly, what the existential quantifier of firstorder logic expresses. Call this the quantificational approach, or QA. A consequence of this approach is that an affirmative answer to (*) is, at least prima facie, a consequence of the fact that some numbers are > 7. I will consider a logical motivation for QA, based on the following idea: A domain is indispensable for quantification in the logic that underlies our discourse. This, as I will explain, can lead to the identification of the existential quantifier’s domain with the class of everything that exists. I will argue, however, that the resulting motivation for QA can be undermined by considering a domainfree model theory for Quarc.
===================
Hongkai Yin (Central European University, Vienna)
Quarc and a Decidable Fragment of Predicate Logic
Quarc (with minor additional settings) has been shown to embed the firstorder predicate logic (PL), where we observe that the use of anaphors contributes a lot to the expressive power of Quarc. Anaphors in effect play the role that variables play in PL. Also, reordered predicates allow us to permutate arguments or quantifiers, which can enhance the expressive power in another way. But as we know, there is a balance between the expressive power of a logic and its computational complexity. The less a logic can express, the more likely it is to be decidable. Not that surprisingly, if we omit anaphors and reordered predicates from Quarc, we get a fragment which can be translated into a decidable fragment of PL (with identity), the fluted fragment. Moreover, the fluted fragment hints at a restricted use of anaphora which does not break decidability.
===================
Matteo Pascucci (Slovak Academy of Sciences, Bratislava; Central European University, Vienna)
Jonas Raab (University of Manchester)
A Geometrical Analysis of Modalities in Quarc
We discuss the way in which various de re and de dicto modalities can be represented in Quarc and encode their logical relations via Aristotelian polygons of opposition. We show that an Aristotelian polygon can be analysed in terms of a deductive framework based on inference trees which allows for decidable reasoning. Furthermore, we illustrate how inference trees can be transformed into sequences of derivations in a modeltheoretic semantics for Quarc.
===================
Hanoch BenYami (Central European University, Vienna)
On ‘There Is’: Logical Investigations into Instantial Sentences
Instantial sentences – ‘There are philosophers who study Quarc’, ‘There are giraffes, but there are no unicorns’ – have been translated in the Fregean tradition with the socalled existential quantifier, assimilating them to particularly quantified sentences and to ascriptions of existence. We first show that natural language distinguishes these three constructions, and note the formal relations between the first two. We then extend Quarc to translate instantial sentences, provide appropriate semantics preserving the noted distinctions and relations, and discuss prooftheoretic issues. Next, we extend the formalisation, to capture instantial sentences with quantified nouns and modal verbs. We note the implication of this work to the possibility of talk about nonexisting particulars and for the irrelevance of these formal structures to ontology.
===================
Elio La Rosa (MCMP, LMU Munich)
Edi Pavlović (MCMP, LMU Munich)
A Nested Sequent Calculus for Quarc
In this talk, we present some advances in a formalisation of a proof system for Quarc without the rule of instantiation (as for the sequent calculus in Pavlović and Gratzl, 2019a, 2021b) with even the rules for quantifiers not having to rely on a unary predicate being instantiated. This is achieved by universally closing the rule of particular quantifier introduction, hence the need of a nested calculus, in which rules can be applied directly to substructures of a sequent. As a starting point, we employ the nested calculus for (a particular kind of) Free Logic of Brünnler (2010), given the similarities that such logics bear with Quarc (Pavlović and Gratzl, 2019b). In order to adapt such a calculus, some arguments can have “structural” counterpart in the same sense in which, in sequent calculus, the comma is the structural counterpart of disjunction.
===================
References
Brünnler, K. (2010) How to universally close the existential rule. In International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer, Berlin, Heidelberg: 172–186.
Pavlović, E., and Gratzl, N. (2019a) Prooftheoretic analysis of the Quantified argument calculus. The Review of Symbolic Logic 12.4: 607–636.
Pavlović, E., and Gratzl, N. (2019b) Free logic and the Quantified argument calculus. In Philosophy of Logic and Mathematics: Proceedings of the 41st International Ludwig Wittgenstein Symposium, G. M. Mras, P. Weingartner, and B. Ritter, Eds., vol. 27, Walter de Gruyter GmbH: 105–115.
Pavlović, E., and Gratzl, N. (2021a) A more unified approach to free logics. Journal of Philosophical Logic 50: 117–148.
Pavlović, E., and Gratzl, N. (2021b) Abstract forms of quantification in the Quantified argument calculus. The Review of Symbolic Logic: 1–32.