The topic of forgetting, which loosely speaking means losing, removing, or even hiding some variables, propositions, or formulas, has been extensively studied in the field of knowledge representation and reasoning for many major formalisms. In this article, we convey this topic to the highly active field of abstract argumentation. We provide an in-depth analysis of desirable syntactical and/or semantical properties of possible forgetting operators. In doing so, we included well-known logic programming conditions, such as strong persistence or strong invariance. Further, we argue that although abstract argumentation and logic programming are closely related, it is not possible to reduce forgetting in abstract argumentation to forgetting in logic programming in a straightforward manner. The analysis of desiderata, adapted to the specifics of abstract argumentation, includes implications among them, individual and collective satisfiability, and identifying inherent limits for a set of prominent semantics. Finally, we conduct a case study on stable semantics incorporating concrete forgetting operators.

We formalize the notions of “permitted and obligatory announcements” in the context of information security, such as privacy policy compliance. In a sender-receiver setting, we define the sender’s permitted and obligatory announcements in terms of the receiver’s ideal epistemic states (i.e., the epistemic states that comply with the given security policies). We propose two logics, LPOA and DLPOA, to reason about permitted and obligatory announcements in static and dynamic contexts, respectively. These two logics are completely axiomatized, and we also study generalizations in which the receiver’s knowledge is characterized by non-S5 logics. Our paper makes two main contributions to the formalization of permitted and obligatory announcements: First, we clarify the interplay between the sender’s permitted and obligatory announcements and the receiver’s knowledge. Second, we distinguish between weakly and strongly permitted announcements.

Abstract In this paper, we provide a formal framework for modeling the burden of persuasion in legal reasoning. The framework is based on abstract argumentation, a frequently studied method of non-monotonic reasoning, and can be applied to different argumentation semantics; it supports burdens of persuasion with arbitrary many levels, and allows for the placement of a burden of persuasion on any subset of an argumentation framework’s arguments. Our framework can be considered an extension of related works that raise questions on how burdens of persuasion should be handled in some conflict scenarios that can be modeled with abstract argumentation. An open source software implementation of the introduced formal notions is available as an extension of an argumentation reasoning library. A theoretical analysis shows that our approach can be generalized to a novel method for the preference-based selection of extensions from argumentation frameworks.

Autonomous agents are supposed to be able to finish tasks or achieve goals that are assigned by their users through performing a sequence of actions. Since there might exist multiple plans that an agent can follow and each plan might promote or demote different values along each action, the agent should be able to resolve the conflicts between them and evaluate which plan he should follow. In this paper, we develop a logic-based framework that combines modal logic and argumentation for value-based practical reasoning with plans. Modal logic is used as a technique to represent and verify whether a plan with its local properties of value promotion or demotion can be followed to achieve an agent’s goal. We then propose an argumentation-based approach that allows an agent to reason about his plans in the form of supporting or objecting to a plan using the verification results.

In the symbolic artificial intelligence community, abstract argumentation with its semantics, i.e. approaches for defining sets of valid conclusions (extensions) that can be derived from argumentation graphs, is considered a promising method for non-monotonic reasoning. However, from a sequential perspective, abstract argumentation-based decision-making processes typically do not guarantee an alignment with common formal notions to assess consistency; in particular, abstract argumentation can, in itself, not enforce the satisfaction of relational principles such as reference independence (based on a key principle of microeconomic theory) and cautious monotony. In this paper, we address this issue by introducing different approaches to ensuring reference independence and cautious monotony in sequential argumentation: a reductionist, an expansionist, and an extension-selecting approach. The first two approaches are generically applicable, but may require comprehensive changes to the corresponding argumentation framework. In contrast, the latter approach guarantees that an extension of the corresponding argumentation framework can be selected to satisfy the relational principle by requiring that the used argumentation semantics is weakly reference independent or weakly cautiously monotonous, respectively, and also satisfies some additional straightforward principles. To highlight the relevance of the approach, we illustrate how the extension-selecting approach to reference independent argumentation can be applied to model (boundedly) rational economic decision-making.

