scholarly journals Possible world semantics for first-order logic of proofs

2014 ◽  
Vol 165 (1) ◽  
pp. 225-240 ◽  
Author(s):  
Melvin Fitting
Author(s):  
Gerhard Lakemeyer ◽  
Hector J. Levesque

In a recent paper Lakemeyer and Levesque proposed a first-order logic of limited belief to characterize the beliefs of a knowledge base (\KB). Among other things, they show that their model of belief is expressive, eventually complete, and tractable. This means, roughly, that a \KB\ may consist of arbitrary first-order sentences, that any sentence which is logically entailed by the \KB\ is eventually believed, given enough reasoning effort, and that reasoning is tractable under reasonable assumptions. One downside of the proposal is that epistemic states are defined in terms of sets of clauses, possibly containing variables, giving the logic a distinct syntactic flavour compared to the more traditional possible-world semantics found in the literature on epistemic logic. In this paper we show that the same properties as above can be obtained by defining epistemic states as sets of three-valued possible worlds. This way we are able to shed new light on those properties by recasting them using the more familiar notion of truth over possible worlds.


2013 ◽  
Vol 2013 ◽  
pp. 1-10
Author(s):  
Zoran Majkić

We considered an extension of the first-order logic (FOL) by Bealer's intensional abstraction operator. Contemporary use of the term “intension” derives from the traditional logical Frege-Russell doctrine that an idea (logic formula) has both an extension and an intension. Although there is divergence in formulation, it is accepted that the “extension” of an idea consists of the subjects to which the idea applies, and the “intension” consists of the attributes implied by the idea. From the Montague's point of view, the meaning of an idea can be considered as particular extensions in different possible worlds. In the case of standard FOL, we obtain a commutative homomorphic diagram, which is valid in each given possible world of an intensional FOL: from a free algebra of the FOL syntax, into its intensional algebra of concepts, and, successively, into an extensional relational algebra (different from Cylindric algebras). Then we show that this composition corresponds to the Tarski's interpretation of the standard extensional FOL in this possible world.


2001 ◽  
Vol 1 (4) ◽  
pp. 475-490 ◽  
Author(s):  
S. Artemov ◽  
T. Yavorskaya (Sidon)

2009 ◽  
Vol 19 (12) ◽  
pp. 3091-3099 ◽  
Author(s):  
Gui-Hong XU ◽  
Jian ZHANG

Author(s):  
Tim Button ◽  
Sean Walsh

Chapters 6-12 are driven by questions about the ability to pin down mathematical entities and to articulate mathematical concepts. This chapter is driven by similar questions about the ability to pin down the semantic frameworks of language. It transpires that there are not just non-standard models, but non-standard ways of doing model theory itself. In more detail: whilst we normally outline a two-valued semantics which makes sentences True or False in a model, the inference rules for first-order logic are compatible with a four-valued semantics; or a semantics with countably many values; or what-have-you. The appropriate level of generality here is that of a Boolean-valued model, which we introduce. And the plurality of possible semantic values gives rise to perhaps the ‘deepest’ level of indeterminacy questions: How can humans pin down the semantic framework for their languages? We consider three different ways for inferentialists to respond to this question.


2020 ◽  
Author(s):  
Michał Walicki

Abstract Graph normal form, introduced earlier for propositional logic, is shown to be a normal form also for first-order logic. It allows to view syntax of theories as digraphs, while their semantics as kernels of these digraphs. Graphs are particularly well suited for studying circularity, and we provide some general means for verifying that circular or apparently circular extensions are conservative. Traditional syntactic means of ensuring conservativity, like definitional extensions or positive occurrences guaranteeing exsitence of fixed points, emerge as special cases.


1991 ◽  
Vol 15 (2) ◽  
pp. 123-138
Author(s):  
Joachim Biskup ◽  
Bernhard Convent

In this paper the relationship between dependency theory and first-order logic is explored in order to show how relational chase procedures (i.e., algorithms to decide inference problems for dependencies) can be interpreted as clever implementations of well known refutation procedures of first-order logic with resolution and paramodulation. On the one hand this alternative interpretation provides a deeper insight into the theoretical foundations of chase procedures, whereas on the other hand it makes available an already well established theory with a great amount of known results and techniques to be used for further investigations of the inference problem for dependencies. Our presentation is a detailed and careful elaboration of an idea formerly outlined by Grant and Jacobs which up to now seems to be disregarded by the database community although it definitely deserves more attention.


2019 ◽  
Vol 29 (8) ◽  
pp. 1311-1344 ◽  
Author(s):  
Lauri T Hella ◽  
Miikka S Vilander

Abstract We propose a new version of formula size game for modal logic. The game characterizes the equivalence of pointed Kripke models up to formulas of given numbers of modal operators and binary connectives. Our game is similar to the well-known Adler–Immerman game. However, due to a crucial difference in the definition of positions of the game, its winning condition is simpler, and the second player does not have a trivial optimal strategy. Thus, unlike the Adler–Immerman game, our game is a genuine two-person game. We illustrate the use of the game by proving a non-elementary succinctness gap between bisimulation invariant first-order logic $\textrm{FO}$ and (basic) modal logic $\textrm{ML}$. We also present a version of the game for the modal $\mu $-calculus $\textrm{L}_\mu $ and show that $\textrm{FO}$ is also non-elementarily more succinct than $\textrm{L}_\mu $.


Sign in / Sign up

Export Citation Format

Share Document