Infinite-Valued First-Order Łukasiewicz Logic: Hypersequent Calculi Without Structural Rules and Proof Search for Sentences in the Prenex Form

The rational first-order Pavelka logic is an expansion of the infinite-valued first-order ?ukasiewicz logic ?? by truth constants. For this logic, we introduce a cumulative hypersequent calculus G¹?? and a noncumulative hypersequent calculus G²?? without structural inference rules. We compare these calculi with the Baaz–Metcalfe hypersequent calculus G?? with structural rules. In particular, we show that every G??-provable sentence is G¹??-provable and a ??-sentence in the prenex form is G??-provable if and only if it is G²??-provable. For a tableau version of the calculus G²??, we describe a family of proof search algorithms that allow us to construct a proof of each G²??-provable sentence in the prenex form.     

Turning cycles into spirals

In [13] Parikh proved the first mathematical result about concrete consistency of contradictory theories. In [6] it is shown that the bounds of concrete consistency given by Parikh are optimal. This was proved by noting that very large numbers can be actually constructed through very short proofs. A more refined analysis of these short proofs reveals the presence of cyclic paths in their logical graphs. Indeed, in [6] it is shown that cycles need to exist for the proofs to be short. Here, we present a new sequent calculus for classical logic which is close to linear logic in spirit, enjoys cut-elimination, is acyclic and its proofs are just elementary larger than proofs in LK. The proofs in the new calculus can be obtained by a small perturbation of proofs in LK and they represent a geometrical alternative for studying structural properties of LK-proofs. They satisfy the constructive disjunction property and most important, simpler geometrical properties of their logical graphs. The geometrical counterpart to a cycle in LK is represented in the new setting by a spiral which is passing through sets of formulas logically grouped together by the nesting of their quantifiers.     

A sequent calculus for logic of knowledge and past time: Completeness and decidability

We consider logic of knowledge and past time. This logic involves the discrete-time linear temporal operators next, until, weak yesterday, and since. In addition, it contains an indexed set of unary modal operators agent i knows.We consider the semantic constraint of the unique initial states for this logic. For the logic, we present a sequent calculus with a restricted cut rule. We prove the soundness and completeness of the sequent calculus presented. We prove the decidability of provability in the considered calculus as well. So, this calculus can be used as a basis for automated theorem proving. The proof method for the completeness can be used to construct complete sequent calculi with a restricted cut rule for this logic with other semantical constraints as well. Published in Lietuvos Matematikos Rinkinys, Vol. 46, No. 3, pp. 427–437, July–September, 2006.     

Labeled sequent calculus for justification logics

Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for combined modal-justification logics. Using a method due to Sara Negri, we internalize the Kripke-style semantics of justification and modal-justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculi. We show that all rules of these systems are invertible and the structural rules (weakening and contraction) and the cut rule are admissible. Soundness and completeness are established as well. The analyticity for some of our labeled sequent calculi are shown by proving that they enjoy the subformula, sublabel and subterm properties. We also present an analytic labeled sequent calculus for $\mathsf{S4LPN}$ based on Artemov–Fitting models.     

A focused approach to combining logics

We present a compact sequent calculus LKU for classical logic organized around the concept of polarization. Focused sequent calculi for classical, intuitionistic, and multiplicative-additive linear logics are derived as fragments of the host system by varying the sensitivity of specialized structural rules to polarity information. We identify a general set of criteria under which cut-elimination holds in such fragments. From cut-elimination we derive a unified proof of the completeness of focusing. Furthermore, each sublogic can interact with other fragments through cut. We examine certain circumstances, for example, in which a classical lemma can be used in an intuitionistic proof while preserving intuitionistic provability. We also examine the possibility of defining classical-linear hybrid logics.     

Hypersequent calculi for intuitionistic logic with classical atoms

We discuss a propositional logic which combines classical reasoning with constructive reasoning, i.e., intuitionistic logic augmented with a class of propositional variables for which we postulate the decidability property. We call it intuitionistic logic with classical atoms. We introduce two hypersequent calculi for this logic. Our main results presented here are cut-elimination with the subformula property for the calculi. As corollaries, we show decidability, an extended form of the disjunction property, the existence of embedding into an intuitionistic modal logic and a partial form of interpolation.     

Extracting BB′IW Inhabitants of Simple Types From Proofs in the Sequent Calculus {LT_\to^{t}} for Implicational Ticket Entailment

