On Gentzen Relations Associated with Finite-valued Logics Preserving Degrees of Truth

When considering m-sequents, it is always possible to obtain an m-sequent calculus VL for every m-valued logic (defined from an arbitrary finite algebra L of cardinality m) following for instance the works of the Vienna Group for Multiple-valued Logics. The Gentzen relations associated with the calculi VL are always finitely equivalential but might not be algebraizable. In this paper we associate an algebraizable 2-Gentzen relation with every sequent calculus VL in a uniform way, provided the original algebra L has a reduct that is a distributive lattice or a pseudocomplemented distributive lattice. We also show that the sentential logic naturally associated with the provable sequents of this algebraizable Gentzen relation is the logic that preserves degrees of truth with respect to the original algebra (in contrast with the more common logic that merely preserves truth). Finally, for some particular logics we obtain 2-sequent calculi that axiomatize the algebraizable Gentzen relations obtained so far.     

Proving theorems of the second order Lambek calculus in polynomial time

In the Lambek calculus of order 2 we allow only sequents in which the depth of nesting of implications is limited to 2. We prove that the decision problem of provability in the calculus can be solved in time polynomial in the length of the sequent. A normal form for proofs of second order sequents is defined. It is shown that for every proof there is a normal form proof with the same axioms. With this normal form we can give an algorithm that decides provability of sequents in polynomial time.The author was sponsored by project NF 102/62–356 (Structural and Semantic Parallels in Natural Languages and Programming Languages), funded by the Netherlands Organization for the Advancement of Research (NWO).Presented byCecylia Rauszer     

Protoalgebraic Gentzen Systems and the Cut Rule

In this paper we show that, in Gentzen systems, there is a close relation between two of the main characters in algebraic logic and proof theory respectively: protoalgebraicity and the cut rule. We give certain conditions under which a Gentzen system is protoalgebraic if and only if it possesses the cut rule. To obtain this equivalence, we limit our discussion to what we call regular sequent calculi, which are those comprising some of the structural rules and some logical rules, in a sense we make precise. We note that this restricted set of rules includes all the usual rules in the literature. We also stress the difference between the case of two-sided sequents and the case of many-sided sequents, in which more conditions are needed.     

Aspects of analytic deduction

Let ? be the ordinary deduction relation of classical first-order logic. We provide an “analytic” subrelation ?³ of ? which for propositional logic is defined by the usual “containment” criterion $$\Gamma \vdash ^a \varphi iff \Gamma \vdash \varphi and Atom(\varphi ) \subseteq Atom(\Gamma ),$$ whereas for predicate logic, ?^a is defined by the extended criterion $$\Gamma \vdash ^a \varphi iff \Gamma \vdash \varphi and Atom(\varphi ) \subseteq ' Atom(\Gamma ),$$ where Atom(?) $ \subseteq '$ Atom(Γ) means that every atomic formula occurring in ? “essentially occurs” also in Γ. If Γ, ? are quantifier-free, then the notions “occurs” and “essentially occurs” for atoms between Γ and ? coincide. If ? is formalized by Gentzen's calculus of sequents, then we show that ?^a is axiomatizable by a proper fragment of analytic inference rules. This is mainly due to cut elimination. By “analytic inference rule” we understand here a rule r such that, if the sequent over the line is analytic, then so is the sequent under the line. We also discuss the notion of semantic relevance as contrasted to the previous syntactic one. We show that when introducing semantic sequents as axioms, i.e. when extending the pure logical axioms and rules by mathematical ones, the property of syntactic relevance is lost, since cut elimination no longer holds. We conclude that no purely syntactic notion of analytic deduction can ever replace successfully the complex semantico-syntactic deduction we already possess.     

A Cut-Free Sequent Calculus for Defeasible Erotetic Inferences

In recent years, the effort to formalize erotetic inferences—i.e., inferences to and from questions—has become a central concern for those working in erotetic logic. However, few have sought to formulate a proof theory for these inferences. To fill this lacuna, we construct a calculus for (classes of) sequents that are sound and complete for two species of erotetic inferences studied by Inferential Erotetic Logic (IEL): erotetic evocation and erotetic implication. While an effort has been made to axiomatize the former in a sequent system, there is currently no proof theory for the latter. Moreover, the extant axiomatization of erotetic evocation fails to capture its defeasible character and provides no rules for introducing or eliminating question-forming operators. In contrast, our calculus encodes defeasibility conditions on sequents and provides rules governing the introduction and elimination of erotetic formulas. We demonstrate that an elimination theorem holds for a version of the cut rule that applies to both declarative and erotetic formulas and that the rules for the axiomatic account of question evocation in IEL are admissible in our system.

     

