Comments on some versions of intuitionistic fuzzy propositional calculus due to K. Atanassov and G. Gargov

We show that the versions of intuitionistic fuzzy propositional calculus given in Definitions 6 and 7 in Atanassov and Gargov (Fuzzy Sets and Systems 95 (1998) 39–52) do not satisfy modus ponens. Furthermore, we show that the version of intuitionistic fuzzy propositional calculus given in Definition 8 by Atanassov and Gargov is incorrect.     

A proof-search procedure for intuitionistic propositional logic

A sequent root-first proof-search procedure for intuitionistic propositional logic is presented. The procedure is obtained from modified intuitionistic multi-succedent and classical sequent calculi, making use of Glivenko’s Theorem. We prove that a sequent is derivable in a standard intuitionistic multi-succedent calculus if and only if the corresponding prefixed-sequent is derivable in the procedure.     

Uniform interpolation and the existence of sequent calculi

This paper presents a uniform and modular method to prove uniform interpolation for several intermediate and intuitionistic modal logics. The proof-theoretic method uses sequent calculi that are extensions of the terminating sequent calculus $\mathsf{G4ip}$ for intuitionistic propositional logic. It is shown that whenever the rules in a calculus satisfy certain structural properties, the corresponding logic has uniform interpolation. It follows that the intuitionistic versions of $\mathsf{K}$ and $\mathsf{KD}$ (without the diamond operator) have uniform interpolation. It also follows that no intermediate or intuitionistic modal logic without uniform interpolation has a sequent calculus satisfying those structural properties, thereby establishing that except for the seven intermediate logics that have uniform interpolation, no intermediate logic has such a sequent calculus.     

A secondary semantics for Second Order Intuitionistic Propositional Logic