The notion of forgetting, as considered in the famous paper by Lin and Reiter in 1994 has been extensively studied in classical logic and more recently, in non-monotonic formalisms like logic programming. In this paper, we convey the idea of forgetting to another major AI formalism, namely Dung-style argumentation frameworks. Our approach is axiomatic-driven and not limited to any specific semantics: we propose semantical and syntactical desiderata encoding different criteria for what forgetting an argument might mean; analyze how these criteria relate to each other; and check whether the criteria can be satisfied in general. The analysis is done for a number of widely used argumentation semantics. Our investigation shows that almost all desiderata are individually satisfiable. However, combinations of semantical and/or syntactical conditions reveal a much more interesting landscape. For instance, we found that the ad hoc approach to forgetting an argument, i.e., by the syntactical removal of the argument and all of its associated attacks, is too restrictive and only compatible with the two weakest semantical desiderata. Amongst the several interesting combinations identified, we showed that one satisfies a notion of minimal change and presented an algorithm that given an AF F and argument x, constructs a suitable AF G satisfying the conditions in the combination.

This article presents a unique method in text and data mining for finding the era, i.e., mining temporal data, in which an anonymous author was living. Finding this era can assist in the examination of a fake document or extracting the time period in which a writer lived. The study and the experiments concern Hebrew, and in some parts, Aramaic and Yiddish rabbinic texts. The rabbinic texts are undated and contain no bibliographic sections, posing an interesting challenge. This work proposes algorithms using key phrases and key words that allow the temporal organization of citations together with linguistic patterns. Based on these key phrases, key words, and the references, we established several types of “Iron-clad,” Heuristic and Greedy rules for estimating the years of birth and death of a writer in an interesting classification task. Experiments were conducted on corpora, including documents authored by 12, 24, and 36 rabbinic writers and demonstrated promising results.

This volume contains selected papers from the workshop ‘Concepts and Meaning’ held on 2–5 May 2012 at the Vienna University of Technology in honour of the 60th birthday of Alexander Leitsch. Alexander Leitsch made substantial contributions to a variety of different research areas including automated deduction, computability theory, proof theory and formal mathematics. The broad scope of his research interests is reflected in the contents of this special issue that features the following papers (in alphabetic order): ... A common thread that runs through Alexander Leitsch' scientific work is his mastery of syntactic precision rooted in the conviction that the syntactic form not only captures but even determines the semantic meaning of concepts, hence also the title of this special issue. In addition to his scientific activities he is also an inspiring colleague and a dedicated and enthusiastic teacher as witnessed by generations of his students who are now successful in academia as well as in industry, some of which are represented in this volume.

Given a network (S,R) , with R ⊂ S2, we view the nodes of S as containing information and view xRy as x transmitting information to y. We argue that such networks provide a more general account of attack and defense as well as being able to simulate the traditional Dung approach.

The traditional 3-valued semantics of an argumentation frameworkidentifies arguments that are “in”, “out” and “undecided”. Yet, it has long been recognised by the community that some elements can be at different degrees in each of these categories [1,2,3]. For example, Dung's semantics can only classify some elements as “out”, but cannot reflect how much “out” they really are or if elements are “in” are they as much “in” as elements which are not attacked at all? In this paper we shall use a numerical approach to give a measure of “in”, “out” and “undecided” to the nodes of a network. We shall devise equations which allow for solutions that reflect these distinctions.

Pietro Baroni, Dov M. Gabbay, Massimiliano Giacomin; Introduction to the special issue on Loops in Argumentation, Journal of Logic and Computation, Volume

Traditional abstract argumentation networks have been studied in two directions Investigate their semantics in detail. This has lead to the study of extensions, dealing with loops, connections with classical logic, the notions joint and disjunctive attacks, and especially what concerns us here, the Equational approach and the ASPIC instantiation approach. Generalize the notion of argumentation to bipolar argumentation and to the addition of the notion of support.

This article is about busting loops in abstract argumentation networks. We propose several approaches to how to deal with networks which have loops (such as even or odd cycles) and get new extensions which are ‘in’, ‘out’ extensions, with no undecided elements.

