Richard Moot

Do model-theoretic grammars have fundamental advantages over proof-theoretic grammars?

Introduction

In a series of articles, [START_REF] Pullum | On the distinction between model-theoretic and generative-enumerative syntactic frameworks[END_REF], 2005), and later Pullum (2013a[START_REF] Pullum | What grammars are, or ought to be[END_REF][START_REF] Pullum | Theorizing about the syntax of human language: a radical alternative to generative formalisms[END_REF] have advocated model-theoretic syntax as a 'radical alternative' to syntactic theory as it has essentially ever been practiced before.

They contrast model-theoretic syntax (MTS) with what they call generative enumerative syntax (GES). Where generative enumerative syntax uses tools from proof theory, model-theoretic syntax uses the tools of model theory, even though in either case the concrete links with model theory and proof theory are generally rather tenuous.

While I can only applaud the introduction of new mathematical tools into formal linguistics, especially when they lead to deep mathematical results and novel perspectives [START_REF] Rogers | A Descriptive Approach to Language-Theoretic Complexity[END_REF]), Pullum's advocacy of MTS is based on claims that there are a number of important facts any linguistic theory should explain, and that the MTS explanations for these facts are inherently superior to any explanation GES could provide, since the flaws of GES are "unavoidable side effects of the deepest aspects of the generative type of formalism itself" [START_REF] Pullum | Theorizing about the syntax of human language: a radical alternative to generative formalisms[END_REF].

These claims about the superiority of MTS are frequently repeated without argument or discussion in the MTS literature. Postal (2010, p. 4) even claims "there are unrefuted arguments in the literature that adequate [natural language] grammars cannot be proof-theoretic". What surprised me about model-theoretic syntax is that although its advantages have been touted for more than 20 years now, few people appear to have bothered trying to demonstrate these advantages in practice. This makes it worth investigating precisely what these claimed advantages are, and how much evidence has been presented in their favour. Is there any substance to these supposed advantages or are they, to cite Pullum (2013a, p. 532) in a different context, "like cosmologists' references to dark energy, known to be out there somewhere but as yet neither empirically located nor theoretically accounted for in detail"?

Background

In this section we will briefly define the basic terms, and make explicit a number of distinctions which are often glossed over.

Logic and algorithms

Unfortunately, there is some confusion in the literature between declarative definitions and procedures, with procedural terminology being used in the proof-theoretic context and declarative terminology in the model-theoretic context. This can give the misleading impression that the main distinction between model-theoretic and proof-theoretic grammars is that the first are declarative and the second procedural.

It is therefore important to remember the following well-known dictum [START_REF] Kowalski | Algorithm = logic + control[END_REF].

algorithm = logic + control (1)
In a declarative programming paradigm, we give a logical description of our problem, then add a control strategy to obtain an algorithm. As an example, suppose we write a simple definite clause grammar (without function symbols). When we use the Prolog execution mechanism, we obtain a top-down parser, but when we use the Datalog execution mechanism we obtain a bottom-up parser. The logic stays exactly the same, but the control mechanism produces very different algorithms. Pullum & Scholz (2001, p. 19) are right to warn about 'procedural metaphors', and these procedural metaphors appear to go back at least to the early work of Chomsky. As a consequence, it is strictly wrong to say that generative grammars provide "a method or program for random construction" (Pullum 2013a, p. 495), or that they are "nondeterministic random construction procedures" (Pullum 2020, p. 4). Generative grammars are "nondeterministic random constrution procedures" in the same sense that linguistic structures in model-theoretic syntax are non-empty strings over the alphabet {0, 1}, and grammars use logic as a type of random access machine to verify these strings satisfy certain properties: strictly speaking both of these statements are valid interpretations, but they leave out so much context as to be exceptionally misleading, a rhetorical strategem that would merit a number of Pinocchios at many fact checking sites. Generative grammars, whatever the formalism used, are declarative statements, and they become algorithms only with the addition of procedural control. Therefore, the distinction Pullum (2020, ibid ) makes between 'expansion oriented' and 'composition oriented' is purely a choice of control mechanism and has no relation to the logic used.

It is a strength of proof-theoretic syntax that it is generally fairly easy to given grammars a procedural interpretation. But even though procedural metaphors are a good tool to describe and explain grammar rules, we should always remember this is just a procedural interpretation of the rule: the literature on parsing and automated theorem proving demonstrates there are often many ways to turn the same declarative rules into different procedures.

Proofs and models

Given that proofs and models will be important throughout this paper, I will review some of the basic notions. Most readers with basic familiarity in logic will be able to skip this section.

The basic objects in model theory are structures, sets with associated relations and/or functions, defined as follows.

Definition 1 A structure is a tuple of the form.

 = ⟨ , , ⟩
In this definition is a non-empty domain, is the signature, specifying the nonlogical symbols (predicates, functions, constants) and their arity, and is an interpretation function. When is a function of arity ( ), ( ) is a function from ( ) to . When is a predicate of arity ( ), ( ) is a subset of ( ) . Constants are treated as functions of arity 0; ( ) is therefore a member of . This is the basic definition of a structure as you might find it in mathematical logic. It defines the non-logical symbols in the formal language of the logic we use, and ensures each symbol receives an interpretation of the appropriate type: an -ary predicate is interpreted as the set of -tuples for which it the predicate it true, an -ary function is a function from entities in our domain to an entity in our domain. This ensures that structures defined this way are possible models for logics with the same signature .

Example 1 As a concrete example, a very crude representation of "John sleeps" in the model-theoretic framework could look as follows. We take

 = ⟨ , , ⟩
, and as follows.

= { , , , , } (John) = 1 (NP) = 1 (sleeps) = 1 (V) = 1 (head) = 2 (S) = 1 (subj) = 2 (cat) = 2 (John) = { } (sleeps) = { } (NP) = { } (VP) = { } (S) = { } (cat) = {( , )} (cat) = {( , )} (head) = {( , )} (subj) = {( , )}
When we portray nodes as their labels (the unary predicate which is true at this node), and binary predicates as arrows from their first to their second argument, we can draw this structure as follows.

John sleeps NP V

S cat cat subj head

◊

In structure  of Example 1, a number of formulas are satisfied, for example ∃ .NP( ) (choose = ) and ∀ NP( ) ⇒ ∃ . ( )∧subj( , ) (we verify the formula for all such that NP( ) holds, only in the structure, and we can choose for ). These formulas are not particularly interesting from a linguistic point of view, but  is still a model for these formulas, so we can write, for example  ⊨ ∃ .NP( ). For our grammatical principles, we generally want to state things which are true in all models, not just specific ones.

The basic objects of proof theory are proofs. These are defined inductively. We have a set of axioms, the basic building blocks of proofs, and a set of rules which take one or more proofs to produce a new proof. For example, from a proof of and a proof of ⇒ we produce a proof of using the familiar modus ponens rule. . . . . . . . .

⇒

There are generally many different proof systems for a logic. For example, we can give a rule to introduce a conjunction ' ∧ ' as follows.

. . . . . . . .

∧

This rule simply states we can combine a proof of with a proof of to produce a proof of ∧ . We can also formulate a system with many axioms and just a few rules, generally just modus ponens plus some rules for the logical quantifiers. In proof systems like this, the previous rule becomes the axiom ⇒ ⇒ ∧ . We can combine this axiom with a proof of and a proof of to produce a proof of ∧ using modus ponens as the only rule. . . . . . . . .

⇒ ⇒ ∧ ⇒ ∧ ∧

What this shows is that we can often turn rules into axioms and vice versa. For some purposes it is more convenient to have a logic with few rules and many axioms, because this means there are few inductive cases to verify. For other purposes it is more convenient to have a logic with many rules and few axioms (often only ⊢ ) because this makes proof search easier, and also because some logically desirable properties can be more easily proved (such as consistency and the subformula property).

Ideally, a logic has both a proof theory and a model theory related by soundness and completeness proofs. These proofs relate model theory to proof theory by proving that is derivable if and only if it is true in all models. We can therefore switch between proof theory and model theory in different ways. Instead of showing is not provable, we can construct a model where is false (a countermodel).

In what follows, we will only consider logics which are both sound and complete. Soundness and completeness allow us to switch between model theory and proof theory as shown below. Remark that 4 and 5 are simply the negations of 2 and 3. Equivalence 5 shows that we can show satisfiability of by showing that ¬ is not provable, exploiting the standard logical definition of '∃' as '¬∀¬'.

