A simple logic for reasoning about incomplete knowledge

The semantics of modal logics for reasoning about belief or knowledge is often described in terms of accessibility relations, which is too expressive to account for mere epistemic states of an agent. This paper proposes a simple logic whose atoms express epistemic attitudes about formulae expressed in another basic propositional language, and that allows for conjunctions, disjunctions and negations of belief or knowledge statements. It allows an agent to reason about what is known about the beliefs held by another agent. This simple epistemic logic borrows its syntax and axioms from the modal logic KD. It uses only a fragment of the S5 language, which makes it a two-tiered propositional logic rather than as an extension thereof. Its semantics is given in terms of epistemic states understood as subsets of mutually exclusive propositional interpretations. Our approach offers a logical grounding to uncertainty theories like possibility theory and belief functions. In fact, we define the most basic logic for possibility theory as shown by a completeness proof that does not rely on accessibility relations.     

Categories with families and first-order logic with dependent sorts

First-order logic with dependent sorts, such as Makkai's first-order logic with dependent sorts (FOLDS), or Aczel's and Belo's dependently typed (intuitionistic) first-order logic (DFOL), may be regarded as logic enriched dependent type theories. Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Löf type theory. We introduce in this article a notion of hyperdoctrine over a cwf, and show how FOLDS and DFOL fit in this semantical framework. A soundness and completeness theorem is proved for DFOL. The semantics is functorial in the sense of Lawvere, and uses a dependent version of the Lindenbaum-Tarski algebra for a DFOL theory. Agreement with standard first-order semantics is established. Applications of DFOL to constructive mathematics and categorical foundations are given. A key feature is a local propositions-as-types principle.     

An epistemic model of an agent who does not reflect on reasoning processes

This paper introduces an epistemic model of a boundedly rational agent under the two assumptions that (i) the agent’s reasoning process is in accordance with the model but (ii) the agent does not reflect on these reasoning processes. For such a concept of bounded rationality a semantic interpretation by the possible world semantics of the Kripke (1963) type is no longer available because the definition of knowledge in these possible world semantics implies that the agent knows all valid statements of the model. The key to my alternative semantic approach is the extension of the method of truth tables, first introduced for the propositional logic by Wittgenstein (1922), to an epistemic logic so that I can determine the truth value of epistemic statements for all relevant truth conditions. In my syntactic approach I define an epistemic logic–consisting of the classical calculus of propositional logic plus two knowledge axioms–that does not include the inference rule of necessitation, which claims that an agent knows all theorems of the logic. As my main formal result I derive a determination theorem linking my semantic with my syntactic approach. The difference between my approach and existing knowledge models is illustrated in a game-theoretic application concerning the epistemic justification of iterative solution concepts.     

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.     

Sémantique de type Kripke d'un système logique basé sur un ensemble ordonné fini

In order to modelize the reasoning of intelligent agents represented by a poset T, H. Rasiowa introduced logic systems called “Approximation Logics”. In these systems the use of a set of constants constitutes a fundamental tool. We have introduced in [8] a logic system called without this kind of constants but limited to the case that T is a finite poset. We have proved a completeness result for this system w.r.t. an algebraic semantics. We introduce in this paper a Kripke‐style semantics for a subsystem of for which there existes a deduction theorem. The set of “possible worldsr is enriched by a family of functions indexed by the elements of T and satisfying some conditions. We prove a completeness result for system with respect to this Kripke semantics and define a finite Kripke structure that characterizes the propositional fragment of logic . We introduce a reational semantics (found by E. Orlowska) which has the advantage to allow an interpretation of the propositionnal logic using only binary relations. We treat also the computational complexity of the satisfiability problem of the propositional fragment of logic .     

Sémantique algébrique ďun système logique basé sur un ensemble ordonné fini

In order to modelize the reasoning of an intelligent agent represented by a poset T, H. Rasiowa introduced logic systems called “Approximation Logics”. In these systems a set of constants constitutes a fundamental tool. In this papers, we consider logic systems called L′_T without this kind of constants but limited to the case where T is a finite poset. We prove a weak deduction theorem. We introduce also an algebraic semantics using Hey ting algebra with operators. To prove the completeness theorem of the L′_T system with respect to the algebraic semantics, we use the method of H. Rasiowa and R. Sikorski for first order logic. In the propositional case, a corollary allows us to assert that it is decidable to know “if a propositional formula is valid”. We study also certain relations between the L′_T logic and the intuitionistic and classical logics.     

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)     

Canonical extensions of double quasioperator algebras: An algebraic perspective on duality for certain algebras with binary operations