We introduce a reactive variant of SDL (standard deontic logic): SDLR1 (reactive standard deontic logic). Given a Kripkean view on the semantics of SDL in terms of directed graphs where arrows → represent the accessibility relation between worlds, reactive models add two elements: arrows → are labelled as ‘active’ or ‘inactive’, and double arrows ↠ connect arrows, e.g. (x1 → x2) ↠ (x3 → x4). The idea is that passing through x1 → x2 activates a switch represented by ↠ that inverts the label of x3 → x4 and hence activates respectively deactivates this arrow. This allows to introduce two modalities: □ is the usual KD-modality of SDL and operates on the Kripkean graph where all labels and double arrows are ignored, while Ø takes them into account. We demonstrate that RSDL1 allows for an intuitive interpretation of ‘ought’. The logic can handle contrary-to-duty cases such as several instantiations of the Chisholm set in a paradox-free way by means of using double arrows and annotations to block and give access to ideal worlds.

Given an argumentation network with initial values to the arguments, we look for a numerical algorithm yielding extensions compatible with such initial values. We offer an iteration schema that takes the initial values of the nodes and follows the attack relation producing a sequence of intermediate values that eventually becomes stable leading to an extension in the limit. The schema can be used in abstract as well as in abstract dialectical frameworks (ADFs).

We develop a model of abduction in abstract argumentation, where changes to an argumentation framework act as hypotheses to explain the support of an observation. We present dialogical proof theories for the main decision problems (i.e., finding hypotheses that explain skeptical/credulous support) and we show that our model can be instantiated on the basis of abductive logic programs.

In this article we show how to model a range of notions in the context of delegation and revocation applied to security scenarios. We demonstrate how a range of delegation–revocation models and policies may be represented in pictorial form and formally represented in terms of reactive Kripke models and a first-order policy specification language. We translate first-order representations of our reactive Kripke models into an equivalent Answer Set Programming form that enables users to apply flexibly well-defined definitions of predicates to represent their requirements in terms of delegation–revocation policy specification.

This article concerns the merging of argumentation systems. We propose an equational approach to this problem by considering an augmented network containing the arguments and attacks of all systems to be merged and then associating a numerical weight to each of the components of the augmented network. The weights are calculated based on how the components are perceived by the agents associated with the systems being merged. The resulting weighted network is then used to define a system of equations, one for each argument, a solution of which corresponds to the overall level of acceptance of the arguments within the community.

We introduce a family of new equational semantics for argumentation networks which can handle odd and even loops in a uniform manner. We offer equational semantics which is equivalent to CF2 semantics, and a better version which gives the same results as traditional Dung semantics for even loops but can still handle odd loops.

In this paper, we characterize a Wigmore Diagram as an information-flow network. A fuzzy approach to weighing the strength of the evidence is defined and compared to the well-known probabilistic approach. This enables an intelligent computer evaluation of the evidence, in order to support a practicing lawyer.

In this paper, we consider two drawbacks of Cayrol and Lagasque-Schiex's meta-argumentation theory to model bipolar argumentation frameworks. We consider first the “lost of admissibility” in Dung's sense and second, the definition of notions of attack in the context of a support relation. We show how to prevent these drawbacks by introducing support meta-arguments. Like the model of Cayrol and Lagasque-Schiex, our formalization confirms the use of meta-argumentation to reuse Dung's properties. We do not take a stance towards the usefulness of a support relation among arguments, though we show that if one would like to introduce them, it can be done without extending Dung's theory. Finally, we show how to use meta-argumentation to instantiate an argumentation framework to represent defeasible support. In this model of support, the support relation itself can be attacked.

We introduce and study higher-order coalition logic, a multi modal monadic second-order logic with operators [{x}ψ]φ expressing that the coalition of all agents satisfying ψ(x) can achieve a state in which φ holds. We use neighborhood semantics to model extensive games of perfect information with simultaneous actions and we provide a framework reasoning about agents in the same way as it is reasoning about their abilities. We illustrate higher-order coalition logic to represent and reason about coalition formation and cooperation, we show a more general and expressive way to quantify over coalitions than quantified coalition logic, we give an axiomatization and prove completeness.

