Search

We define an extension of predicate logic, called Binding Logic, where variables can be bound in terms and in propositions. We introduce a notion of model for this logic and prove a soundness and completeness theorem for it. This theorem is obtained by encoding this logic back into predicate logic and using the classical soundness and completeness theorem there., Comment: Colloque avec actes et comit{\'e} de lecture. internationale

We provide a semi-grammatical description of the set of normal proofs of positive formulae in minimal predicate logic, i.e. a grammar that generates a set of schemes, from each of which we can produce a finite number of normal proofs. This method is complete in the sense that each normal proof-term of the formula is produced by some scheme generated by the grammar. As a corollary, we get a similar description of the set of normal proofs of positive formulae for a large class of theories including simple type theory and System F.

The Satisfiability Modulo Theories (SMT) issue concerns the satisfiability of formulae from multiple background theories, usually expressed in the language of first-order predicate logic with equality. SMT solvers are often based on variants of the Nelson-Oppen combination method, a solver for the quantifier-free fragment of the combination of theories with disjoint signatures, via cooperation among their decision procedures. When each of the theories to be combined by the Nelson-Oppen method is convex (that is, any conjunction of its literals can imply a disjunction of equalities only when it implies at least one of the equalities) and decidable in polynomial time, the running time of the combination procedure is guaranteed to be polynomial in the size of the input formula. In this paper, we prove the convexity of a fragment of Zermelo-Fraenkel set theory, called Multi-Level Syllogistic, most of whose polynomially decidable fragments we have recently characterized., In Proceedings GandALF 2021, arXiv:2109.07798

A notion of strictly primitive recursive realizability is introduced by Damnjanovic in 1994. It is a kind of constructive semantics of the arithmetical sentences using primitive recursive functions. It is of interest to study the corresponding predicate logic. It was argued by Park in 2003 that the predicate logic of strictly primitive recursive realizability is not arithmetical. Park’s argument is essentially based on a claim of Damnjanovic that intuitionistic logic is sound with respect to strictly primitive recursive realizability, but that claim was disproved by the author of this article in 2006. The aim of this paper is to present a correct proof of the result of Park.

Contrary to received opinion, the Aristotelian Square of Opposition (square) is logically sound, differing from standard modern predicate logic (SMPL) only in that it restricts the universe U of cognitively constructible situations by banning null predicates, making it less unnatural than SMPL. U-restriction strengthens the logic without making it unsound. It also invites a cognitive approach to logic. Humans are endowed with a cognitive predicate logic (CPL), which checks the process of cognitive modelling (world construal) for consistency. The square is considered a first approximation to CPL, with a cognitive set-theoretic semantics. Not being cognitively real, the null set Ø is eliminated from the semantics of CPL. Still rudimentary in Aristotle’s On Interpretation (Int), the square was implicitly completed in his Prior Analytics (PrAn), thereby introducing U-restriction. Abelard’s reconstruction of the logic of Int is logically and historically correct; the loca (Leaking O-Corner Analysis) interpretation of the square, defended by some modern logicians, is logically faulty and historically untenable. Generally, U-restriction, not redefining the universal quantifier, as in Abelard and loca, is the correct path to a reconstruction of CPL. Valuation Space modelling is used to compute the effects of U-restriction.

We investigate the role of coalgebraic predicate logic, a logic for neighborhood frames first proposed by Chang, in the study of monotonic modal logics. We prove analogues of the Goldblatt-Thomason Theorem and Fine's Canonicity Theorem for classes of monotonic neighborhood frames closed under elementary equivalence in coalgebraic predicate logic. The elementary equivalence here can be relativized to the classes of monotonic, quasi-filter, augmented quasi-filter, filter, or augmented filter neighborhood frames, respectively. The original, Kripke-semantic versions of the theorems follow as a special case concerning the classes of augmented filter neighborhood frames., Comment: 25 pages; to be published in Studia Logica

In this paper, we deal with a relationship among the law of excluded middle, the double negation elimination and the independence of premiss rule ( $$\mathrm {IPR}$$ ) for (many-sorted) intuitionistic predicate logic. After giving a general machinery, we give, as corollaries, several examples of extensions of $$\mathbf {HA}$$ and $$\mathbf {HA}^\omega $$ which are closed under $$\mathrm {IPR}$$ but do not derive the independence of premiss axiom.

Satisfiability or Sat $$^{1}$$ is the metatheoretic statement Every formally intuitionistically consistent set of first-order sentences has a model. The models in question are the Tarskian relational structures familiar from standard first-order model theory (Chang and Keisler in Model theory, 3rd edn, Dover Publications Inc., Mineola, 2012), but here treated within intuitionistic metamathematics. We prove that both IZF, intuitionistic Zermelo–Fraenkel set theory, and HAS, second-order Heyting arithmetic, prove Sat $$^{1}$$ to be false outright. Following the lead of Carter (Notre Dame J Form Log 49(1):75–95, 2008), we then generalize this result to some provably intermediate first-order logics, including the Rose logic (Trans Am Math Soc 61:1–19, 1953). These metatheorems distinguish the intuitionistic foundational significance of Sat $$^{1}$$ sharply from that of Sat $$^{0}$$ , the satisfiability claim for intuitionistic propositional logic. At the same time, they establish intuitionistic connections with and between Test, COMP $$^{0}$$ , and $$\mathbf{COMP }^{1}$$ . Here, Test is the scheme of Testability, and COMP $$^{0}$$ and $$\mathbf{COMP }^{1}$$ are completeness for intuitionistic propositional logic and predicate logic, respectively.

Classically, any structure for a signature ${\rm{\Sigma }}$ may be completed to a model of a desired regular theory ${T}}$ by means of the chase construction or small object argument. Moreover, this exhibits ${\rm{Mod}}\left(T)$ as weakly reflective in ${\rm{Str}}\left( {\rm{\Sigma }} \right)$.We investigate this in the constructive setting. The basic construction is unproblematic; however, it is no longer a weak reflection. Indeed, we show that various reflectivity principles for models of regular theories are equivalent to choice principles in the ambient set theory. However, the embedding of a structure into its chase-completion still satisfies a conservativity property, which suffices for applications such as the completeness of regular logic with respect to Tarski (i.e., set) models.Unlike most constructive developments of predicate logic, we do not assume that equality between symbols in the signature is decidable. While in this setting, we also give a version of one classical lemma which is trivial over discrete signatures but more interesting here: the abstraction of constants in a proof to variables.

