Search

Summary The fragments considered are first-order theories whose (non-logical) constants are among O, ' (successor), P (predecessor), +,., ÷, [×/n] (n = 2, 3, …); whose axioms are the primitive recursive defining equations for the chosen functions and whose sole (non-logical) rule of inference is the rule of induction for open formulae. The main aims are: (1) to find equivalent systems without a rule of induction, i.e., to see what is the algebraic effect of the open rule of induction, (2) to survey the non-standard models, and (3) to use these models to give independence proofs, in particular to see how much weaker the given rule of induction is than the full rule of induction.

In fuzzy predicate logic, assignment of truth values may be partial, i.e. the truth value of a formula in an interpretation may be undefined (due to lack of some infinite suprema or infima in the underlying structure of truth values). A logic is supersound if each provable formula ϕ is true (has truth value 1) in each interpretation in which the truth value of ϕ is defined. It is shown that among the logics given by continuous t -norms, Godel logic is the only one that is supersound; all others are (sound but) not supersound. This supports the view that the usual restriction of semantics to safe interpretations (in which the truth assignments is total) is very natural.

Rational Pavelka logic extends Łukasiewicz infinitely valued logic by adding truth constants r̄ for rationals in [0. 1]. We show that this is a conservative extension. We note that this shows that provability degree can be defined in Łukasiewicz logic. We also give a counterexample to a soundness theorem of Belluce and Chang published in 1963.

Can one extend crisp Peano arithmetic PA by a possibly many-valued predicate Tr(x) saying “xis true” and satisfying the “dequotation schema”for all sentences φ? This problem is investigated in the frame of Łukasiewicz infinitely valued logic.

In this paper, we study the partial deduction of updateable logic programs. Partial deduction is a transformation technique that, given a normal program P and a normal goal G , produces from P a residual program P ′ wrt G . An updateable program is a normal program to which an update can be applied. An update is a sequence of additions of clauses to a program and deletions of clauses from a program. We present algorithms that, given a normal program P , a normal goal G , a residual program P ′ wrt G , and an update t for P , compute the corresponding update t ′ such that t ′( P ′) is a residual program of t ( P ) wrt G . Weprove the correctness of these algorithms. We also describe an application of one of the algorithms to updateable knowledge bases.

Unfold/fold transformations have been used in logic programming for some years to transform programs into more efficient ones. We describe recent work on the extent to which these transformations produce programs which are equivalent to the original one. Various notions of equivalence are considered: same success set; finite failure set; least Herbrand model; completion. This is used to illustrate the rather unsatisfactory relationship between logic programming and logic shown by the wide variety of different declarative semantics proposed for logic programs.

The underlying language of symbols used in logic programming is usually taken to be the one consisting of the symbols occurring in the program, or the program together with the query, but sometimes infinitely many function symbols are included. As far as Prolog or SLDNF-resolution are concerned, it makes no difference since these operate entirely within the former language. But it does make a difference to the Clark completion of a program and to ‘constructive negation’, a recently proposed extension of negation as failure. The difference is transmitted via the equality theory. We consider the effect of the underlying language on the Clark completion, the equality theory, constructive negation and 3-valued semantics.

In this paper we provide a general framework for extracting programs from proofs in the language of first order predicate calculus directly, that is to say, without first going through a transformation into second order propositional calculus or other higher order logic.

Clark shows that a query evaluation procedure for data base deductions using a “negation as failure” inference rule can be regarded as making deductions from the “completed data base” (CDB) obtained by replacing the “if” clauses of the data base by “iff” clauses. We show they can also be regarded as deductions from the “closed world assumption” (CWA) of Reiter. Usually these deduction systems are incomplete and the CDB and CWA differ; one may be consistent and the other not, and when both are separately consistent they may be incompatible. However when the data base is Horn and definite they are compatible and when Clark's query evaluation procedure is complete for ground literals they are essentially equivalent. When the query evaluation procedure is not complete it may lack some basic closure properties. The conditions given by Clark for the completeness of his query evaluation procedure are not quite sufficient, and when made so are rather restrictive.

