In the proof-theoretic semantics approach to meaning, harmony , requiring a balance between introduction-rules (I-rules) and elimination rules (E-rules) within a meaning conferring natural-deduction proof-system, is a central notion. In this paper, we consider two notions of harmony that were proposed in the literature: 1. GE-harmony , requiring a certain form of the E-rules, given the form of the I-rules. 2. Local intrinsic harmony : imposes the existence of certain transformations of derivations, known as reduction and expansion . We propose (...) a construction of the E-rules (in GE-form) from given I-rules, and prove that the constructed rules satisfy also local intrinsic harmony. The construction is based on a classification of I-rules, and constitute an implementation to Gentzen’s (and Pawitz’) remark, that E-rules can be “read off” I-rules. (shrink)

The paper briefly surveys the sentential proof-theoretic semantics for fragment of English. Then, appealing to a version of Frege’s context-principle (specified to fit type-logical grammar), a method is presented for deriving proof-theoretic meanings for sub-sentential phrases, down to lexical units (words). The sentential meaning is decomposed according to the function-argument structure as determined by the type-logical grammar. In doing so, the paper presents a novel proof-theoretic interpretation of simple type, replacing Montague’s model-theoretic type interpretation (in arbitrary Henkin models). The domains (...) of derivations are collections of derivations in the associated “dedicated” natural-deduction proof-system, and functions therein (with no appeal to models, truth-values and elements of a domain). The compositionality of the semantics is analyzed. (shrink)

The paper presents a proof-theoretic semantics (PTS) for a fragment of natural language, providing an alternative to the traditional model-theoretic (Montagovian) semantics (MTS), whereby meanings are truth-condition (in arbitrary models). Instead, meanings are taken as derivability-conditions in a dedicated natural-deduction (ND) proof-system. This semantics is effective (algorithmically decidable), adhering to the meaning as use paradigm, not suffering from several of the criticisms formulated by philosophers of language against MTS as a theory of meaning. In particular, Dummett’s manifestation argument does not (...) obtain, and assertions are always warranted, having grounds of assertion. The proof system is shown to satisfy Dummett’s harmony property, justifying the ND rules as meaning conferring. The semantics is suitable for incorporation into computational linguistics grammars, formulated in type-logical grammar. (shrink)

The paper suggests a revision of the notion of harmony, a major necessary condition in proof-theoretic semantics for a natural-deduction proof-system to qualify as meaning conferring, when moving to a bilateral proof-system. The latter considers both forces of assertion and denial as primitive, and is applied here to positive logics, lacking negation altogether. It is suggested that in addition to the balance between introduction and elimination rules traditionally imposed by harmony, a balance should be imposed also on: negative introduction and (...) elimination rules, and positive and negative introduction rules. The paper suggests a proof-theoretical definition of duality, using which double harmony is defined. The paper proves that in a doubly-harmonious system, the coordination rule, typical to bilateral systems, is admissible. (shrink)

The paper suggests a revision of the notion of harmony, a major necessary condition in proof-theoretic semantics for a natural-deduction proof-system to qualify as meaning conferring, when moving to a bilateral proof-system. The latter considers both forces of assertion and denial as primitive, and is applied here to positive logics, lacking negation altogether. It is suggested that in addition to the balance between (positive) introduction and elimination rules traditionally imposed by harmony, a balance should be imposed also on: (i) negative (...) introduction and elimination rules, and (ii) positive and negative introduction rules. The paper suggests a proof-theoretical definition of duality (not referring to truthtables), using which double harmony is defined. The paper proves that in a doubly-harmonious system, the coordination rule, typical to bilateral systems, is admissible. (shrink)

This paper motivates the logic PCON, an extension of connexivity to conjunction and disjunction, called poly-connexivity. The motivation arises from differences in intonational stress patterns due to focus, where PCON turns out to be a logic of intentionally stressed connectives in focus.