This chapter introduces a predicate language called Lq. The alphabet of Lq is constituted by the following symbols: a, b, c… P, Q, R… ∼, ⊃, ∀ x, y, z… (, )

In standard epistemic logic, the names and the existence of agents are usually assumed to be common knowledge implicitly. This is unreasonable for various applications in computer science and philosophy. Inspired by term-modal logic and assignment operators in dynamic logic, we introduce a lightweight modal predicate logic where names can be non-rigid, and the existence of agents can be uncertain. The language can handle various de dicto/de re distinctions in a natural way. We characterize the expressive power of our language, obtain complete axiomatisations of the logics over several classes of varying-domain/constant-domain epistemic models, and show their (un)decidability.

We show that the logic of partial quasiary predicates is undecidable over arbitrary structures and not recursively enumerable over finite structures. The results are obtained by reduction from the classical predicate logic.

It is known that some fuzzy predicate logics, such as Łukasiewicz predicate logic, are not complete with respect to the standard real-valued semantics. In the present paper we focus upon a typed version of first-order MTL (Monoidal T-norm Logic), which gives a unified framework for different fuzzy logics including, inter alia, Hajek’s basic logic, Łukasiewicz logic, and Godel logic. And we show that any extension of first-order typed MTL, including Łukasiewicz predicate logic, is sound and complete with respect to the corresponding categorical semantics in the style of Lawvere’s hyperdoctrine, and that the so-called Baaz delta translation can be given in the first-order setting in terms of Lawvere’s hyperdoctrine. A hyperdoctrine may be seen as a fibred algebra, and the first-order completeness, then, is a fibred extension of the algebraic completeness of propositional logic. While the standard real-valued semantics for Łukasiewicz predicate logic is not complete, the hyperdoctrine, or fibred algebraic, semantics is complete because it encompasses a broader class of models that is sufficient to prove completeness; in this context, incompleteness may be understood as telling that completeness does not hold when the class of models is restricted to the standard class of real-valued hyperdoctrine models. We expect that this finally leads to a unified categorical understanding of Takeuti-Titani’s fuzzy models of set theory.