The decidability of the logic of pure ticket entailment means that the problem of inhabitation of simple types by combinators over the base { B, B′, I, W } is decidable too. Type-assignment systems are often formulated as natural deduction systems. However, our decision procedure for this logic, which we presented in earlier papers, relies on two sequent calculi and it does not yield directly a combinator for a theorem of ${T_\to}$ . Here we describe an algorithm to extract an inhabitant from a sequent calculus proof—without translating the proof into another proof system.     

Finite Models of Some Substructural Logics

We give a proof of the finite model property (fmp) of some fragments of commutative and noncommutative linear logic: the Lambek calculus, BCI, BCK and their enrichments, MALL and Cyclic MALL. We essentially simplify the method used in [4] for proving fmp of BCI and the Lambek ca culus and in [5] for proving fmp of MALL. Our construction of finite models also differs from that used in Lafont [8] in his proof of fmp of MALL (we do not use cut elimination).     

Loop-free calculus for modal logic S4. II

In [J. Andrikonis, Loop-free calculus for modal logic S4. I, Lith. Math. J., 52(1):1–12, 2012], loop-free calculus for modal logic S4 is presented. The calculus uses several types of indexes to avoid loops and obtain termination of derivation search. Although the mentioned article proves that derivation search in the calculus is finite, the proof of soundness and completeness is omitted and, therefore, is presented in this paper. Moreover, this paper presents loop-free calculus for modal logics K4, which is obtained by modifying the calculus for S4. Finally, some remarks for programming the given calculi are offered.     

Saturated calculus for Horn-like sequents of a complete class of a linear temporal first order logic

A saturated calculus for the so-called Horn-like sequents of a complete class of a linear temporal logic of the first order is described. The saturated calculus contains neither induction-like postulates nor cut-like rules. Instead of induction-like postulates the saturated calculus contains a finite set of “saturated” sequents, which (1) capture and reflect the periodic structure of inductive reasoning (i.e., a reasoning which applies induction-like postulates); (2) show that “almost nothing new” can be obtained by continuing the process of derivation of a given sequent; (3) present an explicit way of generating the so-called invariant formula in induction-like rules. The saturated calculus for Horn-like sequents allows one: (1) to prove in an obvious way the completeness of a restricted linear temporal logic of the first order; (2) to construct a computer-aided proof system for this logic; (3) to prove the decidability of this logic for logically decidable Horn-like sequents. Bibliography: 15 titles. Translated fromZapiski Nauchnykh Seminarov POMI, Vol. 220, 1995, pp. 123–144. Translated by R. Pliuškevičius.     

The polynomial bounds of proof complexity in Frege systems

The concept of a determinative set of variables for a propositional formula was introduced by one of the authors, which made it possible to distinguish the set of hard-determinable formulas. The proof complexity of a formula of this sort has exponential lower bounds in some proof systems of classical propositional calculus (cut-free sequent system, resolution system, analytic tableaux, cutting planes, and bounded Frege systems). In this paper we prove that the property of hard-determinability is insufficient for obtaining a superpolynomial lower bound of proof lines (sizes) in Frege systems: an example of a sequence of hard-determinable formulas is given whose proof complexities are polynomially bounded in every Frege system.     

Two-sided estimates for essential height in Shirshov’s Height Theorem

The paper is focused on two-sided estimates for the essential height in Shirshov??s Height Theorem. The concepts of the selective height and strong n-divisibility directly related to the height and n-divisibility are introduced. We prove lower and upper bounds for the selective height over nonstrongly n-divisible words of length 2. For any n and sufficiently large l these bounds differ at most twice. The case of words of length 3 is also studied. The case of words of length 2 can be generalized to the proof of an upper exponential estimate in Shirshov??s Height Theorem. The proof uses the idea of V.N. Latyshev related to the application of Dilworth??s theorem to the study of non n-divisible words.     

Circuit lower bounds and linear codes

In 1977, Valiant proposed a graph-theoretical method for proving lower bounds on algebraic circuits with gates computing linear functions. He used this method to reduce the problem of proving lower bounds on circuits with linear gates to proving lower bounds on the rigidity of a matrix, a notion that he introduced in that paper. The largest lower bound for an explicitly given matrix is due to J. Friedman, who proved a lower bound on the rigidity of the generator matrices of error-correcting codes over finite fields. He showed that the proof can be interpreted as a bound on a certain parameter defined for all linear spaces of finite dimension. In this note, we define another parameter that can be used to prove lower bounds on circuits with linear gates. Our parameter may be larger than Friedman’s, and it seems incomparable with rigidity, hence it may be easier to prove a lower bound using this notion. Bibliography: 14 titles. Published in Zapiski Nauchnykh Seminarov POMI, Vol. 316, 2004, pp. 188–204.     