In some presentations of classical and intuitionistic logics, the objectlanguage is assumed to contain (two) truth-value constants: ⊤ (verum) and ⊥ (falsum), that are, respectively, true and false under every bivalent valuation. We are interested to define and study analogical constants ‡, 1 ≤ i ≤ n, that in an arbitrary multi-valued logic over truth-values V = {v1,..., vn} have the truth-value vi under every (multi-valued) valuation. As is well known, the absence or presence of such constants has a significant (...) deductive impact on the logics studied. We define such constants proof-theoretically via their associated I/E-rules in a natural-deduction proof system. In particular, we propose a generalization of the notions of contradiction and explosiveness of a logic to the context of multi-valued logics. (shrink)

The paper proposes a semantic value for the logical constants (connectives and quantifiers) within the framework of proof-theoretic semantics, basic meaning on the introduction rules of a meaning conferring natural deduction proof system. The semantic value is defined based on Fregecontributions” to sentential meanings as determined by the function-argument structure as induced by a type-logical grammar. In doing so, the paper proposes a novel proof-theoretic interpretation of the semantic types, traditionally interpreted in Henkin models. The compositionality of the resulting attribution (...) of semantic values is discussed. Elsewhere, the same method was used for defining proof-theoretic meaning of subsentential phrases in a fragment of natural language. Doing the same for (the simpler and clearer case of) logic sheds more light on the proposal. (shrink)

The paper introduces a variant of connexive logic in which connexivity is extended from the interaction of negation with implication to the interaction of negation also with conjunction and disjunction. The logic is presented by two deductively equivalent methods: an axiomatic one and a natural-deduction one. Both are shown to be complete for a four-valued model theory.

I argue that a recent philosophical interpretation by Jc Beall of the middle value of Weak Kleene logic as ‘being off-topic’ is untenable. My main claim is that “being off-topic” is a relation, not a property, and as such cannot serve as an interpretation of a truth-value.

In this paper, we show how the problem of accounting for the semanticsof temporal preposition phrases (tPPs) leads us to some surprisinginsights into the semantics of temporal expressions ingeneral. Specifically, we argue that a systematic treatment of EnglishtPPs is greatly facilitated if we endow our meaning assignments with context variables, a device which allows a tPP to restrict domainsof quantification arising elsewhere in a sentence. We observe that theuse of context variables implies that tPPs can modify expressions intwo ways, and (...) we use this observation to predict the behaviour of tPPswhose complements are themselves modified by other tPPs. (shrink)

I argue in favour of object languages of logics to be diversely-generated, that is, not having identical immediate sub-formulas. In addition to diversely-generated object languages constituting a more appropriate abstraction of the use of sentential connectives in natural language, I show that such language lead to a simplifications w.r.t. some specific issues: the identity of proofs, the factual equivalence and the Mingle axiom in Relevance logics. I also point out that some of the properties of classical logic based on freely-generated (...) object languagest. (shrink)

We present a number of equivalent calculi for many-valued logics and prove soundness and strong completeness theorems. The calculi are obtained from the truth tables of the logic under consideration in a straightforward manner and there is a natural duality among these calculi. We also prove the cut elimination theorems for the sequent-like systems.

The paper presents a contra-classical dialectic logic, inspired and motivated by Hegel s dialectics. Its axiom schemes are 0.1 Thus, in a sense, this dialectic logic is a kind of “mirror image“ of connexive logic. The informal interpretation of ‘ $$\rightarrow $$ ’ emerging from the above four axiom schemes is not of a conditional (or implication); rather, it is the relation of determination in the presence of truth-value gaps: $$\varphi \rightarrow \psi $$ is read as $$\varphi $$ determines $$\psi (...) $$, namely, necessarily, if $$\varphi $$ is true, then $$\psi $$ is either true or false, not gappy. As far as I know, such a connective has not been considered before in the literature. (shrink)

The paper introduces the formula structure of poly-sequents, allowing the expression of poly-positions: positions with any number of stances, of which bilateralism and trilateralism are special cases. The paper also puts forward the view that s-coherence of such poly-positions can be defined inferentially, without appealing to their validity under interpretations of the object language.

The paper exposes the relevance of permuting conversions (in natural-deduction systems) to the role of such systems in the theory of meaning known as proof-theoretic semantics, by relating permuting conversion to harmony, hitherto related to normalisation only. This is achieved by showing the connection of permuting conversion to the general notion of canonicity, once applied to arbitrary derivations from open assumption. In the course of exposing the relationship of permuting conversions to harmony, a general definition of the former is proposed, (...) generalising the specific cases of disjunction and existential quantifiers considered in the literature. (shrink)