For the first Gödel incompleteness theorem, the existence in a formal system of arithmetic L of a sentence which is neither provable nor refutable, all that is required of the formula Th(x) of L used to express the notion ‘x is the g.n. (gödel number) of a theorem of L’ is mere numeralwise correctness, i.e. that for a numeral n, Th(n) is provable in L iff n is the g.n. of a theorem of L. It is well known that much more is needed for the second Gödel incompleteness theorem, the unprovability in L of the formula Con =df ¬(∃y, z)(Th(y) ∧ Th(z) ∧ neg(z, y)), which (if neg expresses negation) expresses the consistency of L. Conditions sufficient for this second theorem, more or less as stated by Hilbert-Bernays [1, p. 286] and elegantly formulated by Löb [2] may with a cavalier disregard for the distinction between use and mention be stated thus: The result of the first incompleteness theorem: there is a sentence G such that ⊢G ↔ ¬Th G), together with, if ⊢A then ⊢Th A, if ⊢(A → B) then ⊢(Th A → Th B), ⊢(Th A → Th Th A). On the other hand Feferman [3], Kreisel [4, p. 154] and Jeroslow [9] have given examples of systems and consistency formulae, based on numeralwise correct formulae Th(x), which are provable within the system.

The use of the negation as failure rule in logic programming is often considered to be tantamount to reasoning from Clark's “completed data base” [2]. Continuing the investigations of Clark and Shepherdson [2,7], we show that this is not fully equivalent to negation as failure either using classical logic or the more appropriate intuitionistic logic. We doubt whether there is any simple and useful logical meaning of negation as failure in the general case, and study in detail some special kinds of data base where the relationship of the completed data base to negation as failure is closer, e.g. where the data base is definite Horn or hierarchic.

Cobham has observed that Raphael Robinson's well known essentially undecidable theoryR remains essentially undecidable if the fifth axiom scheme\(\left( {x \leqq \bar n \vee \bar n \leqq x} \right)\) is omitted. We note that whether the resulting system is in a sense “minimal essentially undecidable” depends on what the basic constants are taken to be. We give an essentially undecidable theory based on three axiom schemes involving only multiplication and less than or equals.

In [1] Myhill gave a system K in which much of the classical theory of rational and real numbers could be carried out but which was nevertheless complete; this was achieved by sacrificing the notions of negation and universal quantification and introducing instead the ancestral as a primitive idea. He mentioned two ways of dealing with real numbers in K; the first was to use the half-section corresponding to x, i.e. the class of rationals r satisfying r ≤, x; the second was to use the whole-section corresponding to x, i.e. the relation between rationals r, s which holds when r ≤ x and x ≤ s. In [2] he proved various theorems about the relation between these two forms of definition. In particular he proved that every bounded class of half-sections definable in K has a least bound definable in K. In a footnote he said, ‘This theorem risks triviality because it is doubtful whether there exists such a bounded class.’ We show in this note that this is the case; in fact there are not even any definable classes consisting entirely of classes of rationals. It is not difficult to see how this happens; since K has no negation, any statement matrix A (α) defining a class of classes of sequences is satisfied by α = V, where V is the class of all sequences. Thus there are no classes which consist entirely of half-sections. The same is true for whole-sections, showing that Conjecture I of [1], viz. ‘Not every bounded class of whole-sections definable in K has a least bound definable in K’, is trivially false. Since it may be of some intrinsic interest, we give below a more complete description of the classes of classes of sequences which are definable in K (or rather in K1 see below) than is necessary merely in order to prove the above assertion.