Journal Article Connections between Belief Revision, Belief Merging and Social Choice Get access Dov Gabbay, Dov Gabbay Department of Computer Science, King's College, London WC2R 2LS, UK Search for other works by this author on: Oxford Academic Google Scholar Odinaldo Rodrigues, Odinaldo Rodrigues Department of Computer Science, King's College, London WC2R 2LS, UK Search for other works by this author on: Oxford Academic Google Scholar Gabriella Pigozzi Gabriella Pigozzi Computer Science and Communication (CSC) University of Luxembourg 6 rue R. Coudenhove Kalergi L-1359 Luxembourg Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 19, Issue 3, June 2009, Pages 445–446, https://doi.org/10.1093/logcom/exn013 Published: 21 May 2009

We present a revision-based logical framework for modelling hierarchical assemblies of evolvable component systems. An evolvable component is a tight coupling of a pair of components, consisting of a supervisor and a supervisee, with the supervisor able to both monitor and evolve its supervisee. An evolvable component pair is itself a component so may have its own supervisor, or may be encapsulated as part of a larger component. Components are modelled as logical theories containing actions which describe state revisions. Supervisor components are modelled as theories which are logically at a meta-level to their supervisee. Revision actions at the meta-level describe theory changes in the supervisee at the object-level. These correspond to various evolutionary changes in the component. We present this framework and show how it enables us to describe the architecture and logical structure of evolvable systems.

We present a new connectionist model for constructive, intuitionistic modal reasoning. We use ensembles of neural networks to represent in- tuitionistic modal theories, and show that for each intuitionistic modal program there exists a corresponding neural network ensemble that com- putes the program. This provides a massively parallel model for intu- itionistic modal reasoning, and sets the scene for integrated reasoning, knowledge representation, and learning of intuitionistic theories in neural networks, since the networks in the ensemble can be trained by examples using standard neural learning algorithms.

While neural networks have been successfully used in a number of machine learning applications, logical languages have been the standard for the representation of argumentative reasoning. In this paper, we establish a relationship between neural networks and argumentation networks, combining reasoning and learning in the same argumentation framework. We do so by presenting a new neural argumentation algorithm, responsible for translating argumentation networks into standard neural networks. We then show a correspondence between the two networks. The algorithm works not only for acyclic argumentation networks, but also for circular networks, and it enables the accrual of arguments through learning as well as the parallel computation of arguments

We present two embeddings of Łukasiewicz logicŁinto Meyer and Slaney's Abelian logicA, the logic of lattice-ordered Abelian groups. We give new analytic proof systems forAand use the embeddings to derive corresponding systems forŁ. These include hypersequent calculi, terminating hypersequent calculi, co-NP labeled sequent calculi, and unlabeled sequent calculi.

1London

1Department of Computer Science, King's College London, Strand, London WC2R 2LS. e-mail: [email protected], 2Department of Philosophy, University of Konstanz, Germany. e-mail: [email protected], 3The Abductive Systems Group, University of British Columbia, Vancouver, BC, Canada V6T 1Z1, and Department of Computer Science, King's College, London, Strand, London WC2R 2LS e-mail: [email protected] Received November 2001.

Journal Article Editorial Get access Dov Gabbay Dov Gabbay Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 11, Issue 1, 1 February 2001, Page 1, https://doi.org/10.1093/logcom/11.1.1 Published: 01 February 2001

Journal Article What's on my mind... Get access DM Gabbay DM Gabbay King's College, London, UK Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 9, Issue 1, February 1999, Pages 3–6, https://doi.org/10.1093/logcom/9.1.3 Published: 01 February 1999

Agents situated in proactive environments are acting autonomously while the environment is evolving alongside, whether or not the agents carry out any particular actions. A formal framework for simulating and reasoning about this generalized kind of dynamic system is proposed. The capabilities of the agents are modelled by a set of conditional rules in a temporal-logical format. The environment itself is modelled by an independent transition relation of the state space. The temporal language is given a declarative semantics on the basis of an abstract, general model structure for formal specifications of proactive environments. Key words: Agent programming, logic of proactive environments, executable temporal logic.

Journal Article Editorial Get access D. M. GABBAY D. M. GABBAY London Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 8, Issue 1, February 1998, Page 3, https://doi.org/10.1093/logcom/8.1.3 Published: 01 February 1998