The paper proposes an extension of the definition of a canonical proof, central to proof-theoretic semantics, to a definition of a canonical derivation from open assumptions. The impact of the extension on the definition of (reified) proof-theoretic meaning of logical constants is discussed. The extended definition also sheds light on a puzzle regarding the definition of local-completeness of a natural-deduction proof-system, underlying its harmony.

The paper highlights proof-theoretic semantics as providing natural resources for capturing semantic variation in natural language. The semantic variations include:Distinction between extensional predication and attribution to intensional transitive verbs a non-specific object.Omission of a verbal argument in a transitive verb.Obtaining sameness of meaning of sentences with transitive verbs with omitted object and existentially quantified object.Blocking unwarranted entailments in adjective–noun combinations.Capturing quantifier scope ambiguity.Obtaining context dependent quantifier domain restriction. The proof-theoretic resources employed to capture the above semantic variations include:The use of (...) different kinds of formal parameters and different ways of binding them to predicates.Omission of a premise from a proof-rule.Basing meanings on derivations in meaning-conferring proof-systems.Appealing to substructurality of I/E-rules.Controlling the order of rule applications in derivations.Controlling the open formulas participating in a context within a sequent. (shrink)

The paper studies the extension of harmony and stability, major themes in proof-theoretic semantics, from single-conclusion natural-deduction systems to multiple -conclusions natural-deduction, independently of classical logic. An extension of the method of obtaining harmoniously-induced general elimination rules from given introduction rules is suggested, taking into account sub-structurality. Finally, the reductions and expansions of the multiple -conclusions natural-deduction representation of classical logic are formulated.

We show that the relational semantics of the Lambek calculus, both nonassociative and associative, is also sound and complete for its extension with classical propositional logic. Then, using filtrations, we obtain the finite model property for the nonassociative Lambek calculus extended with classical propositional logic.

Inspired by the grammar of natural language, the paper presents a variant of first-order logic, in which quantifiers are not sentential operators, but are used as subnectors . A quantified term formed by a subnector is an argument of a predicate. The logic is defined by means of a meaning-conferring natural-deduction proof-system, according to the proof-theoretic semantics program. The harmony of the I/E-rules is shown. The paper then presents a translation, called the Frege translation, from the defined logic to standard (...) first-order logic, and shows that the proof-theoretic meanings of both logics coincide. The paper criticizes Frege’s original regimentation of quantified sentences of natural language, and argues for advantages of the proposed variant. (shrink)

This paper develops a version of Natural Logic – an inference system that works directly on natural language syntactic representations, with no intermediate translation to logical formulae. Following work by Sánchez, we develop a small fragment that computes semantic order relations between derivation trees in Categorial Grammar. The proposed system has the following new characteristics: It uses orderings between derivation trees as purely syntactic units, derivable by a formal calculus. The system is extended for conjunctive phenomena like coordination and relative (...) clauses. This allows a simple account of non-monotonic expressions that are reducible to conjunctions of monotonic ones. A decision procedure for provability is developed for a fragment of Natural Logic. (shrink)

The paper introduces a proof-theoretic semantics for adjectival modification as an alternative to the traditional model-theoretic semantics basing meaning on truth-conditions. The paper considers the proof-theoretic meaning of modification by means of the three traditional adjective classes: intersective, subsective and privative. It does so by introducing a meaning-conferring natural-deduction proof system for such modification. The PTS theory of meaning is not polluted by ontological commitments, for example, a scale for beauty and a yardstick for being beautiful. It only uses syntactic (...) artefacts of the proof language. The paper also defines, by suitable rules, iterated modification, shedding light on the relationship between iteration and adjectival classes. Modification via coordinated adjectives is covered too. An appendix delineates briefly the main ingredients of PTS. (shrink)