We develop algebraic models of simple type theories, laying out a framework that extends universal algebra to incorporate both algebraic sorting and variable binding. Examples of simple type theories include the unityped and simply-typed $\lambda$-calculi, the computational $\lambda$-calculus, and predicate logic. Simple type theories are given models in presheaf categories, with structure specified by algebras of polynomial endofunctors that correspond to natural deduction rules. Initial models, which we construct, abstractly describe the syntax of simple type theories. Taking substitution structure into consideration, we further provide sound and complete semantics in structured cartesian multicategories. This development generalises Lambek's correspondence between the simply-typed $\lambda$-calculus and cartesian-closed categories, to arbitrary simple type theories., Comment: 14 pages

We study a modal extension of the Continuous First-Order Logic of Ben Yaacov and Pedersen (J Symb Logic 75(1):168–190, 2010). We provide a set of axioms for such an extension. Deduction rules are just Modus Ponens and Necessitation. We prove that our system is sound with respect to a Kripke semantics and, building on Ben Yaacov and Pedersen (2010), that it satisfies a number of properties similar to those of first-order predicate logic. Then, by means of a canonical model construction, we get that every consistent set of formulas is satisfiable. From the latter result we derive an Approximated Strong Completeness Theorem, in the vein of Continuous Logic, and a Compactness Theorem.

We consider the minimal number of productions needed for a grammar to cover a finite language L as the grammatical complexity of L. We study this measure for several types of word and tree grammars and show that it is closely connected to well-known measures for the complexity of formal proofs in first-order predicate logic. We construct an incompressible sequence of finite word languages and transfer this and several other results about the complexity of word and tree languages to formal proofs.

In this paper we present an algorithmic method of lemma introduction. Given a proof in predicate logic with equality the algorithm is capable of introducing several universal lemmas. The method is based on an inversion of Gentzen’s cut-elimination method for sequent calculus. The first step consists of the computation of a compact representation (a so-called decomposition) of Herbrand instances in a cut-free proof. Given a decomposition the problem of computing the corresponding lemmas is reduced to the solution of a second-order unification problem (the solution conditions). It is shown that that there is always a solution of the solution conditions, the canonical solution. This solution yields a sequence of lemmas and, finally, a proof based on these lemmas. Various techniques are developed to simplify the canonical solution resulting in a reduction of proof complexity. Moreover, the paper contains a comprehensive empirical evaluation of the implemented method and gives an application to a mathematical proof.

Purpose Three problematic issues followed by paradigm changes over the recent history of human intellectual endeavour are identified as 1. mysticism/superstition to – conventional science (of physics), 2. predominant use of qualitative/quantitative properties for analysis and design to – structural or systemic properties, and 3. current speculative/fragmented, multiple approaches to the “systemic view” to – a firmer knowledge-based approach reflecting the empirical and universal nature of this view. This paper aims to consider the problematic issues, to conclude that conventional science is inadequate to cope with the 2nd paradigm change and to introduce a “new science of systems” which can integrate conventional science and alleviate the 3rd problematic issue by suggesting three principles implemented by linguistic modelling as operational model. Design/methodology/approach The highly successful methodology of conventional science is followed with systemic content by suggesting three general principles of systems, namely, principle of existence (pervasiveness of structural description), principle of complexity (aggregates for emergence of outcomes) and principle of change (change by purpose or chance), and linguistic modelling of static and dynamic scenarios based on natural language as operational model. This language is processed to “elementary constituents”, of which complex structures can be constructed. These constituents are converted into reasoning schemes consisting of “ordered pairs” and “predicate logic statements” in static and dynamic states. Findings Stories of problematic scenarios are converted into the universal scheme of “management/producers” – “products” – “users/consumers” by constructing linguistic networks of products and semantic diagrams of organizations/user/consumers for investigating the emergence of outcomes in analysis and for designing prototypes. Problematic issues of individual objects in a scenario are resolved by methods of conventional science, which is thus integrated with systems science to form the “scientific enterprise”. Research limitations/implications Once the new approach is debated, further developments in the mathematics of ordered pairs, predicate logic and uncertainties are needed. The linguistic basis is to be further investigated. Connection with AI and “logical atomism of Bertrand Russell” is to be explored. Practical implications Further applications to large-scale scenarios by practitioners using the “universal scheme” and development of software are needed. Social implications The approach is rooted in accepted branches of knowledge, is highly teachable and should lead to be used by professionals and others once debated and accepted.