⊢ ⟺ ∀. ⊨ (2) ⊬ ⟺ ∃. ⊨ ¬ (3) ⊢ ¬ ⟺ ∀. ⊨ ¬ (4) ⊬ ¬ ⟺ ∃. ⊨ (5)
But what about the models themselves? These are structures and quite different objects from proofs. There are elementary model-theoretic results which allow us to translate formulas to models and models to formulas. A model corresponds to a set of atomic formulas and vice versa (Hodges 1997, Chapter 1). The model  of example 1 corresponds to the following set of atomic formulas (the set of all atomic formulas which are true in ).

{ John( ), sleeps( ), NP( ), VP( ), S( ), cat( , ), cat( , ), head( , ), subj( , ) }
The only complication here is that the set of atomic formulas corresponding to a model might not be finite (this is obvious when we look at models of Peano arithmetic for the natural numbers). We can turn this set into a single formula using conjunction.

= 1 ∧ … ∧ , and we then have ⊢ ∃ .NP( ) as the proof theoretic counterpart of  ⊨ ∃ .NP( ).

The things to remember are that model theory and proof theory are different ways to study the same objects, and while some things are easier to prove using model theory and others using proof theory, we can move between model theory and proof theory rather easily: instead of showing there is a model of , we can instead show that ¬ has no proofs. In many cases, we can also switch back and forth between models and formulas, and between rules and axioms.

Proof-theoretic grammars, model-theoretic grammars, and their differences

We should be precise about the distinction between model-theoretic grammars and generative-enumerativegrammars -I prefer term proof-theoretic grammars to generateenumerative grammars and will treat these terms as synonymous throughout this article.

Although the term model-theoretic syntax had been used before, the contrast between was most clearly developed by [START_REF] Pullum | On the distinction between model-theoretic and generative-enumerative syntactic frameworks[END_REF].

Proof-theoretic grammar A 'generative' grammar according to Pullum (2020, Section 1, p. 4) is any grammar specifying syntactic structures in the following way.

1. a set of one or more relevant objects [which is] given initially, 2. a set of operations for constructing new objects from those already available.

Rephrased more succinctly, proof-theoretic theoretic grammars define syntactic structures inductively.

Model-theoretic grammar A model-theoretic grammar, again according to Pullum (2020, Section 3), is defined as follows.

1. a grammar is a set of logical postulates or axioms (Pullum often uses the word 'constraints'),

2. syntactic structures are exactly those structures which satisfy these postulates.

In other words, model-theoretic syntax defines grammars as a logical theory and is interested in the structures which satisfy the postulates of this theory. It is important to emphasise that these definitions do not provide a dichotomy: a grammar can be both model-theoretic and proof-theoretic, or neither. For example, a formalism specifying transderivational constraints is neither proof-theoretic nor model-theoretic1 , and a model-theoretic formalism whose structures can be inductively defined is both modeltheoretic and proof-theoretic.

Key differences

Since nearly all proof-theoretic grammars can be seen as logical theories as well, the main difference is that model-theoretic grammars are satisfaction based rather than validity based. For model-theoretic grammars, the basic question is "what are the models which satisfy our axioms?" and these models are our basic linguistic structures, for proof-theoretic grammars it is "what can we derive using our axioms?", and these derivations are our basic linguistic structures. Stating things in the same terms, linguistic structures in model-theoretic syntax are true in some model, whereas linguistic structures in proof-theoretic syntax are true in all models.

More precisely, in an MTS grammar specified as a set of axioms  = 1 , … , , the grammatical syntactic structures of this grammar are the  such that  satisfies all of the , i.e.  ⊨ 1 ∧ … ∧ . In a proof-theoretic grammar, given a logical theory  , the syntactic structures are exactly the derivable statements in the logic, that is, the set of such that  ⊢ .

In a satisfaction-based theory, like MTS, we start by allowing everything permitted by the signature of our logic, then prohibit more and more by adding axioms. In a validity-based theory, we start by deriving only ⊢ , and adding rules and axioms allows us to derive more and more.

Another key difference is the internal versus the external perspective. In prooftheoretic syntax, our derivations are our syntactic structures, whereas in model-theoretic syntax, our axioms describe these structures (Pullum 2013a, p. 498) 1 gives a summary overview of the differences between the proof-theoretic and model-theoretic perspective. Most of these are simple consequences of the initial difference between validity and satisfaction. For example, in proof-theoretic syntax finding proofs of the form  ⊢ is used for parsing, whereas in model-theoretic syntax it is used to derive grammatical principles from the axioms, as done on many occasions by [START_REF] Johnson | Arc pair grammar[END_REF]. In a proof-theoretic formalism, grammatical principles correspond to theorems about derivations, that is, we prove properties which hold of all derivations, generally by induction on their structure.

Another difference is that while for proof-theoretic grammars, parsing is simply a form of proof search (parsing-as-deduction), model-theoretic grammars do not have such a direct way to decide whether a sentence is grammatical or not. Their main focus is deciding whether a fully specified structure satisfies all axioms (and this can be very inefficient: proof checking is easy, but model checking is at least PSPACE-complete for most of the standard logics used for MTS). There are a number of strategies we could follow for deciding whether a string is grammatical in a model-theoretic framework.

• Model building. Generate all possible structures with the given words as its yield, for example as done by [START_REF] Palm | Parsing complexity and model-theoretic syntax[END_REF].

• Theorem proving. Keep the grammar as it is, and code the input string as a formula. For a grammar  and an input string coded as , we try to prove ¬( ∧  ).

If we find a proof, the sentence is ungrammatical: the sentence contradicts the grammatical theory. If this fails, we can construct a model from the structure of the failed proof. This essentially the approach used by Palm ( 2004) using temporal logic. Appendix A presents a version of this theorem proving approach using first-order logic. Theorem proving for first-order logic or MSO is of course undecidable. While MSO has some important decidable fragments, these are deeply intractable: even when we restrict ourselves to MSO over regular string languages, theorem proving has non-elementary complexity2 .

• Grammar translation. Translate the grammar into a proof-theoretic grammar and use theorem proving. This is the approach of [START_REF] Morawietz | Two-step approaches to natural language formalisms[END_REF], who translates a model-theoretic grammar written in MSO to a tree automaton. This compilation step is still non-elementary, but parsing is then linear.

There is also a difference in the way we determine how many structures are generated by our grammatical theory. For a proof-theoretic grammar, we simply use the inductive definition, and in many cases there will be a countably infinite number of structures in our grammar. However, these are theorems obtained by analysing our logic, not principles imposed on it from outside. For model theory, the analysis of the number of (non-isomorphic) models of a theory is called 'spectrum theory' [START_REF] Shelah | Classification theory and the number of nonisomorphic models[END_REF].

As we will see in what follows, the main problems with the comparison between proof-theoretic and model-theoretic syntax of [START_REF] Pullum | On the distinction between model-theoretic and generative-enumerative syntactic frameworks[END_REF] is that their criticism are either at the wrong level or do not distinguish in any meaningful way between model-theoretic and proof-theoretic grammars.

Model theory, proof theory, and natural language

There are two distinct ways to view model-theoretic syntax, a weak and a strong version.

• Weak MTS. The grammar has a proof-theoretic, inductive backbone generating candidate structures, with a set of axioms filtering out ill-formed ones. Or, alternatively, model-theoretic syntax and proof-theoretic syntax are merely different perspectives on the same structures.

• Strong MTS. There is no proof-theoretic backbone generating candidate structures, only axioms specifying properties of the allowed structures.

Weak MTS is essentially proof-theoretic syntax with constraints, or an alternative way to see the structures generated by proof-theoretic syntax. Pullum (2013a) makes a similar distinction, claiming that Government and Binding theory and Generalised Phrase Structure Grammar (GPSG) are 'hybrid' (weak MTS in my terms) whereas Head-driven Phrase Structure Grammar (HPSG) and Arc Pair Grammar, again according to Pullum, are 'clear examples of the MTS perspective' (strong MTS in my terms). Pullum argues in favour of strong MTS, but even his 'clear examples' are quite obviously instances of weak MTS.