The paper proposes a semantics for contextual (i.e., Temporal and Locative) Prepositional Phrases (CPPs) like during every meeting, in the garden, when Harry met Sally and where I’m calling from. The semantics is embodied in a multi-modal extension of Combinatory Categoral Grammar (CCG). The grammar allows the strictly monotonic compositional derivation of multiple correct interpretations for “stacked” or multiple CPPs, including interpretations whose scope relations are not what would be expected on standard assumptions about surfacesyntactic command and monotonic derivation. A (...) type-hierarchy of functional modalities plays a crucial role in the specification of the fragment. (shrink)

This paper develops an inference system for natural language within the ‘Natural Logic’ paradigm as advocated by van Benthem, Sánchez and others. The system that we propose is based on the Lambek calculus and works directly on the Curry-Howard counterparts for syntactic representations of natural language, with no intermediate translation to logical formulae. The Lambek -based system we propose extends the system by Fyodorov et~al., which is based on the Ajdukiewicz/Bar-Hillel calculus Bar Hillel,. This enables the system to deal with (...) new kinds of inferences, involving relative clauses, non-constituent coordination, and meaning postulates that involve complex expressions. Basing the system on the Lambek calculus leads to problems with non-normalized proof terms, which are treated by using normalization axioms. (shrink)

In this paper we reexamine the question of whether questions areinherently intensional entities. We do so by proposing a novelextensional theory of questions, based on a re-interpretation of thedomain of t as a bilattice rather than the usual booleaninterpretation. We discuss the adequacy of our theory with respect tothe adequacy criteria imposed on the semantics of questionsby (Groenendijk and Stokhof 1997). We show that the theory is able to account in astraightforward manner for some complex issues in the semantics ofquestions (...) including coordinated questions, combined indicative andinterrogative sentences, questions with quantifiers, and theimpossibility of negating questions. (shrink)

The paper presents a generalization of pregroup, by which a freely-generated pregroup is augmented with a finite set of commuting inequations, allowing limited commutativity and cancelability. It is shown that grammars based on the commutation-augmented pregroups generate mildly context-sensitive languages. A version of Lambek’s switching lemma is established for these pregroups. Polynomial parsability and semilinearity are shown for languages generated by these grammars.

The paper presents a plan for negation, proposing a paradigm shift from the Australian plan for negation, leading to a family of contra-classical logics. The two main ideas are the following: Instead of shifting points of evaluation (in a frame), shift the evaluated formula. Introduce an incompatibility set for every atomic formula, extended to any compound formula, and impose the condition on valuations that a formula evaluates to true iff all the formulas in its incompatibility set evaluate to false. Thus, (...) atomic sentences are not independent in their truth-values. The resulting negation, in addition to excluding the negated formula, provides a positive alternative to the negated formula. I also present a sound and complete natural deduction proof systems for those logics. In addition, the kind of negation considered in this paper is shown to provide an innovative notion of grounding negation. (shrink)

We present sound and complete semantics and a sequent calculus for the Lambek calculus extended with intuitionistic propositional logic.

In this paper, we propose a game semantics for the (associative) Lambek calculus . Compared to the implicational fragment of intuitionistic propositional calculus, the semantics deals with two features of the logic: absence of structural rules, as well as directionality of implication. We investigate the impact of these variations of the logic on its game semantics.

I presented a sub-classical relating logic based on a relating via an NL-inspired relating relation Rcss. The relation Rcss is motivated by the NL-phenomenon of phrasal (subsentential) coordination, exhibiting an important aspect of contents relating among the arguments of binary connectives. The resulting logic Lcss can be viewed as a relevance logic exhibiting a contents related relevance, stronger than the variable-sharing property of other relevance logics like R. Note that relating here is not “tailored” to justify some predetermined logic; rather, (...) the relating relation is independently justified, and induces a logic not previously investigated. (shrink)

Unification grammars are known to be Turing-equivalent; given a grammar G and a word w, it is undecidable whether w L(G). In order to ensure decidability, several constraints on grammars, commonly known as off-line parsability (OLP), were suggested, such that the recognition problem is decidable for grammars which satisfy OLP. An open question is whether it is decidable if a given grammar satisfies OLP. In this paper we investigate various definitions of OLP and discuss their interrelations, proving that some of (...) the OLP variants are indeed undecidable. We then present a novel, decidable OLP constraint which is more liberal than the existing decidable ones. (shrink)