The main aim of this article is to extend our representation results on tense MV-algebras into a partial mapping setting. Tense MV-algebras are just MV-algebras with new unary operations G and H which express a universal time quantifiers and they were introduced by D. Diaconescu and G. Georgescu. (C) 2017 Elsevier B.V. All rights reserved.

In this paper the logic of broad necessity is explored. Definitions of what it means for one modality to be broader than another are formulated, and it is proven, in the context of higher-order logic, that there is a broadest necessity, settling one of the central questions of this investigation. It is shown, moreover, that it is possible to give a reductive analysis of this necessity in extensional language (using truth functional connectives and quantifiers). This relates more generally to a conjecture that it is not possible to define intensional connectives from extensional notions. This conjecture is formulated precisely in higher-order logic, and concrete cases in which it fails are examined. The paper ends with a discussion of the logic of broad necessity. It is shown that the logic of broad necessity is a normal modal logic between S4 and Triv, and that it is consistent with a natural axiomatic system of higher-order logic that it is exactly S4. Some philosophical reasons to think that the logic of broad necessity does not include the S5 principle are given.

In this paper we apply proof theoretic methods used for classical systems in order to obtain upper bounds for systems in partial logic. We focus on a truth predicate interpreted in a Kripke style way via strong Kleene; whereas the aim is to connect harmoniously the partial version of Kripke–Feferman with its intended semantics. The method we apply is based on infinitary proof systems containing an $$\omega $$ -rule.

We prove two completeness results, one for the extension of dependence logic by a monotone generalized quantifier Q with weak interpretation, weak in the meaning that the interpretation of Q varies with the structures. The second result considers the extension of dependence logic where Q is interpreted as "there exists uncountable many." Both of the axiomatizations are shown to be sound and complete for FO(Q) consequences., 17 pages

We introduce a new typed combinatory calculus with a type constructor that, to each type $$\sigma $$ , associates the star type $$\sigma ^*$$ of the nonempty finite subsets of elements of type $$\sigma $$ . We prove that this calculus enjoys the properties of strong normalization and confluence. With the aid of this star combinatory calculus, we define a functional interpretation of first-order predicate logic and prove a corresponding soundness theorem. It is seen that each theorem of classical first-order logic is connected with certain formulas which are tautological in character. As a corollary, we reprove Herbrand’s theorem on the extraction of terms from classically provable existential statements.

Strong equivalence is an important concept in the theory of answer set programming. Informally speaking, two sets of rules are strongly equivalent if they have the same meaning in any context. Equilibrium logic was used to prove that sets of rules expressed as propositional formulas are strongly equivalent if and only if they are equivalent in the logic of here-and-there. We extend this line of work to formulas with infinitely long conjunctions and disjunctions, show that the infinitary logic of here-and-there characterizes strong equivalence of infinitary formulas, and give an axiomatization of that logic. This is useful because of the relationship between infinitary formulas and logic programs with local variables.

Stable model semantics had been recently generalized to non-Herbrand structures by several works, which provides a unified framework and solid logical foundations for answer set programming. This article focuses on the expressiveness of normal and disjunctive logic programs under general stable model semantics. A translation from disjunctive logic programs to normal logic programs is proposed for infinite structures. Over finite structures, some disjunctive logic programs are proved to be intranslatable to normal logic programs if the arities of auxiliary predicates and functions are bounded in a certain way. The equivalence of the expressiveness of normal logic programs and disjunctive logic programs over arbitrary structures is also shown to coincide with that over finite structures and coincide with whether the complexity class NP is closed under complement. Moreover, to obtain a more explicit picture of the expressiveness, some intertranslatability results between logic program classes, and fragments of second-order logic are established.

The paper suggests a modal predicate logic that deals with classical quantification and modalities as well as intermediate operators, like “most” and “mostly”. Following up the theory of generalized quantifiers, we will understand them as two-placed operators and call them determiners. Quantifiers as well as modal operators will be constructed from them. Besides the classical deduction, we discuss a weaker probabilistic inference “therefore, probably” defined by symmetrical probability measures in Carnap’s style. The given probabilistic inference relates intermediate quantification to singular statements: “Most S are P” does not logically entail that a particular individual S is also P, but it follows that this is probably the case, where the probability is not ascribed to the propositions but to the inference. We show how this system deals with single case expectations while predictions of statistical statements remain generally problematic.