Strong MTS grammars, because of the absence of inductively defined structures, exhibit 'structural holism'. The structures generated by model-theoretic grammars are not built up from basic objects and operations combining these, since that would make the grammar proof-theoretic 3 . This means that model-theoretic syntax, at least when it is not at the same time proof-theoretic syntax, has no inductive structure, and grammatical correctness is a holistic property of structures. The only clear example of strong MTS in Pullum's writings is the idea of expressing grammars by forbidden configurations of trees or strings [START_REF] Pullum | What grammars are, or ought to be[END_REF]. This is an interesting idea which would deserve to be further developed, opening up connections with graph minor theory from theoretical computer science [START_REF] Robertson | Graph minors XX. Wagner's conjecture[END_REF]. Even then, I consider it quite likely that grammars so developed would also be proof-theoretic (e.g. by taking the complement).

Since the definition of proof-theoretic grammar is any grammar formalism where linguistic structure can be defined inductively (possibly augmented with some constraints in the weak MTS perspective), this makes it quite hard to show that a grammar is not proof-theoretic, because this amounts to showing that there is no inductive structure to grammatical objects. Remember that it is quite irrelevant whether the inductive structure is specified using rules or using axioms. But there are easy ways of showing a grammar is proof-theoretic: a formalism which has any of the standard notions of constituency, dependency, or dominance is proof-theoretic, since these are all ways of defining structures inductively. An easy diagnostic is the following: if the formalism has an Earley-type or CKY-type parsing algorithm, then it is proof-theoretic.

When we look at HPSG, it has a clear generative backbone: there are basic objects defined in the lexicon and operations for creating new objects from already defined ones, such as the head-subject, head-specifier, and the head-complement principle. These principles are all tree construction rules, and clearly presented as such in the authoritative textbooks [START_REF] Pollard | Head-Driven Phrase Structure Grammar[END_REF], Section 1.5), (Sag, Wasow & Bender 1999, Section 4.5). Even the versions of HPSG Pullum designates as clearly model-theoretic have such a proof-theoretic backbone.

Arc pair grammars have a clear inductive structure as well, and their grammatical objects can be seen as a type of (multiple overlapping) constituent trees with additional edges (and relations between those edges). For example, we find notions of constituent structures and principles stating that clauses are trees headed by verbs (Johnson & Postal 1980, PN Law 35, p. 212).

Similarly, Property grammars can be seen as inductively constructing constituent trees4 with some additional edges for representing precedence [START_REF] Blache | Model-theoretic syntax: property grammars, status and directions, in 'Constraints and Language[END_REF].

The problem with this is that most of the arguments against proof-theoretic syntax are actually arguments against inductively defined structures, that is, arguments in favour of structural holism. This means that whatever arguments are presented against inductively defined structures, they apply with equal force to HPSG, Arc Pair grammars and Property grammars, but perhaps not to a strong MTS formalism which might be proposed in the future.

Proof-theoretic syntax

Before discussing Pullum's criticisms in detail, I will present a version of proof-theoretic syntax. This will give a concrete formalism to help with later discussion.

The logic I will present is the Lambek calculus [START_REF] Lambek | The mathematics of sentence structure[END_REF]). Even though it has its known limitations, is it simple enough to allow a discussion with concrete examples and I will refer the reader elsewhere for a discussion of the different variants and extensions of the Lambek calculus and their linguistic applications [START_REF] Moortgat | Typelogical grammar[END_REF][START_REF] Morrill | The Displacement calculus[END_REF][START_REF] Barker | Continuations and Natural Language[END_REF][START_REF] Kubota | Type-Logical Syntax[END_REF][START_REF] Moot | Type-logical investigations: proof-theoretic, computational and linguistic aspects of modern type-logical grammars[END_REF]. The generic name for these formalisms is type-logical grammars.

⊢ Ax Γ ⊢ ∕ Δ ⊢ Γ, Δ ⊢ ∕ Γ, ⊢ Γ ⊢ ∕ ∕ Γ ⊢ Δ ⊢ ∖ Γ, Δ ⊢ ∖ , Γ ⊢ Γ ⊢ ∖ ∖ Figure 1: Lambek natural deduction rules
In a sense, type-logical grammars are the purest examples of proof-theoretic syntax, because the syntactic theories of type-logical grammars are logics rather than logical theories.

Figure 1 presents the logical rules for the Lambek calculus in natural deduction format. There is a single axiom ⊢ and only four rules 5 , two for each connective.

The elimination rules are a form of modus ponens: from together with entails we derive . However, our logic is resource conscious (that is, we care how many occurrences of each formula there are) and sensitive to direction. We therefore have two implications ∕ , which combines with a to its right to form an , and ∖ which combines with a to its left to form an .

We can then paraphrase the ∕ rule as follows: if we have derived some structure Γ to be of type ∕ and some other structure Δ to be of type , then the concatenation of these two structures Γ, Δ is of type . The ∖ rule is symmetric.

For the ∖ rule, if , Γ is a list of formulas from which we can derive , then when we remove from the list, we can derive ∖ . This is the deduction theorem in Hilbert-style formulations of logics: if from Γ and we can derive , then from Γ alone, we can derive entails . In this case, if , Γ derives , then Γ alone derives ∖ , that is, something missing a to its left to form an .

Model theory

Even though this is a purely proof-theoretic interpretation of the logic, the Lambek calculus has a very natural semigroup interpretation for which it is sound and complete [START_REF] Pentus | Models for the lambek calculus[END_REF]. If is a set and '•' is the binary semigroup operation over elements of , then formulas are interpreted as follows.

( ) ⊆ (6) ( ∖ ) = { | ∀ ∈ ( ) • ∈ ( )} (7) ( ∕ ) = { | ∀ ∈ ( ) • ∈ ( )} (8)
Atomic formulas are interpreted as subsets of . The interpretation of ∖ is the set of those such that for every in the interpretation of , • is in the interpretation of . In other words, the objects in ∖ are exactly the things which can be combined with any object in (to their left) to produce an . The interpretation of ∕ is symmetric.

This result is much more profound than it appears at first sight: the Lambek calculus is a logic over strings, and it is sound and complete when interpreted over semigroups. From the point of view of mathematical logic, it is very desirable to have simple, wellunderstood mathematical objects as models for our logic6 .

Logic and grammar

For the Lambek calculus, and type-logical grammars in general, the lexicon is simply a set-valued function from words to formulas. While we will return to the lexicon and lexical dependance in Section 4.3, for now we will simply note that the lexicon is not a part of the logic.

A tiny lexicon is presented below.