Effective Cut-elimination for a Fragment of Modal mu-calculus

A non-effective cut-elimination proof for modal mu-calculus has been given by G. J?ger, M. Kretz and T. Studer. Later an effective proof has been given for a subsystem M ₁ with non-iterated fixpoints and positive endsequents. Using a new device we give an effective cut-elimination proof for M ₁ without restriction to positive sequents.     

A Rule-Extension of the Non-Associative Lambek Calculus

An extension L ⁺ of the non-associative Lambek calculus Lis defined. In L ⁺ the restriction to formula-conclusion sequents is given up, and additional left introduction rules for the directional implications are introduced. The system L ⁺ is sound and complete with respect to a modification of the ternary frame semantics for L.     

Display calculi and other modal calculi: a comparison

In this paper we introduce and compare four different syntactic methods for generating sequent calculi for the main systems of modal logic: the multiple sequents method, the higher-arity sequents method, the tree-hypersequents method and the display method. More precisely we show how the first three methods can all be translated in the fourth one. This result sheds new light on these generalisations of the sequent calculus and raises issues that will be examined in the last section.     

The Pentus Theorem for Lambek Calculus with Simple Nonlogical Axioms

The Lambek calculus introduced in Lambek [6] is a strengthening of the type reduction calculus of Ajdukiewicz [1]. We study Associative Lambek Calculus L in Gentzen style axiomatization enriched with a finite set Γ of nonlogical axioms, denoted by L(Γ).It is known that finite axiomatic extensions of Associative Lambek Calculus generate all recursively enumerable languages (see Buszkowski [2]). Then we confine nonlogical axioms to sequents of the form p → q, where p and q are atomic types. For calculus L(Γ) we prove interpolation lemma (modifying the Roorda proof for L [10]) and the binary reduction lemma (using the Pentus method [9] with modification from [3]). In consequence we obtain the weak equivalence of the Context-Free Grammars and grammars based on L(Γ).     

Acceptance, inference, and the multiple-conclusion sequent

This paper offers an interpretation of multiple-conclusion sequents as a kind of meta-inference rule: just as single-conclusion sequents represent inferences from sentences to sentences, so multiple-conclusion sequents represent a certain kind of inference from single-conclusion sequents to single-conclusion sequents. The semantics renders sound and complete the standard structural rules of reflexivity, monotonicity (or thinning), and transitivity (or cut). The paper is not the first one to attempt to account for multiple-conclusion sequents without invoking notions of truth or falsity??but unlike earlier such efforts, which have typically helped themselves to primitive notions of both acceptance and rejection, the present one makes do with the former alone. For technical reasons, the treatment is limited to sequents with non-empty succedents.     

Proof Systems for Reasoning about Computation Errors

In the paper we examine the use of non-classical truth values for dealing with computation errors in program specification and validation. In that context, 3-valued McCarthy logic is suitable for handling lazy sequential computation, while 3-valued Kleene logic can be used for reasoning about parallel computation. If we want to be able to deal with both strategies without distinguishing between them, we combine Kleene and McCarthy logics into a logic based on a non-deterministic, 3-valued matrix, incorporating both options as a non-deterministic choice. If the two strategies are to be distinguished, Kleene and McCarthy logics are combined into a logic based on a 4-valued deterministic matrix featuring two kinds of computation errors which correspond to the two computation strategies described above. For the resulting logics, we provide sound and complete calculi of ordinary, two-valued sequents. Presented by Yaroslav Shramko and Heinrich Wansing     

A General Framework for $$ {FDE}$$ FDE -Based Modal Logics

We develop a general theory of FDE-based modal logics. Our framework takes into account the four-valued nature of FDE by considering four partially defined modal operators corresponding to conditions for verifying and falsifying modal necessity and possibility operators. The theory comes with a uniform characterization for all obtained systems in terms of FDE-style formula-formula sequents. We also develop some correspondence theory and show how Hilbert-style axiom systems can be obtained in appropriate cases. Finally, we outline how different systems from the literature can be expressed in our framework.

     