Examining the role of examples in proving processes through a cognitive lens: the case of triangular numbers

In this paper, we analyze the role of examples in the proving process. The context chosen for this study was finding a general rule for triangular numbers. The aim of this paper is to show that examples are effective for the construction of a proof when they allow cognitive unity and structural continuity between argumentation and proof. Continuity in the structure is possible if the inductive argumentation is based on process pattern generalization (PPG), but this is not the case if a generalization is made on the results. Moreover, the PPG favors the development of generic examples that support cognitive unity and structural continuity between the argumentation and proof. The cognitive analysis presented in this paper is performed through Toulmin??s model.     

Two proving strategies of highly successful mathematics majors

We examined the proof-writing behaviors of six highly successful mathematics majors on novel proving tasks in calculus. We found two approaches that these students used to write proofs, which we termed the targeted strategy and the shotgun strategy. When using a targeted strategy students would develop a strong understanding of the statement they were proving, choose a plan based on this understanding, develop a graphical argument for why the statement is true, and formalize this graphical argument into a proof. When using a shotgun strategy, students would begin trying different proof plans immediately after reading the statement and would abandon a plan at the first sign of difficulty. The identification of these two strategies adds to the literature on proving by informing how elements of existing problem-solving models interrelate.     

Reliability bounds on HNBUE life distributions with known first two moments

In this paper, we study upper and lower bounds for the reliability function in harmonic new better than used in expectation (HNBUE) life distribution class with known first two moments. Here we say a life distribution has HNBUE property if the integral harmonic mean value of the residual life in any interval [0,t] is no more than its mean. By a constructive proof, we determine the lower and upper reliability bounds analytically and show that these bounds are all sharp.     

On standard models of fuzzy region connection calculus

The Region Connection Calculus (RCC) is perhaps the most influential topological relation calculus. Based on the first-order logic, the RCC, however, does not fully meet the needs of applications where the vagueness of entities or relations is important and not ignorable. This paper introduces standard models for the fuzzy region connection calculus (RCC) proposed by Schockaert et al. (2008) [18]. Each of such a standard fuzzy RCC model is induced by a standard RCC model in a natural way. We prove that each standard fuzzy RCC model is canonical in the sense that any satisfiable set of fuzzy RCC8 constraints have a solution in it. A polynomial realization algorithm is also provided. As a side product, we show similar sets of fuzzy constraints have similar solutions if both are satisfiable. This allows us to approximate fuzzy RCC constraints that have arbitrary bounds by those have bounds with finite precision.     

Combinatorics of Monotone Computations

, and (ii) arbitrary real-valued non-decreasing functions on variables. This resolves a problem, raised by Razborov in 1986, and yields, in a uniform and easy way, non-trivial lower bounds for circuits computing explicit functions even when . The proof is relatively simple and direct, and combines the bottlenecks counting method of Haken with the idea of finite limit due to Sipser. We demonstrate the criterion by super-polynomial lower bounds for explicit Boolean functions, associated with bipartite Paley graphs and partial t-designs. We then derive exponential lower bounds for clique-like graph functions of Tardos, thus establishing an exponential gap between the monotone real and non-monotone Boolean circuit complexities. Since we allow real gates, the criterion also implies corresponding lower bounds for the length of cutting planes proof in the propositional calculus. Received: July 2, 1996/Revised: Revised June 7, 1998     

THE FUNDAMENTAL THEOREM OF ULTRAPRODUCT IN PAVELKA'S LOGIC

In [This Zeitschrift 25 (1979), 45-52, 119-134, 447-464], Pavelka systematically discussed propositional calculi with values in enriched residuated lattices and developed a general framework for approximate reasoning. In the first part of this paper we introduce the concept of generalized quantifiers into Pavelka's logic and establish the fundamental theorem of ultraproduct in first order Pavelka's logic with generalized quantifiers. In the second part of this paper we show that the fundamental theorem of ultraproduct in first order Pavelka's logic is preserved under some direct product of lattices of truth values.