Lex(he) = np Lex(John) = np Lex(him) = np Lex(chair) = n Lex(likes) = (np∖s)∕np Lex(of) = (n∖n)∕np Lex(is) = (np∖s)∕np Lex(his) = np∕n Lex(are) = (np∖s)∕np Lex('s) = (np∖np)∕n Lex(the) = np∕n Lex(department) = n
Using this lexicon, we can find the following derivation for "John is the chair of his department". Even though this proof is more readable, it is isomorphic to the original proof, at least when the lexical assignments have been given.

Terms and features

We can extend the Lambek calculus with some restricted form of linguistic features by using the first-order quantifiers. To keep the logic simple, we only use implicit quantification here.

In the logic, this only changes the elimination rules. When combining ∕ and ′ for the ∕ rule, we compute the most general unifier of and ′ and do a global substitution for the computed unifier. This is standard methodology for theorem proving in first-order logic [START_REF] Fitting | First-order logic and automated theorem proving[END_REF].

Γ ⊢ ∕ Δ ⊢ ′ Γ, Δ ⊢ ∕ Γ ⊢ ′ Δ ⊢ ∖ Γ, Δ ⊢ ∖
This allows us to give a simple analysis of "John likes coffee" as follows.

John ⊢ np(3, sing, )

likes ⊢ (np(3, sing, nom)∖s(fin))∕np( , , acc) coffee ⊢ np(3, sing, ) likes coffee ⊢ np(3, sing, nom)∖s(fin) ∕

John likes coffee ⊢ s(fin) ∖

We have kept the variables from the lexical entries in place. Unification of np( , , acc) with np(3, sing, ) for the ∕ rule produces = 3, = sing and = acc, whereas unification of np(3, sing, ) with np(3, sing, nom) produces = nom.

Structural rules, linear logic, intuitionistic logic

We can also extend the Lambek calculus with a number of structural rules, which operate on the list of formulas in the antecedent. Figure 2 lists the standard structural rules which connect the Lambek calculus to other logics. The permutation rule, [ ], allows us to swap the order of two adjacent formulas on the list. This turns the antecedent from a list into a multiset, and the logic into intuitionistic linear logic, or the Lambek-van Benthem calculus LP.

The contraction and weakening rules, read from premiss to conclusion, allow us to remove duplicates ( ) and add arbitrary formulas ( ). Adding all three rules turns the logic into intuitionistic logic7 . Given that we are interested in the lambda terms generated by our proofs for computing meaning in the formal semantics tradition of [START_REF] Montague | The proper treatment of quantification in ordinary English[END_REF], intuitionistic logic is the most permissive logic we could use for this purpose, at least when we restrict ourselves to the implicational fragment.

Γ, , , Δ ⊢ Γ, , , Δ ⊢ Γ, , , Δ ⊢ Γ, , Δ ⊢ Γ, Δ ⊢ Γ, , Δ ⊢

Complexity

The complexity of theorem proving for most type-logical grammars is NP-complete, with some of the more expressive formalisms going up to PSPACE-complete. For comparison, the simpler task of model-checking for first-order logic is already PSPACE complete.

Criticisms of proof-theoretic syntax

The next sections discuss the main criticisms of [START_REF] Pullum | On the distinction between model-theoretic and generative-enumerative syntactic frameworks[END_REF] and [START_REF] Pullum | Theorizing about the syntax of human language: a radical alternative to generative formalisms[END_REF] and show how they fail to provide clear advantages for model-theoretic syntax.

Generative holism

As we have seen in Section 2.4, under Pullum's conception of model-theoretic syntax (what I call strong MTS), grammatical structures exhibit 'structural holism': grammatical correctness is a holistic property of structures. Pullum argues that proof-theoretic syntax exhibits what he calls 'generative holism', properties of a grammar are holistic properties of all the combined rules and axioms, and he even argues that "no individual operation says anything about any expression" (Pullum 2020, p. 6).

Let's investigate this more closely. What, to take Pullum's example, does the contextfree rule 9 below entail?

PP → P NP (9)
Pullum's criticism of what this rule does or doesn't say seem focused on some of the powerful operations allowed is some, mostly older, versions of generative grammar, which I have no particular interest in defending. For example, some versions of mainstream generative grammars have operations which necessarily delete or replace some symbols. However, this criticism is of highly specific operations in one type of formalism. It is therefore odd to see this criticism as part of a list of "unavoidable side effects of the deepest aspects of the generative type of formalism itself" (Pullum 2020, ibid).

But when we look at context-free grammars, this rule does make a number of claims: there are prepositional phrases, and some of these consist of a prepositional phrase followed by a noun phrase8 .

Another way to interpret this rule is as stating that the following local tree is admissible in our grammar [START_REF] Mccawley | Concerning the base component of a transformational grammar[END_REF]).

PP NP P

A final way to see 9 is as the following logical axiom.

∀ .[P( ) ∧ NP( ) ⇒ PP( + )]

(10) This is another standard interpretation of our example context-free rule, where the '+' infix function symbol denotes string concatenation. It states that if string is a preposition and string a noun phrase, then their concatenation is a prepositional phrase. Pullum claims the following example, which expresses part of rule 9 model-theoretically, is superior.

∀ .[PP( ) ⇒ ∃ .[Head( , ) ∧ P( )]] (11)
First of all, while there are differences in the type of things that 10 and 11 express, these differences are difference in grammar design and how we encode certain grammatical properties in our logic. Nothing specific with respect to model theory or proof theory can be said when we see one of these formulas in isolation.

We can also criticise 11 in ways rather similar to Pullum's critique of 9: this axiom is compatible with structures where prepositions and prepositional phrases are identical (i.e. the axiom allows = ), it is compatible with structures where prepositions have multiple heads (i.e. are not trees), it is compatible with structures were Head( , ) holds, and it is compatible with structures containing a path of countably infinite length between and . Excluding these structures requires knowledge of the other axioms. In other words, just like for the proof-theoretic versions, many properties of the grammar can only be determined globally, exhibiting a similar type of 'holism' if this is the term you want to use for it. In axiomatic systems, especially systems with many axioms, the individual axioms often make sense only when we know the intended interpretation of the predicate and function symbols, and when we have studied how this axiom interacts with the other axioms. One of the main reasons why proof theorists look for ways to replace axioms with rules as much as possible is to avoid such unintended interactions [START_REF] Gentzen | Untersuchungen über das logische Schließen[END_REF][START_REF] Dowek | Theorem proving modulo[END_REF][START_REF] Burel | First-order automated reasoning with theories: when deduction modulo theory meets practice[END_REF].

In the proof-theoretic context of Section 3, assigning a formula (np∖s)∕np to a word like "is" means this formula will necessarily occur in a subproof of the following form (for some structures and ). . . . .

⊢ np is ⊢ (np∖s)∕np . . . . ⊢ np is ⊢ np∖s ∕ is ⊢ s ∖
We can make very precise claims about the shape of the proofs in which formulas in type-logical grammars occur. There is a useful interpretation of proofs in type-logical grammars where each formula corresponds to a 'constraint' (of the type shown above) on the proofs it can be a part of, and proofs correspond to the simultaneous satisfaction of all these constraints. In spite of what this terminology might suggest, this approach is fully proof-theoretic [START_REF] Moot | Type-logical investigations: proof-theoretic, computational and linguistic aspects of modern type-logical grammars[END_REF].

The general point appears to be fairly trivial: there are some properties about prooftheoretic grammars which are harder to prove than for an equivalent model-theoretic grammar, requiring reference to the entire grammar. But this point is not very deep, as there are other properties which are easier to prove about proof-theoretic grammars. When a grammar writer adds subject-verb agreement as an axiom, it seems odd to then congratulate him about how easy it is to show the structures defined by his grammar satisfy subject-verb agreement.

Gradience

One of the main arguments against proof-theoretic syntax is the often repeated claim that these formalisms necessarily impose sharp boundaries, whereas model-theoretic syntax provides a simple account of gradience since it can make some of its axioms optional.

In this way, model-theoretic syntax can then define multiple boundaries: the fully grammatical structures, satisfying all axioms, the structures not satisfying one axiom but satisfying all the others, etc. In proof-theoretic syntax, when seen as a set of axioms, removing axioms means less sentences are derivable, so we would have to add axioms. The argument then appears to be that it is easier to remove axioms than to add them, which is something I can agree with. However, if adding axioms is hard, then grammar learning is hard (we will briefly return to grammar learning in Section 5.1).

From a more formal perspective the problem looks as follows. Take a theory  and a structure with corresponding formula . In the model-theoretic, satisfaction-based context we have ⊭  (that is, is not grammatical for our theory) and we look for the largest  ′ ⊂  such that ⊨  ′ . The advantage of the model-theoretic case is that these  ′ can be enumerated. In the proof-theoretic, validity-based context we have  ⊬ and we look for the smallest  ′ ⊃  such that  ′ ⊢ (we should also verify that  ′ is consistent, i.e.  ′ ⊬⟂). We can reformulate this as looking for the smallest formula such that  ∧ ⊢ . Logically, the proof-theoretic case is a type of abduction, and there are solutions for finding the formula from the failed proof of  ⊬ , essentially by computing the minimal formulas needed to close the open branches in a tableau proof [START_REF] Mayer | First order abduction via tableau and sequent calculi[END_REF].

However, there is a much simpler solution. First, it is important to remember that model-theoretic syntax defines gradience over structures. Given a structure, a modeltheoretic grammar can then indicate, for each axiom, whether it is satisfied or violated.

This notion is easily adapted to the proof-theoretic context: like the model-theoretic case, we look at a structure then mark any local subtree which does not correspond to any of our rules as incorrect. This gives a rather similar notion of gradience as the one advocated for the model-theoretic case. We have the structures where all rule applications are correct, we have those where exactly one application is incorrect, etc. In this scenario, gradience is a form of proof checking, in the same way that it is a form of model checking for MTS.

Pullum's remark that such a structure is not generated is completely besides the point: it confuses parsing/theorem proving with proof checking. He himself simply assumes fully specified structures are given as input to his grammars, and we similarly assume a fully specified proof candidate is given for evaluation to our proof checker. We should either compare model checking with proof checking, as we do here, or model building with theorem proving. We will see below that it is fairly easy to set up a prooftheoretic syntax in such a way that we can generate ungrammatical sentences, thereby giving an account of gradience which operates on strings.