Quine and Slater on Paraconsistency and Deviance

In a famous and controversial paper, B. H. Slater has argued against the possibility of paraconsistent logics. Our reply is centred on the distinction between two aspects of the meaning of a logical constant ^*c^* in a given logic: its operational meaning, given by the operational rules for ^*c^* in a cut-free sequent calculus for the logic at issue, and its global meaning, specified by the sequents containing ^*c^* which can be proved in the same calculus. Subsequently, we use the same strategy to counter Quine's meaning variance argument against deviant logics. In a nutshell, we claim that genuine rivalry between (similar) logics ^*L^* and ^*L^* is possible whenever each constant in ^*L^* has the same operational meaning as its counterpart in ^*L^* although differences in global meaning arise in at least one case.     

Quantum logical calculi and lattice structures

In a preceding paper [1] it was shown that quantum logic, given by the tableaux-calculus T _eff, is complete and consistent with respect to the dialogic foundation of logics. Since in formal dialogs the special property of the value-definiteness of propositions is not postulated, the calculus T _eff represents a calculus of effective (intuitionistic) quantum logic.Beginning with the tableaux-calculus the equivalence of T _eff to calculi which use more familiar figures such as sequents and implications can be investigated. In this paper we present a sequents-calculus of Gentzen-type and a propositional calculus of Brouwer-type which are shown to be equivalent to T _eff. The effective propositional calculus provides an interpretation for a lattice structure, called quasi-implicative lattice. If, in addition, the value-definiteness of quantum mechanical propositions is postulated, a propositional calculus is obtained which provides an interpretation for a quasi-modular orthocomplemented lattice which, as is well-known, has as a model the lattice of subspaces of a Hilbert space.     

A family of Gödel hybrid logics

In this paper, we define a family of fuzzy hybrid logics that are based on Gödel logic. It is composed of two infinite-valued versions called ${\mathsf{GH}}_{\infty }$ and ${\mathsf{WGH}}_{\infty }$, and a sequence of finitary valued versions ${({\mathsf{GH}}_n)}_{0<n<\infty }$. We define decision procedures for both ${\mathsf{WGH}}_{\infty }$ and ${({\mathsf{GH}}_n)}_{0<n<\infty }$ that are based on particular sequents and on a set of proof rules dealing with such sequents. As these rules are strongly invertible the procedures naturally allow one to generate countermodels. Therefore we prove the decidability and the finite model property for these logics. Finally, from the decision procedure of ${\mathsf{WGH}}_{\infty }$, we design a sound and complete sequent calculus for this logic.     

Symmetry, Compact Closure and Dagger Compactness for Categories of Convex Operational Models

In the categorical approach to the foundations of quantum theory, one begins with a symmetric monoidal category, the objects of which represent physical systems, and the morphisms of which represent physical processes. Usually, this category is taken to be at least compact closed, and more often, dagger compact, enforcing a certain self-duality, whereby preparation processes (roughly, states) are interconvertible with processes of registration (roughly, measurement outcomes). This is in contrast to the more concrete “operational” approach, in which the states and measurement outcomes associated with a physical system are represented in terms of what we here call a convex operational model: a certain dual pair of ordered linear spaces–generally, not isomorphic to one another. On the other hand, state spaces for which there is such an isomorphism, which we term weakly self-dual, play an important role in reconstructions of various quantum-information theoretic protocols, including teleportation and ensemble steering. In this paper, we characterize compact closure of symmetric monoidal categories of convex operational models in two ways: as a statement about the existence of teleportation protocols, and as the principle that every process allowed by that theory can be realized as an instance of a remote evaluation protocol—hence, as a form of classical probabilistic conditioning. In a large class of cases, which includes both the classical and quantum cases, the relevant compact closed categories are degenerate, in the weak sense that every object is its own dual. We characterize the dagger-compactness of such a category (with respect to the natural adjoint) in terms of the existence, for each system, of a symmetric bipartite state, the associated conditioning map of which is an isomorphism.     

Cognitive load eliminates the global perceptual bias for unlimited exposure durations