Game logic is a dynamic modal logic which models strategic two person games; it contains propositional dynamic logic (PDL) as a fragment. We propose an interpretation of game logic based on stochastic effectivity functions. A definition of these functions is given, and some algebraic properties of effectivity functions such as congruences are investigated. The relationship with stochastic relations is characterized through a deduction system. Logical and behavioral equivalence of game models is investigated. Finally the completion of models receives some attention.

This paper presents an efficient approach to verifying higher-degree Galois-field (GF) arithmetic circuits. The proposed method describes GF arithmetic circuits using a mathematical graph-based representation and verifies them by a combination of algebraic transformations and a new verification method based on natural deduction for first-order predicate logic with equal sign. The natural deduction method can verify one type of higher-degree GF arithmetic circuit efficiently while the existing methods require an enormous amount of time, if they can verify them at all. In this paper, we first apply the proposed method to the design and verification of various Reed-Solomon (RS) code decoders. We confirm that the proposed method can verify RS decoders with higher-degree functions while the existing method needs a lot of time or fail. In particular, we show that the proposed method can be applied to practical decoders with 8-bit symbols, which are performed with up to 2,040-bit operands. We then demonstrate the design and verification of the Advanced Encryption Standard (AES) encryption and decryption processors. As a result, the proposed method successfully verifies the AES decryption datapath while an existing method fails.

I present a reconstruction of the logical system of the Tractatus, which differs from classical logic in two ways. It includes an account of Wittgenstein’s “form-series” device, which suffices to express some effectively generated countably infinite disjunctions. And its attendant notion of structure is relativized to the fixed underlying universe of what is named.There follow three results. First, the class of concepts definable in the system is closed under finitary induction. Second, if the universe of objects is countably infinite, then the property of being a tautology is $\Pi _1^1$-complete. But third, it is only granted the assumption of countability that the class of tautologies is ${\Sigma _1}$-definable in set theory.Wittgenstein famously urges that logical relationships must show themselves in the structure of signs. He also urges that the size of the universe cannot be prejudged. The results of this paper indicate that there is no single way in which logical relationships could be held to make themselves manifest in signs, which does not prejudge the number of objects.

In this paper we introduce arbitrary arrow update logic (AAUL). The logic AAUL takes arrow update logic, a dynamic epistemic logic where the accessibility relations of agents are updated rather than the set of possible worlds, and adds a quantifier over such arrow updates.We investigate the relative expressivity of AAUL compared to other logics, most notably arbitrary public announcement logic (APAL). Additionally, we show that the model checking problem for AAUL is PSPACE-complete. Finally, we introduce a proof system for AAUL, and prove it to be sound and complete. (C) 2016 Elsevier B.V. All rights reserved.

We present a simple proof of Thrakhtenbrot's theorem for the classical predicate logic in the language with only three individual variables. Both forms of Thrakhtenbrot's theorem are established: we prove that the classical predicate logic QCL over finite domains is not recursively enumerable in the language with only three individual variables and that the set of theorems of QCL over arbitrary domains and the set of non-theorems of QCL over finite domains, in the language with only three individual variables, form a recursively inseparable pair of recursively enumerable sets. The techniques used here can be generalised to obtain similar results for non-classical predicate logics with further restrictions on their vocabularies.

Empty categories are one of the fundamental parts of generativist’s view towards language. Empty operators, the so-called null elements, which are syntactically active in relative clauses and possibly move into [spec, CP], have reportedly been found in different languages. However, there is no solid evidence for the existence of empty operators in Persian relative clauses. Despite this, syntactic evidences such as theta theory, argument structure and subjacency condition provide satisfactory provable tests in favor of their role in Persian grammar. Namely, Persian relative clauses contain resumptive pronouns which may be covert. Their movement into [spec, CP] can precisely account for subjacency effect in relative clauses. Resumptive pronouns can occupy the subject as well as the object position. This articles attempts to introduce empty operators to Persian syntax, and shows that in such a way it is possible to account for the peculiar behavior of the Persian complementizer “ke” and its obligatory nature.