I will illustrate this in the context to categorial grammars by taking Pullum's examples of successively worse versions of "He is the chair of his department", repeated below, complete with his error counts.

(1) a.

He is the chair of his department. b.

* He are the chair of his department.

( (5 errors)

Starting with example (1-b), there is a unification failure between "he" and "are" either of number sing ≠ plur or of person 2 ≠ 3. This can be handled by the basic treatment of features in the Lambek calculus introduced before, giving the following schematic proof for "he are" with the ∖ rule marked as incorrect because of the unification failure. The proposal I sketched here adequately accounts for the desired degrees of granularity, it allows us point to where specific rules are incorrectly applied, and the approach is fully constructive and local.

Gradience and proof search

We have only compared proof checking with model checking in our discussion so far, which is a comparison at the same level. We will now investigate how to handle gradience in proof search. Given that removing axioms in model-theoretic syntax amounts to adding rules in proof-theoretic syntax, or at least relaxing their conditions, this points to a fairly obvious solution.

A simple candidate rule for relaxing derivability would be the permutation rule [ ] of Figure 2. We can even add the contraction and weakening rule, and some non-logical axioms between atomic formulas (e.g. n ⊢ np) without affecting decidability. Similarly, instead of incorporating unification into the ∕ and ∖ rules, we treat unification of the arguments as a side condition to the rule to be verified when the proof is completed.

This gives us a logic for generating proof candidates, with Lambek calculus proofs as a proper subset. We can then use a standard proof search procedure to obtain proofs, combined with a proof checking mechanism to verify the generated proofs are Lambek calculus proofs like we did in the previous section.

The complexity of proof search remains NP-complete when adding commutativity, which compares very favourably to parsing in model-theoretic frameworks.

Obviously, some work is needed to turn this into a fully-fledged theory of gradience: permutations degrade the acceptability of a sentence very rapidly, and weakening appears acceptable mostly in cases of self-correction. However, all that I needed to show here is that gradience can be treated in a proof-theoretic formalism, and that this does not require us to abandon any of the foundational assumptions of proof-theoretic syntax.

Gradience in model-theoretic syntax

The basic idea of handling gradience in model-theoretic syntax is making axioms optional. While this sounds simple enough, it is not enough on its own to make accurate predictions. Pullum apparently believes this is trivial, since he doesn't give the slightest indication of how structures (grammatical or not) are generated from strings or how he intends to obtain the error scores for his example sentences. If we model subject-verb agreement by an axiom of the schematic form shown in 12 below, then this axiom is satisfied by example (1-b), simply because the antecedent of the material implication is false. The result will be that we obtain a forest consisting of two trees, one with root NP and one with root VP, but we have no idea where a constraint was violated (in general, when an axiom with an existential quantifier is not satisfied, we cannot say where).

∀ .[NP( , …) ∧ VP( , …) ⇒ S(…)] (12)
We can change 12 to the slightly more complicated 13 below, but then we will have the same problem when we use backward chaining proof search (or a top-down parser).

∀ .[NP( , …) ∧ VP( , …) ⇒ S(…) ∧ = ] (13)
So even getting subject-verb agreement correct requires careful engineering of the axioms, and knowledge of the algorithm used for generating partially correct structures. For a vivid example showing why model-theoretic syntax does not have a fundamental advantage over proof-theoretic syntax, take the string "of the and a but through or", which [START_REF] Pullum | On the distinction between model-theoretic and generative-enumerative syntactic frameworks[END_REF] rightfully consider to be 'complete gibberish'. It has the following model-theoretic analysis. When we analyse the string like this, it violates only a single tree axiom, namely 1 from Rogers (1998) which stipulates the existence of a node which dominates all others. Other than that, every word is assigned a syntactic category. It satisfies several other axioms as well: all prepositional phrases have a preposition as their head, all coordinate structures have a coordinator. All these axioms are vacuously satisfied, of course, but this is the way it should be. It is not clear what type of principle should be added to make this structure violate more axioms: when we add an axiom requiring a vertex to have a parent, we always make an exception for the root node. We could restrict the categories allowed for the root node, we could also require sister or parent nodes for certain categories, but in either case the treatment of fragments would disappear.

Since this structure violates only a single axiom, it should therefore be comparable in grammaticalness to other structures violating a single axiom, such as "He are the chair of his department" or "his and my book"

The problem with the model-theoretic approach to gradience is that when axioms become mere suggestions, then the structure satisfying the greatest amount of these suggestions might actually be a quite impoverished one. It is therefore no coincidence that researchers who have experimented with gradience in model-theoretic syntax use, first of all, a proof-theoretic base grammar to generate candidate structures inductively, but also much more sophisticated machinery to compute an acceptability score, essentially a type of percentage of constraints satisfied among those which could potentially apply [START_REF] Blache | Gradience, constructions and constraint systems[END_REF], and weighted axioms [START_REF] Duchier | A model-theoretic framework for grammaticality judgements[END_REF]. So while some excellent work has been done on gradience in model-theoretic syntax, it needs some fairly complex calculations, weights, and a proof-theoretic backbone.

So in spite of giving the impression of being a strong argument in favour of modeltheoretic syntax seen from an abstract, high level, this is only because the comparison is at the wrong level and details of empirical evaluation are conveniently ignored. Modeltheoretic syntax has no advantages over proof-theoretic syntax when we compare them at the same level, or when we look in detail at concrete examples.

Lexical dependence

The final main claim of Pullum, which he calls "devastating", is that proof-theoretic syntax is necessarily dependant on the lexicon whereas model-theoretic syntax is not.

The claim that proof-theoretic syntax is necessarily dependant on the lexicon is certainly true in a boring way: the definitions of many grammar formalisms generally start by specifying an explicit signature Σ. These basic units of a grammar formalism need not be words: they can be smaller units (morphemes, phonemes, characters) or abstract categories like part-of-speech tags. But in the same way, whatever logical formalism is used for a model-theoretic approach, an alphabet and a signature are generally required. So if we want to analyse "Pirots karulize elatically" in any way, our logical signature needs all these symbols in its alphabet to assign them to nodes in the structure: an expression like karulize( ) is a well-formed formula only when karulize is a unary predicate symbol in our logic. In other words, a model-theoretic grammar cannot say anything about "karulize" because it is not even in the language.

This may seem pedantic, but just like most logic texts only specify an explicit signature for some of their more basic examples, so do most formal grammars (and prooftheoretic grammars) only specify an explicit terminal alphabet for some toy grammars.

Pullum proposes to analyse phrases containing invented words by simply assuming there is some morphological process assigning "Pirots karulize elatically" the correct NP V Adv part-of-speech tags. However, once we have the part-of-speech tags, we can use a proof-theoretic grammar to analyse it, and whatever mechanism is used for assigning these part-of-speech tags, for Pullum's argument to be valid, he must show that such an assignment is necessarily model-theoretic.

For example, we could add rules like the following to our grammar.

∀ , . string( , + s) ⇒ postag( , NP(pl)) ∧ meaning( , (NP(pl), ))

(14) ∀ , . string( , + ize) ⇒ postag( , V(3 )) ∧ meaning( , (V, )) (15) ∀ , . string( , + ally) ⇒ postag( , ADV) ∧ meaning( , (ADV, )) (16)
In the rules above, is a vertex, a string, and + the string concatenation operation, postag assigns a part-of-speech tag to a vertex, and meaning assigns a meaning to a vertex, while is a function computing a meaning given part-of-speech tags and the root (the details of this function are up to the grammar designer). Rule 14 can informally be summarised as stating that words ending with the suffix "s" can be plural noun phrases. Similarly, rule 15 states that words with root and suffix "ize" can be third-person singular verbs, and rule 16 states that words with suffix "ally" can be adverbs 10 .

Even when adding the above rules to a model-theoretic grammar, "pirot", "karul" or "elatic" are possible as values for only when we have made these terms part of the signature of our language in advance.

For words not appearing in the lexicon, the following strategies (and many combinations) are possible.

1. Part-of-speech tagging. In computational linguistics, part-of-speech tagging is a task which has been considered solved for a long time. This allows us to use the following strategy for the lexicon: if the word is not in the lexicon, we simply use its part-of-speech tag in the grammar. This is again completely orthogonal to model-theoretic or proof-theoretic syntax, and Pullum (2020) uses this strategy himself without comment or reflection.

2. Change the lexical units. Our lexical entries can contain units other than fully inflected words. Our lexical entries can instead be morphemes, phonemes or characters (part-of-speech tags, as suggested by solution 1, can be another possibility).

3. Machine learning. While Pullum & Scholz (2001) are mostly right about rejecting statistics/machine learning for gradience, machine learning has achieved stunning successes for resolving lexical ambiguity (so-called supertagging) and a side-effect of this is that we can assign complex lexical assignments to unknown words without problem [START_REF] Bangalore | Supertagging: Using Complex Lexical Descriptions in Natural Language Processing[END_REF], this explicitly includes typelogical grammars [START_REF] Kogkalidis | Geometry-aware supertagging with heterogeneous dynamic convolutions[END_REF].

4.

Inference. In type-logical grammars, we can in many cases simply solve for the unknowns analytically [START_REF] Moortgat | Categorial Investigations: Logical and Linguistic Aspects of The Lambek Calculus[END_REF][START_REF] Emms | Parsing with polymorphism[END_REF][START_REF] Mirzapour | Finding missing categories in incomplete utterances[END_REF]).