Abstract This is Part 1 of a paper on fibred semantics and combination of logics. It aims to present a methodology for combining arbitrary logical systemsLi,i∈I, to form a new systemLI. The methodology ‘fibres’ the semantics iofLiinto a semantics forLI, and ‘weaves’ the proof theory (axiomatics) ofLiinto a proof system ofLI. There are various ways of doing this, we distinguish by different names such as ‘fibring’, ‘dovetailing’ etc, yielding different systems, denoted by etc. Once the logics are ‘weaved’, further ‘interaction’ axioms can be geometrically motivated and added, and then systematically studied. The methodology is general and is applied to modal and intuitionistic logics as well as to general algebraic logics. We obtain general results on bulk, in the sense that we develop standard combining techniques and refinements which can be applied to any family of initial logics to obtain further combined logics. The main results of this paper is a construction for combining arbitrary, (possibly not normal) modal or intermediate logics, each complete for a class of (not necessarily frame) Kripke models. We show transfer of recursive axiomatisability, decidability and finite model property. Some results on combining logics (normal modal extensions ofK) have recently been introduced by Kracht and Wolter, Goranko and Passy and by Fine and Schurz as well as a multitude of special combined systems existing in the literature of the past 20–30 years. We hope our methodology will help organise the field systematically.

We present a general proof theoretical methodology for default systems. Given a default theory W, D, the default rules D are simply understood as restrictions on the tableaux construction of the logic. Different default approaches approch (such as Reiter, Brewka or Lukaszewicz), the allowable default extensions can be obtained from the default tableau construction. The advantage of our approach, besides being simple and neat, is in its generality: it allows for the development of a default theory for any logic with a tableau formulation, such as intuitionistic logic, linear logic or modal logic.

Abstract In this paper a methodology for the use of temporal logic as an executable imperative language is introduced. The approach, which provides a concrete framework, calledMetateM, for executing temporal formulae, is motivated and illustrated through examples. In addition, this introduction provides references to further, more detailed, work relating to theMetateMapproach to executable logics.

The development of most large and complex systems necessarily involves many people-each with their own perspectives on the system defined by their knowledge, responsibilities, and commitments. To address this we have advocated distributed development of specifications from multiple perspectives. However, this leads to problems of identifying and handling inconsistencies between such perspectives. Maintaining absolute consistency is not always possible. Often this is not even desirable since this can unnecessarily constrain the development process, and can lead to the loss of important information. Indeed since the real-world forces us to work with inconsistencies, we should formalize some of the usually informal or extra-logical ways of responding to them. This is not necessarily done by eradicating inconsistencies but rather by supplying logical rules specifying how we should act on them. To achieve this, we combine two lines of existing research: the ViewPoints framework for perspective development, interaction and organization, and a logic-based approach to inconsistency handling. This paper presents our technique for inconsistency handling in the ViewPoints framework by using simple examples.>

The interest in fragments of predicate logics is motivated by the well-known fact that full classical predicate calculus is undecidable (cf. Church [1936]). So it is desirable to find decidable fragments which are in some sense “maximal”, i.e., which become undecidable if they are “slightly” extended. Or, alternatively, we can look for “minimal” undecidable fragments and try to identify the vague boundary between decidability and undecidability. A great deal of work in this area concerning mainly classical logic has been done since the thirties. We will not give a complete review of decidability and undecidability results in classical logic, referring the reader to existing monographs (cf. Suranyi [1959], Lewis [1979], and Dreben, Goldfarb [1979]). A short summary can also be found in the well-known book Church [1956]. Let us recall only several facts. Herein we will consider only logics without functional symbols, constants, and equality. (C1) The fragment of the classical logic with only monadic predicate letters is decidable (cf. Behmann [1922]). (C2) The fragment of the classical logic with a single binary predicate letter is undecidable. (This is a consequence of Gödel [1933].) (C3) The fragment of the classical logic with a single individual variable is decidable; in fact it is equivalent to Lewis S5 (cf. Wajsberg [1933]). (C4) The fragment of the classical logic with two individual variables is decidable (Segerberg [1973] contains a proof using modal logic; Scott [1962] and Mortimer [1975] give traditional proofs.) (C5) The fragment of the classical logic with three individual variables and binary predicate letters is undecidable (cf. Surańyi [1943]). In fact this paper considers formulas of the following type φ,ψ being quantifier-free and the set of binary predicate letters which can appear in φ or ψ being fixed and finite.