The functions of a protein can be inferred from the molecules that associate with it. A protein-molecules association can be identified from their co-occurrences in biomedical literature. Based on this, recent computational methods predict protein functions, especially with the exponential explosion of biomedical literatures post-genomic era. These methods extract information from the literatures that explicitly describe the functions of proteins. We observe that some molecule terms pertaining protein functions may co-occur implicitly with proteins in biomedical texts. Thus, these recent methods may miss vital information about protein functions that is implicitly mentioned in the literature. To overcome this, we propose an Information Extraction system called PLPF that adopts techniques for predicting the functions of proteins from their both explicit and implicit co-occurrences in biomedical texts with molecule terms pertaining protein functions. It uses a combination of explicit term extraction methods and logic-based implicit term extraction methods. Let $\boldsymbol{t}$ be a functional term that co-occurrence with an unannotated protein $\boldsymbol{p_{u}}$ . PLPF will assign pu the functional category $\boldsymbol{t}$ , if: (1) the co-occurrences of the pair $\boldsymbol{t}-\boldsymbol{p_{u}}$ are explicit and the pair is semantically related bases on the syntactic structures of sentences, or (2) the co-occurrences of the pair $\boldsymbol{t}-\boldsymbol{p_{u}}$ are implicit based on the inference rules of predicate logic. We evaluated PLPF by comparing it experimentally with four existing methods. Results showed marked improvement.

In this paper, we study finitely axiomatizable conservative extensions of a theoryUin the case whereUis recursively enumerable and not finitely axiomatizable. Stanisław Krajewski posed the question whether there are minimal conservative extensions of this sort. We answer this question negatively.Consider a finite expansion of the signature ofUthat contains at least one predicate symbol of arity ≥ 2. We show that, for any finite extensionαofUin the expanded language that is conservative overU, there is a conservative extensionβofUin the expanded language, such that$\alpha \vdash \beta$and$\beta \not \vdash \alpha$. The result is preserved when we consider eitherextensionsormodel-conservative extensionsofUinstead ofconservative extensions. Moreover, the result is preserved when we replace$\dashv$as ordering on the finitely axiomatized extensions in the expanded language by a relevant kind of interpretability, to witinterpretability that identically translates the symbols of the U-language.We show that the result fails when we consider an expansion with only unary predicate symbols for conservative extensions ofUordered by interpretability that preserves the symbols ofU.

On the standard view for something to exist is for one thing to exist: in slogan form, to be is to be countable (cf. van Inwagen 2009). E.J. Lowe (2009, 2003, 1998) argues something can exist without being countable as one, however. His primary example is homogenous “stuff,” i.e., qualitatively uniform and infinitely divisible matter. Lacking nonarbitrary boundaries and being everywhere the same, homogenous stuff lacks a principle of individuation that would yield countably distinct constituents. So, for Lowe, homogenous stuff is strongly uncountable. Olson (2011) rejects Lowe’s view and defends the orthodox connection between existence and number. He argues that if there is any stuff, there is a (determinate) number of portions of stuff. Sider (2011, 2001) also rejects a stuff ontology, claiming it is incompatible with his preferred view that the familiar quantifiers of predicate logic carve at nature’s joints. Against these arguments, I defend the uncountability of stuff and the possibility of existence without countability. If to be is to be countable, more is needed than the arguments that Olson and Sider provide.

We consider the two-variable logic with counting quantifiers (C 2 ) interpreted over finite structures that contain two forests of ranked trees. This logic is strictly more expressive than standard C 2 and it is no longer a fragment of first-order logic. In particular, it can express that a structure is a ranked tree, a cycle, or a connected graph of bounded degree. It is also strictly more expressive than first-order logic with two variables and two successor relations of two finite linear orders. We present a decision procedure for the satisfiability problem for this logic. The procedure runs in NE xp T ime , which is optimal since the satisfiability problem for plain C 2 is NE xp T ime -complete.

We show that the constructive predicate logic with positive (covariant) quantification is hard for doubly exponential universal time, that is, for the class co- 2-N exptime . Our approach is to represent proof-search as computation of an alternating automaton. The memory of the automaton is structured in a way that strictly corresponds to scopes of the binders used in the constructed proof. This provides an application of automata-theoretic techniques in proof theory.

This paper introduces Allen's extended interval logic whose sentences are Boolean combinations of sentences of Allen's interval logic with metric constraints on time points. For this extended logic, a deduction method based on analytic tableaux is defined. This method is used for answering queries on ontologies specified in Allen's extended interval logic. An example illustrating the applicability of this extended logic to the problem of workflow specification is presented.