5. Default rules. These are rules like 14 to 16 above where, when no more specific rule is found, we use a generic rule as backup. Some logics -non-monotonic logic, default logic -have been developed for cases much like this.

6. Parameters. In model theory, we can extend our structure with parameters, essentially a type of additional constants. It is possible to argue that "pirots" is a parameter. However, this amounts to admitting our grammar doesn't have anything to say about this word. Using parameters is morally equivalent to the proof-theoretic solution of [START_REF] Neeleman | Comments on Pullum[END_REF], who proposed to temporarily add words to the lexicon. Given his comments on this paper, it would be hard for [START_REF] Pullum | Consigning phenomena to performance: A response to Neeleman[END_REF] to consistently advocate for the parameter approach in the model-theoretic context.

So again, if lexical dependence is a problem, then it is a problem for model-theoretic syntax as well, and the different available solutions are not tied to any specific framework.

Minor arguments 5.1 Learnability

There have been a number of results about the learnability of certain classes of language. In a very abstract way, the language learner is exposed to a number of strings in the language, then progressively forms and refines his hypothesis about the structure of the language.

With respect to learnability, the difference between the model-theoretic and prooftheoretic perspective is the following. From the proof-theoretic perspective, the 'blank slate' is where nothing is grammatical, and a grammar is constructed by adding more and more rules or axioms to account for the expressions encountered by the learner. From the model-theoretic perspective, the blank slate is allowing everything, and the learner hypothesises postulates to account for the regularities in the expressions encountered, reducing the allowed structures. Even though Pullum emphasises the negative results about learnability from the proof-theoretic perspective, there have been quite a few positive results as well. So while [START_REF] Gold | Language identification in the limit[END_REF] has shown that there are classes of regular languages which are not learnable according to his theoretical model, [START_REF] Shinohara | Inductive inference from positive data is powerful[END_REF] has shown that even context-sensitive languages are learnable in this paradigm, provided that we impose a bound on the number of rules. There are also quite expressive type-logical grammars which are learnable [START_REF] Costa-Florêncio | Learning Categorial Grammars[END_REF].

This means it is rather up to the proponents of model-theoretic syntax to show learnability of their specific set of axioms, and it is not at all clear how language learners would acquire their logical postulates, or what would cause them to revise a postulate. One possibility is that all these postulates are innate and that the learner simply has to pick and choose postulates from this fixed, innate set, e.g. choose between head first or head final. This is rather similar to the old Principles and Parameters type of learning11 and would therefore not be a point in favour of model-theoretic syntax with respect to its proof-theoretic counterparts.

But there doesn't seem to be any reasonable alternative for model-theoretic syntax. If the learner is allowed to hypothesise any well-formed formula, then it appears exceedingly unlikely that there is a process which converges to something resembling the correct grammar given grammatical strings as input and feedback, positive and/or negative, about the learner's hypothesised grammars and structures. While it is certainly possible that something could be worked out, doing so is a research program, the success of which remains to be determined.

In sum, there are a number learnability results for proof-theoretic syntax, some negative but also some important positive ones. There are no such results, positive or negative, for model-theoretic syntax. I fail to see how anyone can reasonably claim advantages with respect to learnability for model-theoretic syntax.

Fragments

Pullum & Scholz (2001, Section 3.2) claim that proof-theoretic grammars cannot say anything about expression fragments or incomplete expressions, such as "and of the". The argument is rather similar to the gradience argument discussed before: given a structure representing an incomplete expression, a model theoretic grammar can say which axioms it satisfies and which ones it doesn't, Pullum & Scholz are silent about how to produce a structure for a fragment, but proof-theoretic syntax is criticised for failing to produce the structure which is simply assumed as given in the model-theoretic case.

This criticism can therefore be addressed the same way as the gradience criticism: given a proof candidate, we can use a proof checker to verify correct applications of the rules and count the incorrect applications in the same way Pullum & Scholz would count the axioms not satisfied.

However, in the case of the Lambek calculus, there is an even simpler solution. We can simply compute the formula assigned to "and of the" as follows.

and

⊢ ( ∖ )∕ of ⊢ ∕ the ⊢ ∕ ⊢ the ⊢ ∕ of the ⊢ ∕ and of the ⊢ ∖ ∕ and of the ⊢ ( ∖ )∕ ∕
This is a perfect Lambek calculus proof. We might argue that the proof should indicate it depends crucially on associativity of the basic logic, but there are simple technical solutions to that [START_REF] Kurtonina | Structural control[END_REF][START_REF] Moortgat | Typelogical grammar[END_REF]. So this is another nonissue.

Finite model theory

Pullum (2020, p. 10) invokes finite model theory as an important logical foundation for research in model-theoretic syntax. I agree that finite model theory is a research area which has revealed many profound connections between logic, complexity theory and formal language theory. I also agree that there are undoubtedly still many connections to explore between finite model theory and research in formal linguistics. However, when it comes to expressing linguistically relevant properties in various logics, many results in finite model theory are negative. For example, if we choose to use first-order logic we cannot express that our graphs are connected, acyclic or trees. Other linguistically useful properties not expressible in first-order logic are queries like "does this phrase contain a gap?". Given that these are some of the most basic types of constraints to impose upon linguistic structures and that all linguistic theories impose at least one of these upon their structures, finite model theory therefore shows first-order logic to be inadequate for expressing natural language grammars. In addition, finite model theory is concerned with model checking and has relatively little to say about model building (parsing).

What are some possible solutions to these negative results?

1. Use a more expressive logic. The most obvious candidate here is monadic secondorder logic (MSO), and several prominent authors in formal linguistics and modeltheoretic syntax have used MSO for modelling natural language [START_REF] Rogers | A Descriptive Approach to Language-Theoretic Complexity[END_REF][START_REF] Morawietz | Two-step approaches to natural language formalisms[END_REF]). An alternative would be to add a form of fixed-point to our logic, essentially using Datalog to write our grammars. However, this means that even the most basic questions such as "is this fully specified structure grammatical according to our logical axioms?" become PSPACE-complete or worse12 .

2. Use a more restrictive logic. Several authors have proposed more restrictive logics, generally some type of modal logic, to deal explicitly with tree structures [START_REF] Blackburn | Linguistics, logic and finite trees[END_REF][START_REF] Palm | Model theoretic syntax and parsing: An application to temporal logic[END_REF]). While this ensures better complexity-theoretic properties than monadic second-order logic, it is unclear whether these logics have the required expressivity for natural language syntax. Some of the most important points of [START_REF] Rogers | A Descriptive Approach to Language-Theoretic Complexity[END_REF] and [START_REF] Morawietz | Two-step approaches to natural language formalisms[END_REF] are the connections they make to standard linguistic theories, thereby showing that MSO has the required expressivity. It remains to be shown that any of these more restricted logics has the expressivity required to implement Pullum's program.

Cardinalities, fixed or not

Pullum ( 2020) is right in claiming that, given a proof-theoretic grammar we can generally decide more or less easily what the size of the given grammar is in terms of the generated objects. In most cases, the number of expressions generated will be countably infinite: all it takes is that the grammar contains a recursive definition which is not primitive recursive. Whether or not there are languages which do not generate an infinite set of strings is ultimately an empirical question, open for reasoned debate. However, where Pullum is wrong is when he claims that model-theoretic syntax is silent about the cardinalities of languages. There has been a fruitful line of work exploring the number of models (up to isomorphism) of theories, and there are many definite answers to these questions [START_REF] Shelah | Classification theory and the number of nonisomorphic models[END_REF]. So in many cases, model-theoretic grammars do make claims about the cardinality of the structures described by a grammar, but they can make claims which are quite different from those expressible in proof-theoretic formalisms.