Editorial Get access DOV GABBAY DOV GABBAY Imperical CollegeLondon Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 3, Issue 1, February 1993, Pages 1–2, https://doi.org/10.1093/logcom/3.1.1 Published: 01 February 1993

The so-called Curry-Howard interpretation (Curry [1934], Curry and Feys [1958], Howard [1969], Tait [1965]) is known to provide a rather neat term-functional account of intuitionistic implication. Could one refine the interpretation to obtain an almost as good account of other neighbouring implications, including the so-called ‘resource’ implications (e.g. linear, relevant, etc.)? We answer this question positively by demonstrating that just by working with side conditions on the rule of assertability conditions for the connective representing implication (‘→’) one can characterise those ‘resource’ logics. The idea stems from the realisation that whereas the elimination rule for conditionals (of which implication is a particular case) remains virtually unchanged no matter what kind of conditional one has (i.e. linear, relevant, intuitionistic, classical, etc., all have modus ponens), the corresponding introduction rule carries an element of vagueness which can be explored in the characterisation of several sorts of conditionals. The rule of →-introduction is classified as an ‘improper’ inference rule, to use a terminology from Prawitz [1965]. Now, the so-called improper rules leave room for manoeuvre as to how a particular logic can be obtained just by imposing conditions on the discharge of assumptions that would correspond to the particular logical discipline one is adopting (linear, relevant, ticket entailment, intuitionistic, classical, etc.). The side conditions can be ‘naturally’ imposed, given that a degree of ‘vagueness’ is introduced by the presentation of those improper inference rules, such as the rule of →-introduction: which says: starting from assumption ‘A’, and arriving at ‘B’ via an unspecified number of steps, one can discharge the assumption and conclude that ‘A’ implies ‘B’.

Editorial Get access D. M. GABBAY D. M. GABBAY Editor-in-Chief Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 1, Issue 1, July 1990, Pages 1–4, https://doi.org/10.1093/logcom/1.1.1 Published: 01 July 1990

A Hilbert style axiomatization of the temporal logic with connectives Until and Since for the real numbers is presented. We prove independence of the axioms, and completeness for this semantics with respect to single formulas.

The use of the temporal logic formalism for program reasoning is reviewed. Several aspects of responsiveness and fairness are analyzed, leading to the need for an additional temporal operator: the 'until' operator -U. Some general questions involving the 'until' operator are then discussed. It is shown that with the addition of this operator the temporal language becomes expressively complete. Then, two deductive systems DX and DUX are proved to be complete for the languages without and with the new operator respectively.

This is a continuation of two previous papers by the same title [2] and examines mainly the interpolation property for the logic CD with constant domains, i.e., the extension of the intuitionistic predicate logic with the schema It is known [3], [4] that this logic is complete for the class of all Kripke structures with constant domains. Theorem 47. The strong Robinson consistency theorem is not true for CD. Proof. Consider the following Kripke structure with constant domains. The set S of possible worlds is ω0, the set of positive integers. R is the natural ordering ≤. Let ω0 0 = , Bn, is a sequence of pairwise disjoint infinite sets. Let L0 be a language with the unary predicates P, P1 and consider the following extensions for P,P1 at the world m. (a) P is true on ⋃i≤2nBi, and P1 is true on ⋃i≤2n+1Bi for m = 2n. (b) P is true on ⋃i≤2nBi, and P1 for ⋃i≤2n+1Bi for m = 2n. Let (Δ,Θ) be the complete theory of this structure. Consider another unary predicate Q. Let L be the language with P, Q and let M be the language with P1, Q.