In this paper, we propose an extension of free pregroups with lower bounds on sets of pregroup elements. Pregroup grammars based on such pregroups provide a kind of an algebraic counterpart to universal quantification over type-variables. In particular, we show how our pregroup extensions can be used for pregroup grammars expressing natural-language coordination and extraction.

A semantics with plural entitles and plural times accounts for cumulative relations between plural arguments and temporal expressions. The semantics equips nominal, verbal and sentential meanings with temporal context variables and treats temporal modifiers as temporal generalized quantifiers; cumulative conjunction, however, takes place at types lower than generalized quantifiers. The mediation of temporal context variables allows cumulative relations to percolate between an argument in a main clause and one in a temporal clause, in apparent violation of locality restrictions. Plural times (...) form a semilattice structure imposed on the set of intervals; no interaction is observed between this and the internal temporal structure of intervals. (shrink)

The paper provides a proof-theory for a negative presentation of classical logic based on a single primitive of exclusion, generalizing the known presentation via the binary ‘nand. The completeness is established via deductive equivalence to Gentzens NK/LK systems.

In this paper I introduce the notion of bilogics, namely logics interpreted over a pair of structures, in contrast to classical logic and many of its variations, the formulae of which are interpreted over one structure. In particular, I introduce and study Contrastive Logic, suitable for expressing contrast and conformity between the two structures involved.A major reason for this study is striving towards an extension of truth-conditional semantics to cover several natural-language particles, which have been hitherto considered not to be (...) amenable to such an extensional treatment, and were delegated to the level of non-extensional pragmatics. Examples of such particles are but and already. (shrink)

This paper investigates the meaning of restricted quantification when the embedded conditional is taken as the conditional of some first-order connexive logics. The study is carried out by checking the suitability of RQ for defining a connexive class theory, in analogy to the definition of Boolean class theory by using RQ in classical logic. Negative results are obtained for Wansing’s first-order connexive logic QC and one variant of Priest’s first-order connexive logic QP. A positive result is obtained for another variant (...) of QP. (shrink)

The paper proposes grounding the ternary connective “if … then … else” (classically interpreted), thus far not considered in the logical grounding literature. In doing so, a new kind of plural grounding, called collective immediate grounding, is proposed as more adequate than the traditional complete immediate grounding in avoiding redundancy. The approach is proof‐theoretic.

The paper proposes grounding the ternary connective “if … then … else” (classically interpreted), thus far not considered in the logical grounding literature. In doing so, a new kind of plural grounding, called collective immediate grounding, is proposed as more adequate than the traditional complete immediate grounding in avoiding redundancy. The approach is proof‐theoretic.

Theoria, Volume 87, Issue 5, Page 1175-1192, October 2021.

I show that in the context of proof-theoretic semantics, Dummett’s distinction between the assertoric meaning of a sentence and its ingredient sense can be seen as a distinction between two proof-theoretic meanings of a sentence: 1.Meaning as a conclusion of an introduction rule in a meaning-conferring natural-deduction proof system. 2.Meaning as a premise of an introduction rule in a meaning-conferring natural-deduction proof system. The effect of this distinction on compositionality of proof-theoretic meaning is discussed.

The paper has two parts: 1. A brief exposition of proof-theoretic semantics, not necessarily in connection to natural language. 2. A review, with a contrastive flavour, of some of the applications of PTS to NL with an indication of advantages of PTS as a theory of meaning for NL.

We study structural rules in the context of multi-valued logics with finitely-many truth-values. We first extend Gentzen’s traditional structural rules to a multi-valued logic context; in addition, we propos some novel structural rules, fitting only multi-valued logics. Then, we propose a novel definition, namely, structural rules completeness of a collection of structural rules, requiring derivability of the restriction of consequence to atomic formulas by structural rules only. The restriction to atomic formulas relieves the need to concern logical rules in the (...) derivation. (shrink)

We present an embedding of the Lambek–Grishin calculus into an extension of the nonassociative Lambek calculus with negation. The embedding is based on the De Morgan interpretation of the dual Grishin connectives.