Nonmonotonic consequence based on intuitionistic logic

1992 ◽  
Vol 57 (4) ◽  
pp. 1176-1197 ◽  
Author(s):  
Gisèle Fischer Servi
Keyword(s):  
Intuitionistic Logic ◽  
Numerical Approach ◽  
Order Logic ◽  
First Order Logic ◽  
Material Implication ◽  
First Order ◽  
Alternative Approach ◽  
Logical Notion

Research in AI has recently begun to address the problems of nondeductive reasoning, i.e., the problems that arise when, on the basis of approximate or incomplete evidence, we form well-reasoned but possibly false judgments. Attempts to stimulate such reasoning fall into two main categories: the numerical approach is based on probabilities and the nonnumerical one tries to reconstruct nondeductive reasoning as a special type of deductive process. In this paper, we are concerned with the latter usually known as nonmonotonic deduction, because the set of theorems does not increase monotonically with the set of axioms.It is generally acknowledged that nonmonotonic (n.m.) formalisms (e.g., [C], [MC1], [MC2] [MD], [MD-D], [Rl], [R2], [S]) are plagued by a number of difficulties. A key issue concerns the fact that most systems do not produce an axiomatizable set of validities. Thus, the chief objective of this paper is to develop an alternative approach in which the set of n.m. inferences, which somehow qualify as being deductively sound, is r.e.The basic idea here is to reproduce the situation in First Order Logic where the metalogical concept of deduction translates into the logical notion of material implication. Since n.m. deductions are no longer truth preserving, our way to deal with a change in the metaconcept is to extend the standard logic apparatus so that it can reflect the new metaconcept. In other words, the intent is to study a concept of nonmonotonic implication that goes hand in hand with a notion of n.m. deduction. And in our case, it is convenient that the former be characterized within the more tractable context of monotonic logic.

scholarly journals Subformula Linking for Intuitionistic Logic with Application to Type Theory

2021 ◽  
pp. 200-216
Author(s):  
Kaustuv Chaudhuri
Keyword(s):  
Theorem Proving ◽  
Intuitionistic Logic ◽  
Type Theory ◽  
Linear Logic ◽  
Interactive Theorem Proving ◽  
Order Logic ◽  
First Order Logic ◽  
Direct Manipulation ◽  
First Order

AbstractSubformula linking is an interactive theorem proving technique that was initially proposed for (classical) linear logic. It is based on truth and context preserving rewrites of a conjecture that are triggered by a user indicating links between subformulas, which can be done by direct manipulation, without the need of tactics or proof languages. The system guarantees that a true conjecture can always be rewritten to a known, usually trivial, theorem. In this work, we extend subformula linking to intuitionistic first-order logic with simply typed lambda-terms as the term language of this logic. We then use a well known embedding of intuitionistic type theory into this logic to demonstrate one way to extend linking to type theory.

scholarly journals The Mystery of the Fifth Logical Notion (Alice in the Wonderful Land of Logical Notions)

Studia Humana ◽  
2020 ◽  
Vol 9 (3-4) ◽  
pp. 19-36
Author(s):  
Jean-Yves Beziau
Keyword(s):  
Formal Language ◽  
Order Logic ◽  
First Order Logic ◽  
Main Stream ◽  
Square Of Opposition ◽  
First Order ◽  
Alfred Tarski ◽  
The Third ◽  
Logical Notion ◽  
The Square Of Opposition

AbstractWe discuss a theory presented in a posthumous paper by Alfred Tarski entitled “What are logical notions?”. Although the theory of these logical notions is something outside of the main stream of logic, not presented in logic textbooks, it is a very interesting theory and can easily be understood by anybody, especially studying the simplest case of the four basic logical notions. This is what we are doing here, as well as introducing a challenging fifth logical notion. We first recall the context and origin of what are here called Tarski-Lindenbaum logical notions. In the second part, we present these notions in the simple case of a binary relation. In the third part, we examine in which sense these are considered as logical notions contrasting them with an example of a nonlogical relation. In the fourth part, we discuss the formulations of the four logical notions in natural language and in first-order logic without equality, emphasizing the fact that two of the four logical notions cannot be expressed in this formal language. In the fifth part, we discuss the relations between these notions using the theory of the square of opposition. In the sixth part, we introduce the notion of variety corresponding to all non-logical notions and we argue that it can be considered as a logical notion because it is invariant, always referring to the same class of structures. In the seventh part, we present an enigma: is variety formalizable in first-order logic without equality? There follow recollections concerning Jan Woleński. This paper is dedicated to his 80th birthday. We end with the bibliography, giving some precise references for those wanting to know more about the topic.

scholarly journals The Complexity of Circumscription in DLs

2009 ◽  
Vol 35 ◽  
pp. 717-773 ◽  
Author(s):  
P. A. Bonatti ◽  
C. Lutz ◽  
F. Wolter
Keyword(s):  
Description Logics ◽  
Default Logic ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Alternative Approach ◽  
Default Rules ◽  
Logic Description ◽  
Interesting Alternative ◽  
Natural Way