We use the notation of Kripke's paper [1]. Let M = (G, K, R) be a tree structure and D a domain and η a Beth model on M. The truth conditions of the Beth semantics for ∨ and ∃ are (see [1]): (a) η (A ∨ B, H) = T iff for some B ⊆ K, B bars H and for each H′ ∈ B, either η(A, H′) = T or η(B, H′) = T. (b) η(∃xA(x), H) = T iff for some B ⊆ K, B bars H and for each H′ ∈ B there exists an a ∈ D such that η(A (a), H′) = T. Suppose we change the truth definition η to η* by replacing condition (b) by the condition (b*) (well known from the Kripke interpretation): Call this type of interpretation the new version of Beth semantics. We prove Theorem 1. Intuitionistic predicate logic is complete for the new version of the Beth semantics. Since Beth structures are of constant domains, and in the new version of Beth semantics the truth conditions for ∧, →, ∃, ∀, ¬ are the same as for the Kripke interpretation, we get: Corollary 2. The fragment without disjunction of the logic CD of constant domains (i.e. with the additional schema ∀x(A ∨ B(x))→ A ∨ ∀xB(x), x not free in A) equals the fragment without disjunction of intuitionistice logic.

Validity in recursive structures was investigated by several authors. Kreisel [10] has shown that there exists a consistent sentence of classical predicate calculus (CPC) that does not possess a recursive model. The sentence is a conjunction of the axioms of a variant of Bernays set theory, including the axiom of infinity. The language contains additional constants besides ϵ. Later Kreisel [2] and Mostowski [3] presented a sentence (not possessing recursive models) which was a conjunction of axioms of a variant of Bernays set theory without the axiom of infinity but still with additional constants besides ϵ. Later Mostowski [4] improved the result by giving a sentence which can be demonstrated in Heyting arithmetic to be consistent and to have no recursive models. Rabin [6] obtained a simple proof that some sentence of set theory with the single nonlogical constant ϵ does not have any recursively enumerable models. More generally, Mostowski [5] has shown that the set of all sentences valid in all RE models is not arithmetical and Vaught [1] improved this result by showing that it holds for a language of one binary relation. In fact, Vaught gives· a way of translating n-place relations to 2-place ones that preserves the RE characteristic of the model. For further results pertaining to recursive models see Vaught [1].

The intuitionistic propositional logic I has the following (disjunction) property . We are interested in extensions of the intuitionistic logic which are both decidable and have the disjunction property. Systems with the disjunction property are known, for example the Kreisel-Putnam system [1] which is I + (∼ϕ → (ψ ∨ α))→ ((∼ϕ→ψ) ∨ (∼ϕ→α)) and Scott's system I + ((∼ ∼ϕ→ϕ)→(ϕ ∨ ∼ϕ))→ (∼∼ϕ ∨ ∼ϕ). It was shown in [3c] that the first system has the finite-model property. In this note we shall construct a sequence of intermediate logics Dn with the following properties: These systems are presented both semantically and syntactically, using the remarkable correspondence between properties of partially ordered sets and axiom schemata of intuitionistic logic. This correspondence, apart from being interesting in itself (for giving geometric meaning to intuitionistic axioms), is also useful in giving independence proofs and obtaining proof theoretic results for intuitionistic systems (see for example, C. Smorynski, Thesis, University of Illinois, 1972, for independence and proof theoretic results in Heyting arithmetic).