In this paper we propose a Kripke‐style semantics for second order intuitionistic propositional logic and we provide a semantical proof of the disjunction and the explicit definability property. Moreover, we provide a tableau calculus which is sound and complete with respect to such a semantics. (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Sequent calculi for propositional star-free likelihood logic

We consider classical, multisuccedent intuitionistic, and intuitionistic sequent calculi for propositional likelihood logic. We prove the admissibility of structural rules and cut rule, invertibility of rules, correctness of the calculi, and completeness of the classical calculus with respect to given semantics.__________Published in Lietuvos Matematikos Rinkinys, Vol. 45, No. 1, pp. 3–21, January–March, 2005.     

A semantic hierarchy for intuitionistic logic

Brouwer’s views on the foundations of mathematics have inspired the study of intuitionistic logic, including the study of the intuitionistic propositional calculus and its extensions. The theory of these systems has become an independent branch of logic with connections to lattice theory, topology, modal logic, and other areas. This paper aims to present a modern account of semantics for intuitionistic propositional systems. The guiding idea is that of a hierarchy of semantics, organized by increasing generality: from the least general Kripke semantics on through Beth semantics, topological semantics, Dragalin semantics, and finally to the most general algebraic semantics. While the Kripke, topological, and algebraic semantics have been extensively studied, the Beth and Dragalin semantics have received less attention. We bring Beth and Dragalin semantics to the fore, relating them to the concept of a nucleus from pointfree topology, which provides a unifying perspective on the semantic hierarchy.     

Answer set programming in intuitionistic logic

As a demonstration of the flexibility of constructive mathematics, we propose an interpretation of propositional answer set programming (ASP) in terms of intuitionistic proof theory, in particular in terms of simply typed lambda calculus. While connections between ASP and intuitionistic logic are well-known, they usually take the form of characterizations of stable models with the help of some intuitionistic theories represented by specific classes of Kripke models. As such the known results are model-theoretic rather than proof-theoretic. In contrast, we offer an explanation of ASP using constructive proofs.     

Complexity of subclasses of the intuitionistic propositional calculus

We investigate the complexity of the decision problem for subclasses of the intuitionistic propositional calculus and present upper bounds for decision procedures locating these subclasses into lower complexity classes like co-NP or polynomial time.     

基础模糊命题演算系统BL~*的改进系统

基础模糊命题演算系统BL*是一个和基础命题演算系统BL相对独立的命题演算系统。命题演算系统L*是系统BL*的扩张,但不是系统BL的扩张。通过对系统BL*及其它模糊命题演算系统的研究,本文对BL*系统进行了修正,进一步改进了BL*系统中的公理体系。     

A Finite Hilbert-Style Axiomatization of the Implication-Less Fragment of the Intuitionistic Propositional Calculus

In this paper we obtain a finite Hilbert-style axiomatization of the implicationless fragment of the intuitionistic propositional calculus. As a consequence we obtain finite axiomatizations of all structural closure operators on the algebra of {–}-formulas containing this fragment. Mathematics Subject Classification: 03B20, 03B22, 06D15.     

Tableau method for residuated logic

Residuated logic is a generalization of intuitionistic logic, which does not assume the idempotence of the conjunction operator. Such generalized conjunction operators have proved important in expert systems (in the area of Approximate Reasoning) and in some areas of Theoretical Computer Science. Here we generalize the intuitionistic tableau procedure and prove that this generalized tableau method is sound for the semantics (the class of residuated algebras) of residuated propositional calculus (RPC). Since the axioms of RPC are complete for the semantics we may conclude that whenever a formula 0 is tableau provable, it is deducible in RPC. We present two different approaches for constructing residuated algebras which give us countermodels for some formulas φ which are not tableau provable. The first uses the fact that the theory of residuated algebras is equational, to construct quotients of free algebras. The second uses finite algebras. We end by discussing a number of open questions.     

Interpreting Intuitionistic Propositional Logic in Terms of Intuitionistic Protothetics

An algebra of sentences of the quite intuitionistic protothetics, that is, an intuitionistic propositional logic with quantifiers augmented by the negation of the excluded middle, is a faithful model of intuitionistic propositional logic.     

Proof analysis in intermediate logics

Using labelled formulae, a cut-free sequent calculus for intuitionistic propositional logic is presented, together with an easy cut-admissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by one or more geometric implications. Each of these logics is embedded by the G?del–McKinsey–Tarski translation into an extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive proof-theoretic methods, without appeal to semantics other than in the explanation of the rules.     

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.     

Note on grammatical translations of logical calculi

It is shown that there exists no grammatical translation into classical (propositional) logic of the modal logics, nor of intuitionistic logic and of the relatedness and dependence logics, as defined in Richard L. Epstein's bookThe Semantic foundations of logic. In the book the result is proved for translations without parameters.Classical propositional logicPC can be translated into other logics. Usually the grammatical structure of propositions is preserved, in the sense of the following definition.     

Realisability for infinitary intuitionistic set theory

We introduce a realisability semantics for infinitary intuitionistic set theory that is based on Ordinal Turing Machines (OTMs). We show that our notion of OTM-realisability is sound with respect to certain systems of infinitary intuitionistic logic, and that all axioms of infinitary Kripke-Platek set theory are realised. Finally, we use a variant of our notion of realisability to show that the propositional admissible rules of (finitary) intuitionistic Kripke-Platek set theory are exactly the admissible rules of intuitionistic propositional logic.     

An intuitionistic formula hierarchy based on high‐school identities

We revisit the notion of intuitionistic equivalence and formal proof representations by adopting the view of formulas as exponential polynomials. After observing that most of the invertible proof rules of intuitionistic (minimal) propositional sequent calculi are formula (i.e., sequent) isomorphisms corresponding to the high‐school identities, we show that one can obtain a more compact variant of a proof system, consisting of non‐invertible proof rules only, and where the invertible proof rules have been replaced by a formula normalization procedure. Moreover, for certain proof systems such as the G4ip sequent calculus of Vorob'ev, Hudelmaier, and Dyckhoff, it is even possible to see all of the non‐invertible proof rules as strict inequalities between exponential polynomials; a careful combinatorial treatment is given in order to establish this fact. Finally, we extend the exponential polynomial analogy to the first‐order quantifiers, showing that it gives rise to an intuitionistic hierarchy of formulas, resembling the classical arithmetical hierarchy, and the first one that classifies formulas while preserving isomorphism.     

New concepts in neutrosophic graphs with application

A neutrosophic set is a generalization of an intuitionistic fuzzy set. Neutrosophic models give more flexibility, precisions and compatibility to the system as compared to intuitionistic fuzzy models. In this research study, we apply the concept of neutrosophic sets to graphs and discuss certain concepts of single-valued neutrosophic graphs. We illustrate the concepts by several examples. We investigate some interesting properties. We describe an application of single-valued neutrosophic graph in decision making process. We also present the procedure of our proposed method as an algorithm.     

A fuzzy logic for an ordinal sum t-norm

Among the class of residuated fuzzy logics, a few of them have been shown to have standard completeness both for propositional and predicate calculus, like Gödel, NM and monoidal t-norm-based logic systems. In this paper, a new residuated logic NMG, which aims at capturing the tautologies of a class of ordinal sum t-norms and their residua, is introduced and its standard completeness both for propositional calculus and for predicate calculus are proved.