In the present study, we used Navon-type Cognitive Psychology 9: 353–383 (1977) hierarchical patterns to demonstrate that cognitive load eliminates a global perceptual bias and enhances the representation of local elements at unlimited exposure durations. We added a cognitive-load manipulation to Kimchi and Palmer’s Journal of Experimental Psychology: Human Perception and Performance 8:521–535 (1982) similarity-matching experiment with hierarchical patterns, and presented the stimuli for either unlimited or limited exposure durations. When exposures were unlimited, we demonstrated that observers exhibited a global bias under low, but not under high, cognitive load (Exp. 2). When exposures were limited, however, cognitive load exerted no effect, and the global bias remained (Exp. 1). We suggest that (1) these findings are best reconciled by proposing two stages in the representation of global structure, namely construction and maintenance; (2) the construction and maintenance stages are isolated, respectively, by limited-duration and unlimited-duration paradigms; and (3) cognitive processes play an integral role only in the maintenance stage. Given that real-world vision is not driven by a series of brief stimulus exposures, and is therefore likely to reflect maintenance processes, we argue that unlimited-exposure paradigms are more suitable for addressing real-world perceptual biases. When unlimited-exposure paradigms are used, cognitive load eliminates the commonly reported global bias.     

Demands of Justice, Feasible Alternatives, and the Need for Causal Analysis

Many political philosophers hold the Feasible Alternatives Principle (FAP): justice demands that we implement some reform of international institutions P only if P is feasible and P improves upon the status quo from the standpoint of justice. The FAP implies that any argument for a moral requirement to implement P must incorporate claims whose content pertains to the causal processes that explain the current state of affairs. Yet, philosophers routinely neglect the need to attend to actual causal processes. This undermines their arguments concerning moral requirements to reform international institutions. The upshot is that philosophers’ arguments must engage in causal analysis to a greater extent than is typical.     

A distinction concerning vision-for-action and affordance perception

In this paper, I offer a discussion concerning the conceptual connection between the notion of vision-for-action and the one of affordance perception. I first analyze the notion of vision-for-action. I then analyze a notion usually coupled with it: the notion of affordance perception, the main insights behind which are guiding several current neuroscientific enterprises and the related philosophical speculations. Then, I argue that we should not couple these two notions with a light heart: though these two processes can be, from a theoretical point of view, related, we should be careful in inferring the actual and effective occurrence of the latter in the presence of the former. This will be done by carrying out a conceptual analysis of the experimental evidence coming from the ‘Two Visual Systems Model’, which is the main reference in the literature on affordance perception and vision-for-action. My point has strong philosophical implications for our view concerning the best interpretation of how vision-for-action really works, and the specific relation it actually entertains with affordance perception.     

The Influence of the BDNF Val66Met Polymorphism on Mechanisms of Semantic Priming: Analyses with Drift-Diffusion Models of Masked and Unmasked Priming

Automatic and strategic processes in semantic priming can be investigated with masked and unmasked priming tasks. Unmasked priming is thought to enable strategic processes due to the conscious processing of primes, while masked priming exclusively depends on automatic processes due to the invisibility of the prime. Besides task properties, interindividual differences may alter priming effects. In a recent study, masked and unmasked priming based on mean response time (RT) and error rate (ER) differed as a function of the BDNF Val66Met polymorphism (Sanwald et al., 2020). The BDNF Val66Met polymorphism is related to the integrity of several cognitive executive functions and might thus influence the magnitude of priming. In the present study, we reanalyzed this data with drift-diffusion models. Drift-diffusion models conjointly analyze single trial RT and ER data and serve as a framework to elucidate cognitive processes underlying priming. Masked and unmasked priming effects were observed for the drift rates ν, presumably reflecting semantic preactivation. Priming effects on nondecision time t0 were especially pronounced in unmasked priming, suggesting additional conscious processes to be involved in the t0 modulation. Priming effects on the decision thresholds a may reflect a speed-accuracy tradeoff. Considering the BDNF Val66Met polymorphism, we found lowered drift rates and decision thresholds for Met allele carriers, possibly reflecting a superficial processing style in Met allele carriers. The present study shows that differences in cognitive tasks between genetic groups can be elucidated using drift-diffusion modeling.