As fragments of first-order logic, Description logics (DLs) do not provide nonmonotonic features such as defeasible inheritance and default rules. Since many applications would benefit from the availability of such features, several families of nonmonotonic DLs have been developed that are mostly based on default logic and autoepistemic logic. In this paper, we consider circumscription as an interesting alternative approach to nonmonotonic DLs that, in particular, supports defeasible inheritance in a natural way. We study DLs extended with circumscription under different language restrictions and under different constraints on the sets of minimized, fixed, and varying predicates, and pinpoint the exact computational complexity of reasoning for DLs ranging from ALC to ALCIO and ALCQO. When the minimized and fixed predicates include only concept names but no role names, then reasoning is complete for NExpTime^NP. It becomes complete for NP^NExpTime when the number of minimized and fixed predicates is bounded by a constant. If roles can be minimized or fixed, then complexity ranges from NExpTime^NP to undecidability.

scholarly journals Possibility Semantics for Intuitionistic Logic

2004 ◽  
Vol 2 ◽  
Author(s):  
M. J. Cresswell
Keyword(s):  
Intuitionistic Logic ◽  
Possible Worlds ◽  
Predicate Logic ◽  
Order Logic ◽  
Semantic Interpretation ◽  
First Order Logic ◽  
First Order ◽  
Partial Indices ◽  
Closure Conditions ◽  
First Order Predicate Logic

The paper investigates interpretations of propositional and first-order logic in which validity is defined in terms of partial indices; sometimes called possibilities but here understood as non-empty subsets of a set W of possible worlds. Truth at a set of worlds is understood to be truth at every world in the set. If all subsets of W are permitted the logic so determined is classical first-order predicate logic. Restricting allowable subsets and then imposing certain closure conditions provides a modelling for intuitionistic predicate logic. The same semantic interpretation rules are used in both logics for all the operators.

An intuitionistic logic for preference relations

2019 ◽  
Vol 27 (4) ◽  
pp. 434-450 ◽  
Author(s):  
Paolo Maffezioli ◽  
Alberto Naibo
Keyword(s):  
Intuitionistic Logic ◽  
Preference Relation ◽  
Order Logic ◽  
First Order Logic ◽  
Strict Preference ◽  
Preference Relations ◽  
First Order ◽  
Weak Preference ◽  
The Way

AbstractWe investigate in intuitionistic first-order logic various principles of preference relations alternative to the standard ones based on the transitivity and completeness of weak preference. In particular, we suggest two ways in which completeness can be formulated while remaining faithful to the spirit of constructive reasoning, and we prove that the cotransitivity of the strict preference relation is a valid intuitionistic alternative to the transitivity of weak preference. Along the way, we also show that the acyclicity axiom is not finitely axiomatizable in first-order logic.

scholarly journals Maximality of bi-intuitionistic propositional logic

2021 ◽  
Author(s):  
Grigory Olkhovikov ◽  
Guillermo Badia
Keyword(s):  
Intuitionistic Logic ◽  
Propositional Logic ◽  
Expressive Power ◽  
Formal Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Intuitionistic Propositional Logic ◽  
Abstract Logic ◽  
First Order ◽  
Work Done

Abstract In the style of Lindström’s theorem for classical first-order logic, this article characterizes propositional bi-intuitionistic logic as the maximal (with respect to expressive power) abstract logic satisfying a certain form of compactness, the Tarski union property and preservation under bi-asimulations. Since bi-intuitionistic logic introduces new complexities in the intuitionistic setting by adding the analogue of a backwards looking modality, the present paper constitutes a non-trivial modification of the previous work done by the authors for intuitionistic logic (Badia and Olkhovikov, 2020, Notre Dame Journal of Formal Logic, 61, 11–30).

scholarly journals Dialogues for proof search

10.29007/5t86 ◽  
2018 ◽  
Author(s):  
Jesse Alama
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Order Logic ◽  
Theorem Prover ◽  
First Order Logic ◽  
Dialogue Games ◽  
First Order ◽  
Proof Search ◽  
Automated Theorem Prover

Dialogue games are a two-player semantics for a variety of logics, including intuitionistic and classical logic. Dialogues can be viewed as a kind of analytic calculus not unlike tableaux. Can dialogue games be an effective foundation for proof search in intuitionistic logic (both first-order and propositional)? We announce Kuno, an automated theorem prover for intuitionistic first-order logic based on dialogue games.

First-Order Logic Reasoning Support for the Semantic Web

2009 ◽  
Vol 19 (12) ◽  
pp. 3091-3099 ◽  
Author(s):  
Gui-Hong XU ◽  
Jian ZHANG
Keyword(s):  
Semantic Web ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Logic Reasoning

Boolean-valued structures

2018 ◽  
Author(s):  
Tim Button ◽  
Sean Walsh
Keyword(s):  
Model Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Inference Rules ◽  
Mathematical Concepts ◽  
Semantic Framework ◽  
First Order ◽  
Standard Models ◽  
Boolean Valued Model ◽  
Semantic Values

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.

Sign in / Sign up

Export Citation Format

Share Document