Let T be a set of axioms for a classical theory TC (e.g. abelian groups, linear order, unary function, algebraically closed fields, etc.). Suppose we regard T as a set of axioms for an intuitionistic theory TH (more precisely, we regard T as axioms in Heyting's predicate calculus HPC). Question. Is TH decidable (or, more generally, if X is any intermediate logic, is TX decidable)? In [1] we gave sufficient conditions for the undecidability of TH. These conditions depend on the formulas of T (different axiomatization of the same TC may give rise to different TH) and on the classical model theoretic properties of TC (the method did not work for model complete theories, e.g. those of the title of the paper). For details see [1]. In [2] we gave some decidability results for some theories: The problem of the decidability of theories TH for a classically model complete TC remained open. An undecidability result in this direction, for dense linear order was obtained by Smorynski [4]. The cases of algebraically closed fields and real closed fields and divisible abelian groups are treated in this paper. Other various decidability results of the intuitionistic theories were obtained by several authors, see [1], [2], [4] for details. One more remark before we start. There are several possible formulations for an intuitionistic theory of, e.g. fields, that correspond to several possible axiomatizations of the classical theory. Other formulations may be given in terms of the apartness relation, such as the one for fields given by Heyting [5]. The formulations that we consider here are of interest as these systems occur in intuitionistic mathematics. We hope that the present methods could be extended to the (more interesting) case of Heyting's systems [5].

We investigate extensions of Heyting's predicate calculus (HPC). We relate geometric properties of the trees of Kripke models (see [2]) with schemas of HPC and thus obtain completeness theorems for several intermediate logics defined by schemas. Our main results are: (a) ∼(∀x ∼ ∼ϕ(x) Λ ∼∀xϕ(x)) is characterized by all Kripke models with trees T with the property that every point is below an endpoint. (From this we shall deduce Glivenko type theorems for this extension.) (b) The fragment of HPC without ∨ and ∃ is complete for all Kripke models with constant domains. We assume familiarity with Kripke [2]. Our notation is different from his since we want to stress properties of the trees. A Kripke model will be denoted by (Aα, ≤ 0), α ∈ T where (T, ≤, 0) is the tree with the least member 0 ∈ T and Aα, α ∈ T, is the model standing at the node α. The truth value at α of a formula ϕ(a1 … an) under the indicated assignment at α is denoted by [ϕ(a1 … an)]α. A Kripke model is said to be of constant domains if all the models Aα, α ∈ T, have the same domain.

Let Δ be a set of axioms of a theory Tc(Δ) of classical predicate calculus (CPC); Δ may also be considered as a set of axioms of a theory TH(Δ) of Heyting's predicate calculus (HPC). Our aim is to investigate the decision problem of TH(Δ) in HPC for various known theories Δ of CPC. Theorem I(a) of §1 states that if Δ is a finitely axiomatizable and undecidable theory of CPC then TH(Δ) is undecidable in HPC. Furthermore, the relations between theorems of HPC are more complicated and so two CPC-equivalent axiomatizations of the same theory may give rise to two different HPC theories, in fact, one decidable and the other not. Semantically, the Kripke models (for which HPC is complete) are partially ordered families of classical models. Thus a formula expresses a property of a family of classical models (i.e. of a Kripke model). A theory Θ expresses a set of such properties. It may happen that a class of Kripke models defined by a set of formulas Θ is also definable in CPC (in a possibly richer language) by a CPC-theory Θ′! This establishes a connection between the decision problem of Θ in HPC and that of Θ′ in CPC. In particular if Θ′ is undecidable, so is Θ. Theorems II and III of §1 give sufficient conditions on Θ to be such that the corresponding Θ′ is undecidable. Θ′ is shown undecidable by interpreting the CPC theory of a reflexive and symmetric relation in Θ′.

Suppose T is a first order intuitionistic theory (more precisely, a theory of Heyting's predicate calculus, e.g., abelian groups, one unary function, dense linear order, etc.) presented to us by a set of axioms (denoted also by) T. Question. Is T decidable? One knows that if the classical counterpart of T (i.e., take the same axioms but with the classical predicate calculus as the underlying logic) is not decidable, then T cannot be decidable. The problem remains for theories whose classical counterpart is decidable. In [8], sufficient conditions for undecidability were given, and several intuitionistic theories such as abelian groups and unary functions (both with decidable equality) were shown to be undecidable. In this note we show decidability results (see Theorems 1 and 2 below), and compare these results with the undecidability results previously obtained. The method we use is the reduction-method, described fully in [12] and widely applied in [3], which is applied here roughly as follows: Let T be a given theory of Heyting's predicate calculus. We know that Heyting's predicate calculus is complete for the Kripke-model type of semantics. We choose a class M of Kripke models for which T is complete, i.e., all axioms of T are valid in any model of the class and whenever φ is not a theorem of T, φ is false in some model of M.

The intuitionistic propositional logic I has the following disjunction property This property does not characterize intuitionistic logic. For example Kreisel and Putnam [5] showed that the extension of I with the axiom has the disjunction property. Another known system with this propery is due to Scott [5], and is obtained by adding to I the following axiom: In the present paper we shall prove, using methods originally introduced by Segerberg [10], that the Kreisel-Putnam logic is decidable. In fact we shall show that it has the finite model property, and since it is finitely axiomatizable, it is decidable by [4]. The decidability of Scott's system was proved by J. G. Anderson in his thesis in 1966.