The context for this paper is a class of distributive lattice expansions, called double quasioperator algebras (DQAs). The distinctive feature of these algebras is that their operations preserve or reverse both join and meet in each coordinate. Algebras of this type provide algebraic semantics for certain non-classical propositional logics. In particular, MV-algebras, which model the ?ukasiewicz infinite-valued logic, are DQAs.Varieties of DQAs are here studied through their canonical extensions. A variety of this type having additional operations of arity at least 2 may fail to be canonical; it is already known, for example, that the variety of MV-algebras is not. Non-canonicity occurs when basic operations have two distinct canonical extensions and both are necessary to capture the structure of the original algebra. This obstruction to canonicity is different in nature from that customarily found in other settings. A generalized notion of canonicity is introduced which is shown to circumvent the problem. In addition, generalized canonicity allows one to capture on the canonical extensions of DQAs the algebraic operations in such a way that the laws that these obey may be translated into first-order conditions on suitable frames. This correspondence may be seen as the algebraic component of duality, in a way which is made precise.In many cases of interest, binary residuated operations are present. An operation h which, coordinatewise, preserves ∨ and 0 lifts to an operation which is residuated, even when h is not. If h also preserves binary meet then the upper adjoints behave in a functional way on the frames.     

On Binary Computation Structures

Based on a modification of Moss' and Parikh's topological modal language [8], we study a generalization of a weakly expressive fragment of a certain propositional modal logic of time. We define a bimodal logic comprising operators for knowledge and nexttime. These operators are interpreted in binary computation structures. We present an axiomatization of the set T of theorems valid for this class of semantical domains and prove – as the main result of this paper – its completeness. Moreover, the question of decidability of T is treated.     

Fibered universal algebra for first-order logics

We extend Lawvere-Pitts prop-categories (aka. hyperdoctrines) to develop a general framework for providing fibered algebraic semantics for general first-order logics. This framework includes a natural notion of substitution, which allows first-order logics to be considered as structural closure operators just as propositional logics are in abstract algebraic logic. We then establish an extension of the homomorphism theorem from universal algebra for generalized prop-categories and characterize two natural closure operators on the prop-categorical semantics. The first closes a class of structures (which are interpreted as morphisms of prop-categories) under the satisfaction of their common first-order theory and the second closes a class of prop-categories under their associated first-order consequence. It turns out that these closure operators have characterizations that closely mirror Birkhoff's characterization of the closure of a class of algebras under the satisfaction of their common equational theory and Blok and Jónsson's characterization of closure under equational consequence, respectively. These algebraic characterizations of the first-order closure operators are unique to the prop-categorical semantics. They do not have analogues, for example, in the Tarskian semantics for classical first-order logic. The prop-categories we consider are much more general than traditional intuitionistic prop-categories or triposes (i.e., topos representing indexed partially ordered sets). Nonetheless, to the best of our knowledge, our results are new, even when restricted to these special classes of prop-categories.     

Formal similarities and differences among qualitative conditional semantics

Various semantics have been used for conditionals in the area of knowledge representation and reasoning. In this paper, we study similarities and differences between a purely qualitative semantics based on the popular system-of-spheres semantics of Lewis, an ordinal semantics making use of rankings, a possibilistic semantics, and a semantics representing conditionals by probabilities in a qualitative way. As a common framework for the corresponding logics, we use Goguen and Burstall’s notion of institutions whose central motto is that truth is invariant under the change of notation. The institution framework provides the formal rigidity needed for our investigation, but leaves enough abstract freedom to formalize and compare quite different logics. We show precisely in which sense the conditional semantics mentioned above are logically similar, and point out the semantical subtleties each semantics allows.     

On Non-Deterministic Quantification

This paper offers a framework for extending Arnon Avron and Iddo Lev’s non-deterministic semantics to quantified predicate logic with the intent of resolving several problems and limitations of Avron and Anna Zamansky’s approach. By employing a broadly Fregean picture of logic, the framework described in this paper has the benefits of permitting quantifiers more general than Walter Carnielli’s distribution quantifiers and yielding a well-behaved model theory. This approach is purely objectual and yields the semantical equivalence of both α-equivalent formulae and formulae differing only by codenotative terms. Finally, we make a brief excursion into non-deterministic model theory, proving a strong ?o?’ Theorem and compactness for all finitely-valued, non-deterministic logics whose quantifiers have intensions describable in a first order metalanguage.     

A bipolar model of assertability and belief

Valuation pairs are introduced as a bipolar model of the assertability of propositions. These correspond to a pair of dual valuation functions, respectively, representing the strong property of definite assertability and the dual weaker property of acceptable assertability. In the case where there is uncertainty about the correct valuation pair for a language then a probability distribution is defined on possible valuation pairs. This results in two measures, μ⁺ giving the probability that a sentence is definitely assertable, and μ⁻ giving the probability that a sentence is acceptable to assert. It is shown that μ⁺ and μ⁻ can be determined directly from a two dimensional mass function m defined on pairs of sets of propositional variables. Certain natural properties of μ⁺ and μ⁻ are easily expressed in terms of m, and in particular we introduce certain consonance or nestedness assumptions. These capture qualitative information in the form of assertability orderings for both the propositional variables and the negated propositional variables. On the basis of these consonance assumptions we show that label semantics, intuitionistic fuzzy logic and max-min fuzzy logic can all be viewed as special cases of this bipolar model. We also show that bipolar belief measures can be interpreted within an interval-set model.     