We prove that the problem of tabularity over Johansson’s minimal logic J is decidable. Describing all pretabular extensions of the minimal logic, we find that there are seven of them and show that they are all recognizable over J. We find axiomatizations and semantic characterizations of all seven pretabular logics.

MTL is a Monoidal t-norm based logic introduced by Esteva and Godo by omitting divisibility axiom from H´ajek's Basic logic (BL). Many logics can be obtained by adding axioms to MTL logic. Logic system WBL is obtained by adding weak divisibility axiom to logic system MTL. Logic system WMV is obtained by adding involution axiom to logic system WBL. WBL-algebra corresponding to logic system WBL and WMV-algebra to logic system WMV are defined respectively. It is proved that the both of logic system Luk and logic system Nilpotent minimum (NM) are the schematic extensions of logic system WMV. Weak Wajsberg algebra and the simplified form of logic system WMV are obtained.

A new logic is presented without predicates—except equality. Yet its expressive power is the same as that of predicate logic, and relations can faithfully be represented in it. In this logic we also develop an alternative for set theory. There is a need for such a new approach, since we do not live in a world of sets and predicates, but rather in a world of things with relations between them.

The semantics of the predicate logic based on the absolute arithmetical realizability is proved to differ from the semantics based on the primitive recursive realizability by Salehi.

We deal with size reduction of concept lattices by means of factorization by block relations defined on corresponding formal context. We show that all block relations with a multiplication defined by means of relational composition form a (non-commutative) residuated lattice. Such residuated lattice can be then thought of as a scale of truth degrees using which we evaluate formulas of predicate logic specifying the desired parameters of the factorization. We also introduce efficient algorithms computing operations on a residuated lattice of block relations. The naive way how to design such algorithms is to compute all the formal concepts of a given context in advance, and then apply some well-known properties of residuated lattices. Our algorithms get rid of the time-consuming precomputation of all concepts.

The present author developed a calculus for the logic of ‘because’. In a recent paper in this journal, it has been claimed that the central inference rules for the logic are invalid and that the intuition upon which the rules are based is not accounted for. This note criticises these arguments and presents an independent argument in favour of the rules used in the logic.

This article investigates the role of arity of second-order quantifiers in existential second-order logic, also known as Σ 1 1 . We identify fragments L of Σ 1 1 where second-order quantification of relations of arity k 1 is (nontrivially) vacuous in the sense that each formula of L can be translated to a formula of (a fragment of) monadic Σ 1 1 . Let polyadic Boolean modal logic with identity ( PBML = ) be the logic obtained by extending standard polyadic multimodal logic with built-in identity modalities and with constructors that allow for the Boolean combination of accessibility relations. Let Σ 1 1 ( PBML = ) be the extension of PBML = with existential prenex quantification of accessibility relations and proposition symbols. The principal result of the article is that Σ 1 1 ( PBML = ) translates into monadic Σ 1 1 . As a corollary, we obtain a variety of decidability results for multimodal logic. The translation can also be seen as a step towards establishing whether every property of finite directed graphs expressible in Σ 1 1 ( FO 2 ) is also expressible in monadic Σ 1 1 . This question was left open in the 1999 paper of Gradel and Rosen in the 14th Annual IEEE Symposium on Logic in Computer Science.

This paper is devoted to study of the logic corresponding to intervals of the real line, where the modality is interpreted as "after." Since this logic is finitely axiomatizable, the proof of the finite model property given in the paper implies its decidability. Also, a description of the class of finite rooted Kripke frames corresponding to this logic is provided.

Compositionality is at the heart of model theoretical semantics, and the most common way of doing truth value semantics for natural language (NL) is to translate a fragment of NL into some extensions of classical predicate logic. Yet, somewhat ironically and strangely enough, predicate logic itself is not compositional, because the truth conditions for quantification as usually stated are not a function of the denotations of its parts but depend on value assignments for variables. That this kind of dependence on value assignments leads to non-compositionality is well-known and will be demonstrated explicitly in section 1.3. One could, as is also well-known, remedy this awkwardness by considering not truth values as denotations of formulas but sets of value assignments for variables. As we will show in 1.4, such a semantics is compositional, but now an additional problem emerges, namely the lack of alphabetical “innocence” (or “invariance”) in that the denotation of P(x) is different from that of P(y) although the formulas are mere alphabetic variants of each other.1 This new problem is related to what Fine (2007), p. 7, calls the “antinomy of the variable”