One important difference is that model-theoretic grammars can define theories which have an uncountable number of models (and several standard theories have many such models), whereas the number of proofs in a proof theory is generally countable. While it is true some authors have argued in favour of natural languages being uncountable [START_REF] Langendoen | The vastness of natural language[END_REF]), these claims depend on a number of assumptions, such as the existence of infinite-length sentences (i.e. length , not simply unbounded), which we can combine using infinitary operations, to successively construct larger and larger uncountable classes. [START_REF] Hart | A critique of 'the vastness of natural languages' by Langendoen and Postal[END_REF] presents a detailed argument about the mathematical problems with the arguments of [START_REF] Langendoen | The vastness of natural language[END_REF]. There are a number of problems with sentences of uncountable lengths 13 . For example, it entails that sentences are not subsets of Σ * (that is, sequences of letters from an alphabet consisting of a finite number of letters or morphemes), and that it is impossible to give a lexicographic ordering on sentences.

When we make the linguistically reasonable restriction to finite models14 , there is no clear distinction between proof theory and model theory for this question.

Conclusions

Might I just be "too conservative to like the idea that MTS offers better theories of linguistic phenomena" [START_REF] Pullum | Consigning phenomena to performance: A response to Neeleman[END_REF])? It's just an idea, and what's up for debate is whether or not it is true, and the weight of the evidence presented in its favour. While the advantages of model-theoretic syntax have been loudly proclaimed since the seminal article of [START_REF] Pullum | On the distinction between model-theoretic and generative-enumerative syntactic frameworks[END_REF], when we look at the much-repeated arguments in favour of model-theoretic syntax, we find that they have little substance on closer examination. This should not surprise anyone skeptical about theoretical advantages unless they are backed up by concrete empirical advantages.

There is no evidence that model-theoretic syntax has the fundamental advantages over proof-theoretic syntax that [START_REF] Pullum | On the distinction between model-theoretic and generative-enumerative syntactic frameworks[END_REF] have been arguing. Indeed, I am skeptical about the most fundamental point that it is possible (or even useful) to define grammatical structures for natural language without using any form of structural induction.

There has been a lot of excellent research done under the banner of model-theoretic syntax, and I hope I will see a lot more of it in the future. But I believe that modeltheoretic proselytism would do better to showcase the actual successes of model-theoretic syntax [START_REF] Rogers | A Descriptive Approach to Language-Theoretic Complexity[END_REF][START_REF] Rogers | wMSO theories as grammar formalisms[END_REF][START_REF] Morawietz | Two-step approaches to natural language formalisms[END_REF]) rather than claiming abstract, high-level advantages which somehow fail to materialise empirically.

Figure 2 :

 2 Figure 2: Structural rules, linear and intuitionistic

  Him are chair of he's department. (3 errors) e. **** Him chair are of he's department. (4 errors) f. ***** Him chair are he's department of.

  .

		PTS	MTS
	basic logical principle	validity	satisfaction
	grammatical objects	derivations	structures
	generated language	derivable statements	structures satisfying the theory
	grammatical principles	theorems about derivations logical consequences of the theory
	grammaticality checking proof checking	satisfaction checking
	parsing	theorem proving	model building, proof theory
	grammar cardinality	proof-theoretic analysis	spectrum theory
	Table 1: A summary of the differences between the proof-theoretic and model-theoretic
	view of syntax
	Table

  While proofs like this are the objects of study for proof theorists, they are not that readable to ordinary humans. It is therefore fairly common in type-logical grammars to use some 'syntactic sugar' and replace formulas on the left hand side of the turnstile by the corresponding word from the lexicon. This gives the following, more readable proof.

		his ⊢ np∕n dept ⊢ n
	John ⊢ np	is ⊢ (np∖s)∕np is the chair of his dept ⊢ np∖s the ⊢ np∕n chair ⊢ n chair of his dept ⊢ n of ⊢ (n∖n)∕np of his dept ⊢ n∖n his dept ⊢ np ∖ ∕ the chair of his dept ⊢ np ∕ John is the chair of his dept ⊢ s ∖	∕

np ⊢ np (np∖s)∕np ⊢ (np∖s)∕np np∕n ⊢ np∕n n ⊢ n (n∖n)∕np ⊢ (n∖n)∕np np∕n ⊢ np∕n n ⊢ n np∕n, n ⊢ np (n∖n)∕np, np∕n, n ⊢ n∖n ∕ n, (n∖n)∕np, np∕n, n ⊢ n ∖ np∕n, n, (n∖n)∕np, np∕n, n ⊢ np ∕ (np∖s)∕np, np∕n, n, (n∖n)∕np, np∕n, n ⊢ np∖s ∕ np, (np∖s)∕np, np∕n, n, (n∖n)∕np, np∕n, n ⊢ s ∖

  However, the permutations which produce reasonable sentences are quite limited: the only other reasonable permutation would be "chair of he's dept are".

	∖ and is therefore counted as an additional error.
	him ⊢ np For example (1-d), it is possible to analyse "he's" as a similar unification failure, by are ⊢ (np∖s)∕np chair ⊢ n of ⊢ (n∖n)∕np his ⊢ np∕n dept ⊢ n he's dept ⊢ np ∕ of he's dept ⊢ n∖n ∕ chair of his dept ⊢ n ∖ chair of his dept ⊢ np * are chair of his dept ⊢ np∖s ∕ him are chair of his dept ⊢ s ∖ * him ⊢ np are ⊢ (np∖s)∕np chair ⊢ n of ⊢ (n∖n)∕np he ⊢ np 's ⊢ np∖(np∕n) he's ⊢ np∕n he's dept ⊢ np ∖ * dept ⊢ n ∕ * he's dept of ⊢ n∖n ∖ chair he's dept of ⊢ n * chair he's dept of ⊢ np ∕ * chair are he's dept of ⊢ np∖s him chair are he's dept of ⊢ s ∖ *	∕
	modelling the "'s" genitive as requiring an uncased noun phrase to its left 9 . This gives
	the following proof.
	he ⊢ np(sing, …) are ⊢ (np∖s)∕np chair ⊢ n ∖ him ⊢ np him ⊢ np of ⊢ (n∖n)∕np he ⊢ np 's ⊢ np∖(np∕n) he's ⊢ np∕n are ⊢ (np∖s)∕np chair ⊢ n of ⊢ (n∖n)∕np he ⊢ np 's ⊢ np∖(np∕n) he's ⊢ np∕n ∖ * dept ⊢ n he's dept ⊢ np ∕ of he's dept ⊢ n∖n ∖ chair of he's dept ⊢ n * chair of he's dept ⊢ np ∕ * chair are of he's dept ⊢ np∖s ∖ * him chair are of he's dept ⊢ s . . . . he are … ⊢ s ∖ * are … ⊢ np(plur, …)∖s Finally, from example (1-e) to (1-f) the topmost starred ∕ essentially becomes a	∕
	For example (1-c), we count the missing determiner counts as an additional error,
	because even when we add a rule like n ⊢ np it would be restricted to plurals.

* dept ⊢ n he's dept ⊢ np ∕ of he's dept ⊢ n∖n ∕ chair of he's dept ⊢ n ∖ chair of he's dept ⊢ np * are chair of he's dept ⊢ np∖s ∕ him are chair of he's dept ⊢ s ∖ * From example (1-d) to (1-e), only the ∕ rule marked with * changes.

In this context, a transderivational constraint would be a proof rule with Γ ⊬ as a premiss, or a model constraint of the type if 1 ⊨  then

⊭  , two different ways of making the grammaticality of a structure/proof depend on the ungrammaticality of another.

More precisely, the complexity is a tower of exponentials, with the height of the tower depending on the number of quantifier alternations, and the topmost exponent depending on the size of the quantifier-free part of the formula[START_REF] Meyer | Weak monadic second order theory of succesor is not elementaryrecursive[END_REF][START_REF] Libkin | Elements of finite model theory[END_REF]).

It is possible to claim that grammatical structures are generated co-inductively instead, but this makes a difference only when we consider the basic linguistic objects to be infinite structures.