In this third and last paper on inner models we consider some of the inherent limitations of the method of using inner models of the type defined in 1.2 for the proof of consistency results for the particular system of set theory under consideration. Roughly speaking this limitation may be described by saying that practically no further consistency results can be obtained by the construction of models satisfying the conditions of theorem 1.5, i.e., conditions 1.31, 1.32, 1.33, 1.51, viz.:This applies in particular to the ‘complete models’ defined in 1.4. Before going on to a precise statement of these limitations we shall consider now the theorem on which they depend. This is concerned with a particular type of complete model examples of which we call “proper complete models”; they are those complete models which are essentially interior to the universe, those whose classes are sets of the universe constituting a class thereof, i.e., those for which the following proposition is true:The main theorem of this paper is that the statement that there are no models of this kind can be expressed formally in the same way as the axioms A, B, C and furthermore it can be proved that if the axiom system A, B, C is consistent then so is the system consisting of axioms A, B, C, plus this new hypothesis that there exist no proper complete models. When combined with the axiom ‘V = L’ introduced by Gödel in (1) this new hypothesis yields a system in which any normal complete model which exists has for its universal class V, the universal class of the original system.

Van der Waerden (1930 a , pp. 128- 131) has discussed the problem of carrying out certain field theoretical procedures effectively, i.e. in a finite number of steps. He defined an ‘explicitly given’ field as one whose elements are uniquely represented by distinguishable symbols with which one can perform the operations of addition, multiplication, subtraction and division in a finite number of steps. He pointed out that if a field K is explicitly given then any finite extension K' of K can be explicitly given, and that if there is a splitting algorithm for K , i.e. an effective procedure for splitting polynomials with coefficients in K into their irreducible factors in K [x], then(1) there is a splitting algorithm for K' . He observed in (1930 b ), however, that there was no general splitting algorithm applicable to all explicitly given fields K , or at least that such an algorithm would lead to a general procedure for deciding problems of the type ‘Does there exist an n such that E(n) ?’, where E is an arbitrarily given property of positive integers such that there is an algorithm for deciding for any n whether E(n) holds. In this paper we review these results in the light of the precise definition of algorithm (finite procedure) given by Church (1936), Kleene (1936) and Turing (1937) and discuss the existence of a number of field theoretical algorithms in explicit fields, and the effective construction of field extensions. We sharpen van der Waerden’s result on the non-existence of a general splitting algorithm by constructing (§7) a particular explicitly given field which has no splitting algorithm. We show (§7) that the result on the existence of a splitting algorithm for a finite extension field does not hold for inseparable extensions, i.e. we construct a particular explicitly given field K and an explicitly given inseparable algebraic extension K ( x ) such that K has a splitting algorithm but K ( x ) has not. (2) We note also (in §6) that there exist two isomorphic explicitly given fields, one of which possesses a splitting algorithm but the other of which does not. Thus the sort of properties of fields we are interested in depend not only on the abstract field but also on the particular representation chosen. It is necessary therefore to state rather carefully our definitions of explicit ring, extension ring, splitting algorithm, etc., and to introduce the concept of explicit isomorphism (3) and homomorphism. This occupies §§ 1,2 and 3. On the basis of these definitions we then discuss the existence of some fundamental field theoretical algorithms in explicit fields and their extension fields. This leads also to a classification of the types of extension fields which can be effectively constructed.

Negation as failure is sound both for the closed world assumption and the completed database or completion, comp ( P ) of a program P . In general it is not complete for either of these declarative semantics. Indeed there can be no semantics for which it is both sound and complete, for all programs and queries, because non-ground negative literals cannot be dealt with, and cause floundering. By extending the negation as failure rule we exclude floundering and we give a semantics T ω ( P ) for which the extended rule is both sound and complete. T ω ( P ) is a weak version of comp ( P ) based on an iterative construction. We show that the soundness and completeness results still hold if the classical consequence relation ⊢ is replaced by a weaker relation ⊢ 31 which is sound for both 3-valued logic and intuitionistic logic.

Shepherdson showed that there are maximal safe computation rules R m for SLDNF resolution, such that if a query succeeds under any safe rule it succeeds under R m , and if it fails under any safe rule it fails under R m . Later he showed that such maximal rules also get all possible answers, i.e., if a query succeeds with answer θ under any safe rule, then it succeeds with answer equivalent to θ under R m . The question was raised there, whether there were always recursive maximal rules. We answer this negatively. We also show the unsolvability of the problems of deciding whether a query leads to a dead end, whether the Clark completion comp( P ) of a program P is consistent, and whether a query which is known to be a logical consequence of the program succeeds in PROLOG.