The algebra of fuzzy logic

In the following, human thinking based on premises with no complete truth value is reviewed for controlling the algebra of fuzzy sets operations. Assuming a system may be developed in this sphere, it should be considered as the algebra of fuzzy sets, as the same algebra is satisfied by classical logic and sets. As will be proved, this algebra is not a lattice and consequently the Zadeh definitions do not constitute an adequate representation. The binary operations of my algebra are “interactive” types. An axiom system is given that, in my opinion, is the foundation of the conception, adequately and without redundancy. The agreement of the theorems deduced from the axiom system with the intuitive expectations is shown. A special arithmetical structure satisfying this algebra is given, and the relation between this structure and the theory of probability is analyzed.Adapting a process of classical logics, fuzzy quantifiers are defined on the basis of the operations of propositional algebra. A “qualifier” is also defined. The qualifier is functional; applying it to Ax we get the statement “usually Ax” s a middle cource between the statements “at least once Ax” and “always Ax”. The concept of entailment of fuzzy logics is introduced. This concept is an innovative generalization of the classical deduction theory, opposite to the concept of entailment of classical multi-valued logics. An important error of the abbreviated system of notation of the fuzzy theory [e.g. m(x, AvB)] appears: the functional type operations (e.g. quantifiers) cannot be interpreted in propositional calculus. Therefore a new system of symbols is proposed in this paper.     

A Routley–Meyer Semantics for Gödel 3-Valued Logic and Its Paraconsistent Counterpart

Routley–Meyer semantics (RM-semantics) is defined for Gödel 3-valued logic G3 and some logics related to it among which a paraconsistent one differing only from G3 in the interpretation of negation is to be remarked. The logics are defined in the Hilbert-style way and also by means of proof-theoretical and semantical consequence relations. The RM-semantics is defined upon the models for Routley and Meyer’s basic positive logic B₊, the weakest positive RM-semantics. In this way, it is to be expected that the models defined can be adapted to other related many-valued logics.     

Actualism and Modal Semantics

According to actualism, modal reality is constructed out of valuations (combinations of truth values for all propositions). According to possibilism, modal reality consists in a set of possible worlds, conceived as independent objects that assign truth values to propositions. According to possibilism, accounts of modal reality can intelligibly disagree with each other even if they agree on which valuations are contained in modal reality. According to actualism, these disagreements (possibilist disagreements) are completely unintelligible. An essentially actualist semantics for modal propositional logic specifies which sets of valuations are compatible with the meanings of the truth-functional connectives and modal operators without drawing on formal resources that would enable us to represent possibilist disagreements. The paper discusses the availability of an essentially actualist semantics for modal propositional logic. I argue that the standard Kripkean semantics is not essentially actualist and that other extant approaches also fail to provide a satisfactory essentially actualist semantics. I end by describing an essentialist actualist semantics for modal propositional logic.     

A Sahlqvist theorem for distributive modal logic

In this paper we consider distributive modal logic, a setting in which we may add modalities, such as classical types of modalities as well as weak forms of negation, to the fragment of classical propositional logic given by conjunction, disjunction, true, and false. For these logics we define both algebraic semantics, in the form of distributive modal algebras, and relational semantics, in the form of ordered Kripke structures. The main contributions of this paper lie in extending the notion of Sahlqvist axioms to our generalized setting and proving both a correspondence and a canonicity result for distributive modal logics axiomatized by Sahlqvist axioms. Our proof of the correspondence result relies on a reduction to the classical case, but our canonicity proof departs from the traditional style and uses the newly extended algebraic theory of canonical extensions.     

Inquisitive logic as an epistemic logic of knowing how

In this paper, we present an alternative interpretation of propositional inquisitive logic as an epistemic logic of knowing how. In our setting, an inquisitive logic formula α being supported by a state is formalized as knowing how to resolve α (more colloquially, knowing how α is true) holds on the S5 epistemic model corresponding to the state. Based on this epistemic interpretation, we use a dynamic epistemic logic with both know-how and know-that operators to capture the epistemic information behind the innocent-looking connectives in inquisitive logic. We show that the set of valid know-how formulas corresponds precisely to the inquisitive logic. The main result is a complete axiomatization with intuitive axioms using the full dynamic epistemic language. Moreover, we show that the know-how operator and the dynamic operator can both be eliminated without changing the expressivity over models, which is consistent with the modal translation of inquisitive logic existing in the literature. We hope our framework can give an intuitive alternative interpretation to various concepts and technical results in inquisitive logic, and also provide a powerful and flexible tool to handle both the inquisitive reasoning and declarative reasoning in an epistemic context.