Technically, both Arc Pair grammars and Property grammars can be seen as inductively constructing constituent trees which are free trees (that is, acyclic, connected graphs).

[START_REF] Lambek | The mathematics of sentence structure[END_REF] presented a sequent calculus and additional rules for a product connective.

The Lambek calculus also has Kripke models, which are a staple in model theory, and which extend more easily to variants of type-logical grammars[START_REF] Kurtonina | Structural control[END_REF]).

Adding and produces affine logic, adding and a type of relevant logic.

We assume here and elsewhere that neither P nor NP is a 'useless' variable, that is, there are strings in the grammar which derive P and strings which derive NP. This is easy to verify, and grammars containing useless variables can, by elementary transformations, be transformed into simpler grammars without such variables.Note that the same type of criticism can be levelled at model-theoretic versions of this rule, but there it need not be easy to show that there are expressions assigned P and NP.

We can also attribute the error to the morphology component of our grammar, and then count " he's" as incorrect for reasons similar to why we would count "betted" and "curiouser" as wrong.

Such rules would of course need to be refined with some sort of default mechanism to avoid the generation of incorrect forms for irregular plurals e.g. "foots" instead of "feet" and "mans" instead of "men".

I find it quite implausible that something functionally equivalent to the formal apparatus of mainstream generative grammar is innate, and would be similarly skeptical about innate logical postulates, making a possible exception for the tree axioms.

Under the reasonable assumption that the graphs representing linguistic structures are sufficiently treelike, we can compute these queries in linear time, but this requires a compilation of MSO formulas to tree automata. This compilation has non-elementary complexity even when the MSO theory describes a regular string language; more precisely, there is a stack of exponentials whose height is bound by the number of quantifier alternations(Libkin 2004, Chapter 7). This compilation is therefore deeply intractable.Morawietz (2003, Chapter 6) provides a good description of parsing MSO grammars and presents experimental results for compilation of some crucial parts of his grammars.

Uncountable structures are very strange, so we should be careful. A tree with an uncountable number of vertices need not have any uncountable branches nor have an uncountable number of descendants at any specific depth.

When we abandon finite models in first-order logic, the upward Löwenheim-Skolem theorem will immediately give us uncountable models, i.e. fully grammatical sentences with uncountable structures.

We need the tree axioms relating the 'parent' and '<' relations to close the ¬( < ) branch.

A Parsing model-theoretic grammars

Parsing is one of the most important ways to verify the predictions of our grammar: we input a sentence as a sequence of words, and our parser outputs the different structures our grammar predicts for this sentence.

When using model-theoretic grammars, parsing can still be done proof-theoretically. As a simple example, suppose we want to parse "John sleeps". The first step is to code the input string as a logical formula. For example, we can use the formula below.

The relation '<' denotes the linear precedence relation between words, so expresses that there are two nodes (labelled 'John') and (labelled 'sleeps') with preceding , the first word, and the last word. The formula then codes, in a simple way, the linear order on the words of the input sentence.

We can then combine with the simple theory  consisting of axioms 17-19 below.

The relation parent( , ) is true when node is the (immediate) parent of node . Axiom 17 then specifies nodes labelled 'John' have a parent node which is a noun phrase. Some additional axioms are necessary to ensure that nodes are distinct from their parents, and that parents are unique. Axiom 18 specifies that 'sleeps' has a verb phrase parent. Finally, axiom 19 specifies that when is a noun phrase and a verb phrase, with preceding , then they both have a sentence node as parent.

To parse this sentence, we can then either take the model-building road, first constructing all possible 1-vertex models satisfying  ∧ , then all 2-vertex models, etc., until we find a structure with yield 'John sleeps'. To show the sentence is ungrammatical, we do the same for  ∧ ¬ . If our theory has the finite model property, we will either find a model of  ∧ , indicating the sentence is grammatical, or a model of  ∧ ¬ , indicating the sentence is ungrammatical.

We can also parse proof-theoretically. Given this theory  and the formula encoding our input sentence, a tableau prover [START_REF] Fitting | First-order logic and automated theorem proving[END_REF] would produce the following schematic tableau for  ∧ .

Reading the proof from the root upwards, we first remove the existential quantifiers, replacing variables and by constants and , then unfold the conjunctions into their subformulas. We can then expand axiom 17, instantiating to . In a tableau proof, ⇒ is treated as ¬ ∨ , so the implications produces two branches, the left one with ¬John( ), which we can close because John( ) appears in the branch). We unfold the right branch, replacing the existentially quantified by a new variables and removing the conjunctions. We continue with axioms 18 and 19 until no further rules can be applied 15 .

The tableau cannot be closed, which means there is no proof of ¬( ∧ ), and therefore that  ∧ has a model. One of the attractive properties of tableau proof search is that when we fail to find a proof, we can use the constructed tableau to recover a countermodel. In our case, a countermodel of ¬( ∧ ) is a model of  ∧ and therefore a successful syntactic analysis of .

To recover this model, we can simply collect the positive atomic atomic formulas along any open branch, with different open branches corresponding to different models. These positive atomic formulas are enough to construct a model [START_REF] Hodges | A shorter model theory[END_REF]). In the current case these formulas are: John( ), sleeps( ), NP( ), VP( ), S( ) < , < parent( , ), parent( , ),


Guillaume Ducournau

Denis Bacquet

P Szriftgiser

Fabio Pavanello

Emilien Peytavit

Mohammed Zaknoune

Alexandre Beck

Jean-Francois Lampin

Narrow linewidth generation at 1 THz using cascaded Brillouin fiber lasers and quasi-optic UTC-PD

teaching and research institutions in France or abroad, or from public or private research centers.

I. INTRODUCTION

HE generation using photomixing techniques is an efficient way to obtain a tunable THz emission, taking advantage of the large tunability of photonics compared to electronics. Moreover, THz generation using electronic multiplication chains suffers from phase noise degradation, increasing with the order of the harmonic generation (N). The proposed scheme for narrow linewidth THz generation is efficient for any laser wavelength, and the reported performance is < 100 Hz full width at half maximum (FWHM) at 1014 GHz without any stabilization system.

II. CASCADED BRILLOUIN FIBER LASER

The figure 1 shows the cascade Brillouin Fiber Laser (BFL) architecture. BFL are known since a long time to provide a narrow spectral linewidth emission, [START_REF] Stokes | All-fiber stimulated Brillouin ring laser with submilliwatt pump threshold[END_REF][START_REF] Debut | Experimental and theoretical study of linewidth narrowing in Brillouin fiber ring lasers[END_REF]. The outputted Stokes line is red-shifted by around 10 GHz (at 1550 nm) and might be narrower by a factor ~100 to ~1000 with respect to its pump. Such architecture has been used for coherent terahertz wave generation (~1 kHz FWHM) at 316 GHz [START_REF] Ducournau | Highly coherent terahertz wave generation with a dual-frequency Brillouin fiber laser and a 1.55 µm photomixer[END_REF]. The figure 2 shows the spectrum measured using a subharmonic mixer driven by an electrical spectrum analyzer (ESA). ESA intrinsic phase noise is shown for comparison.

Fig. 1 .

 1 Fig. 1. Cascaded Brillouin fiber laser structure. After being amplified by EDFA1, the emission of two distributed feedback laser diodes (DFB1 and DFB2) seeds a first BFL cavity (BFL1). Two narrow Stokes lines are generated and seed a second BFL to be further narrowed. The resulting output is amplified and focused on an UTC photodiode producing a 1 THz line with a < 100 Hz FWHM.

Fig. 2 .

 2 Fig. 2. Measured spectra at 1014.7 GHz, with ESA phase-noise level.III. CONCLUSIONSNarrow bandwidth THz generation is proposed using cascaded BFL above 1 THz, featuring a < 100 Hz FWHM generation.

AKNOWLEDGMENT

This work has been partially supported by the European commission in the framework of MITEPHO Marie Curie program, the "Agence Nationale de la Recherche" in the "WITH" franco-japanese project, Ministry of Higher Education and Research, Nord-Pas de Calais Regional Council and FEDER through the "Contrat de Projets Etat Région "Campus Intelligente Ambiante" (CPER-CIA)", the equipex program "FLUX", Fiber optics for high Fluxes and the "COM'TONIQ" ANR project (grant ANR-13-INFR-0011-01).