Mints (1986) has given a deductive calculus, a set of proof rules, for pure Prolog such that the goal X = A1,..., An succeeds in Prolog iff X is derivable in this calculus and X fails in Prolog iff (∼)X is derivable in this calculus. We summarise Mints' results and give appropriate modifications of his calculus to deal with (a) use of negated goals in Prolog, (b) SLD- resolution, (c) SLDNF-resolution, (d) extensions of SLDNF-resolution allowing negation as failure to be applied to nonground negative literals.

The G -schemes are a class of structured flowchart schemes defined algebraically by Elgot in [1]. Bloom and Tindell [2] gave a graph theoretic characterization of the biaccessible G -schemes, i.e. those in which every vertex is on a path from begin to exit. We give here a graph theoretic characterization of the entire class of G -schemes, and also of a smaller and simpler class, the T L -schemes of [5].

The flowchart schemes called “reducible” are of interest because (1) they schematize programs without “go to” statements; (2) for every flowchart scheme there is a reducible one which is step-by-step equivalent to it; (3) they manipulate readily. The reducible flowchart schemes admit both graph-theoretic and algebraic descriptions. A flowchart scheme F with n begins and p exits is reducible iff both (a) for every vertex v there is a begin-path (i.e. a path from a begin vertex) which ends in v (b) for every closed path C there is a vertex vC of C such that every begin path to a vertex of C meets vC. Algebraically: F is reducible iff it can be built up from atomic flowchart schemes (which may be thought of as corresponding to single instructions) and surjective trivial flowchart schemes (which may be thought of as redirecting flow of control) by means of composition (∘), separated pairing (+), and scalar iteration (†). Dropping † yields the accessible, acyclic flowchart schemes.

A “scalar” flowchart scheme, i.e. one with a single begin “instruction” is reducible iff its underlying flowgraph is reducible in the sense of Cocke and Allen or Hecht and Ullman. We characterize the class of reducible scalar flowchart schemes as the smallest class containing certain members and closed under certain operations (on and to flowchart schemes). These operations are “semantically meaningful” in the sense that operations of the same form are meaningful for “the” functions (or partial functions) computed by interpreted flowchart schemes; moreover, the schemes and the functions “are related by a homomorphism.” By appropriately generalizing “flowgraph” to (possibly) several begins (i.e. entries) we obtain a class of reducible “vector” flowchart schemes which can be characterized in a manner analogous to the scalar case but involving simpler more basic operations (which are also semantically meaningful). A significant side effect of this semantic viewpoint is the treatment of multi-exit flowchart schemes on an equal footing with single exit ones.

S OF PAPERS 425 logic, Notre Dame Journal of Formal Logic, vol. 12 (1971), pp. 447-453. [2] , The relative consistency of the class axioms of abstraction and extensionality and the Axioms of NBG in a three-valued logic, Notre Dame Journal of Formal Logic, vol. 13 (1972), pp. 161-176. [31 R. ROUTLEY, Ultralogic as universal?, Relevance Logic Newsletter, vol. 2 (1977), pp. 50-89 and pp. 138-175, and Exploring Meinong's jungle and beyond, A.N.V., 1980. M.W. BUNDER, The consistency of a higher order predicate calculus and set theory based on combinatory logic. In this paper it is shown that proofs in the higher order predicate calculus of [2] and [3] (which is a weaker version of the system in [1]) can be normalised in a particular way. This leads directly to the weak consistency result that certain terms without normal forms are not provable. It is then possible to show that the false proposition PHI (every proposition is a theorem) is not provable using a normalised proof. As negation (r) is defined by Ax (x v EHI) this proves that for no term x, both x and rx are provable. In addition it can be shown that the consistency proof is not affected by the extra axioms of [2] which lead to the pairing, comprehension, replacement, sum set, power set and infinity properties of set theory. Similarly the addition of most of the extra axioms, including extensionality of [3] which also lead to comprehension, pairing, replacement and sum set, does not effect the consistency proof.