In contrast to Hintikka’s enormously complex distributive normal forms of first- order logic, this paper shows how to generate minimized disjunctive normal forms of first-order logic. An effective algorithm for this purpose is outlined, and the benefits of using minimized disjunctive normal forms to explain the truth conditions of propo- sitions expressible within pure first-order logic are presented.

The system of natural deduction that originated with Gentzen , and for which Prawitz proved a normalization theorem, is re-cast so that all elimination rules are in parallel form. This enables one to prove a very exigent normalization theorem. The normal forms that it provides have all disjunction-eliminations as low as possible, and have no major premisses for eliminations standing as conclusions of any rules. Normal natural deductions are isomorphic to cut-free, weakening-free sequent proofs. This form of (...) normalization theorem renders unnecessary Gentzen's resort to sequent calculi in order to establish the desired metalogical properties of his logical system.Ultimate normal forms are well-adapted to the needs of the computational logician, affording valuable constraints on proof-search. They also provide an analysis of deductive relevance. There is a deep isomorphism between natural deductions and sequent proofs in the relevantized system. (shrink)

In this note we sketch a decision procedure for S3.51 based on reduction to conjunctive normal form. Using the following theorem of S3.5: and its dual for M over a conjunction, any formula can be reduced by standard methods (as in S52) to a conjunction of disjunctions of the form where Í is (p ⊃ p), 0 is ∼(p ⊃ p) and α — λ are all PC-wffs (i.e. they contain no modal operators).

We show that in quantum logic of closed subspaces of Hilbert space one cannot substitute quantum operations for classical (standard Hilbert space) ones and treat them as primitive operations. We consider two possible ways of such a substitution and arrive at operation algebras that are not lattices what proves the claim. We devise algorithms and programs which write down any two-variable expression in an orthomodular lattice by means of classical and quantum operations in an identical form. Our results show that (...) lattice structure and classical operations uniquely determine quantum logic underlying Hilbert space. As a consequence of our result, recent proposals for a deduction theorem with quantum operations in an orthomodular lattice as well as a, substitution of quantum operations for the usual standard Hilbert space ones in quantum logic prove to be misleading. Quantum computer quantum logic is also discussed. (shrink)

In this paper, we describe the completeness of a calculation procedure of logic programs. The procedure is the combination of two procedures, a replacement procedure of atoms in the goal by the bodies or the negation of the bodies of rules in the program, and a transformation procedure of equations to disjunctive normal forms equivalent under Clark's Equational Theory. To combine replacement of atoms in the goal to logical formulae determined from the program and transformation of equations (...) to DNF equivalent under CET is a method by which procedures with the capability of expressing answers in DNF can be build, so it is a leading method for expressing answers in a form including negation. Some procedures based on the method are devised, and their calculation capabilities are shown by applying the theory of completed programs. However, the procedure that uses the bodies or the negation of the bodies of rules for replacement has higher calculation capability, and is intuitively more natural than they. Therefore, to clarify the calculation capability of the procedure is considered an important subject for research into calculation procedures of logic programs with the capability for expressing answers in a form including negation. Moreover, since the completeness is realized by standing on the viewpoint of treating the implication symbol as a different implication symbol from usual, and interpreting logic programs in three-valued logic, examples which support the viewpoint are also described. (shrink)

In this paper, we describe an improvement of a calculation procedure of logic programs. The procedure proposed before is the combination of a replacement procedure of logical formulae and a transformation procedure of equations to disjunctive normal form, and it can calculate logical consequences of the completion of any given first-order logic program, which is equivalent to the FLP in two-valued logic, soundly and completely in three-valued logic. The new procedure is also the combination of them, but the (...) transformation procedure is improved to be able to calculate two-valued logical consequences of the FLP more than the old one. We prove that it can calculate logical consequences of a completed program, which is not equivalent to the completion of the FLP, soundly and completely in three-valued logic. (shrink)

Abstract.Carrying out a suggestion by Kreisel, we adapt Gödel’s functional interpretation to ordinary first-order predicate logic(PL) and thus devise an algorithm to extract Herbrand terms from PL-proofs. The extraction is carried out in an extension of PL to higher types. The algorithm consists of two main steps: first we extract a functional realizer, next we compute the β-normal-form of the realizer from which the Herbrand terms can be read off. Even though the extraction is carried out in the extended (...) language, the terms are ordinary PL-terms. In contrast to approaches to Herbrand’s theorem based on cut elimination orɛ-elimination this extraction technique is, except for the normalization step, of low polynomial complexity, fully modular and furthermore allows an analysis of the structure of the Herbrand terms, in the spirit of Kreisel ([13]), already prior to the normalization step. It is expected that the implementation of functional interpretation in Schwichtenberg’s MINLOG system can be adapted to yield an efficient Herbrand-term extraction tool. (shrink)

The aim of this paper is to clarify why propositional logic is Post complete and its weak completeness was almost unnoticed by Hilbert and Bernays, while first-order logic is Post incomplete and its weak completeness was seen as an open problem by Hilbert and Ackermman. Thus, I will compare propositional and first-order logic in the Prinzipien der Mathematik, Bernays’s second Habilitationsschrift and the Grundzüge der Theoretischen Logik. The so called “arithmetical interpretation”, the conjunctive and disjunctive normal forms (...) and the soundness of the propositional rules of inference deserve special emphasis. (shrink)

Herbrand disjunctions are a means for reducing the problem ofwhether a first-oder formula is valid in an open theory T or not to theproblem whether an open formula, one of the so called Herbrand disjunctions,is T -valid or not. Nevertheless, the set of Herbrand disjunctions, which hasto be examined, is undecidable in general. Fore this reason the practicalvalue of Herbrand disjunctions has been estimated negatively .Relying on completeness proofs which are based on the algebraizationtechnique presented in [30], but taking a (...) more optimistic view, we show howHerbrand disjunctions become the base of a method for building in theoriesinto automatic theorem provers [26]. Surveying newer results we discusshow to treat heterogeneous theories [29] as well as practical implications ofdifferent normal form transformations. (shrink)

Most, perhaps all, non-classical logics are a blend of classical logic with extralogical elements. Possibly this thesis has no general proof, and only a casuistic argument can be provided. I discuss a case of paraconsistency that results of applying a “filter” to two syllogistics. These syllogistics incorporate two ideas of Nikolai Vasiliev: the idea of a complete system of contrary judgements, and the idea of double judgements. I also show how these results can be extended to propositional logic, with the (...) aid of the conjunctive and disjunctive normal forms. Despite the non-classical appearance, it is used, without exception, the classical notion of deductive validity: a conclusion cannot carry more information, but may carry less information than the information carried by the collection of the premisses. (shrink)

Warren Goldfarb, Deductive Logic, Hackett Publishing Company, 2003.    : 0872206602. Deductive Logic is an introductory textbook in formal logic. The book is divided into four parts covering truth-functional logic, monadic quantifi- cation, polyadic quantification and names and identity, and there are exercises for all these topics at the end of the book. In the truth-functional logic part, the reader learns to produce paraphrases of English statements and arguments in logical notation, then about the semantic properties of such (...) paraphrased statements and arguments, such as satisfiability, implication and equivalence and finally there is an axiomatic proof method and some important extras such as disjunctive normal form and expressive adequacy. Parts two and three mirror this analysis/assessment/reflection structure for monadic and polyadic quantification, though this time the proof system is a natural deduction one, and part three contains a completeness proof for that system. The fourth part of the book introduces names, the identity predicate and descriptions and examines the additional expressive power which these provide. I do not think there should be any doubt that this is an excellent book; it presents the essential topics of a first logic course with accuracy, clarity and attention to detail, and it makes material that can be confusing the first time round—say, the translation of conditionals—transparent and easy to understand. But there are a lot of good introductory logic textbooks out there, so I will say something about how it resembles and differs from some other books, and then discuss one minor irritation with this one. (shrink)

Although the notion of spatiality has always lurked in the background of discussions of literary form, the self-conscious use of the term as a critical concept is generally traced to Joseph Frank's seminal essay of 1945, "Spatial Form in Modern Literature."1 Frank's basic argument is that modernist literary works are "spatial" insofar as they replace history and narrative sequence with a sense of mythic simultaneity and disrupt the normal continuities of English prose with disjunctive syntactic arrangements. This argument (...) has been attacked on several fronts. An almost universal objection is that spatial form is a "mere metaphor" which has been given misplaced concreteness and that it denies the essentially temporal nature of literature. Some critics will concede that the metaphor contains a half-truth, but one which is likely to distract attention from more important features of the reading experience. The most polemical attacks have come from those who regard spatial form as an actual, but highly regrettable, characteristic of modern literature and who have linked it with antihistorical and even fascist ideologies.2 Advocates of Frank's position, on the other hand, have generally been content to extrapolate his premises rather than criticize them, and have compiled an ever-mounting list of modernist texts which can be seen, in some sense, as "antitemporal." The whole debate can best be advanced, in my view, not by some patchwork compromise among the conflicting claims but by a radical, even outrageous statement of the basic hypothesis in its most general form. I propose, therefore, that far from being a unique phenomenon of some modern literature, and far from being restricted to the features which Frank identifies in those works , spatial form is a crucial aspect of the experience and interpretation of literature in all ages and cultures. The burden of proof, in other words, is not on Frank to show that some works have spatial form but on his critics to provide an example of any work that does not. · 1. Frank's essay first appeared in Sewanee Review 53 and was revised in his The Widening Gyre . Frank's basic argument has not changed essentially even in his most avante-garde statements; he still regards spatial form "as a particular phenomenon of modern avante-garde writing." See "Spatial Form: An Answer to Critics," Critical Inquiry 4 : 231-52. A useful bibliography, "Space and Spatial Form in Narrative," is being complied by Jeffrey Smitten .· 2. This charge generally links the notion of spatial form with Wyndham Lewis and Ezra Pound, the imagist movement, the "irrationality" and pessimistic antihistoricism of modernism, and the conservative Romantic tradition. Frank discusses the complex motives behind these associations in the work of Robert Weimann and Frank Kermode in his "Answer to Critics," pp. 238-48. W. J. T. Mitchell, editor of Critical Inquiry, is the author of Blake's Composite Art, and The Last Dinosaur Book: The Life and Times of a Cultural Icon. The present essay is part of Iconology: The Image in Literature and the Visual Arts. "Diagrammatology" appeared in the Spring 1981 issue of Critical Inquiry. Leon Surette responds to the current essay in "‘Rational Form in Literature’". (shrink)

This paper describes a decision procedure for disjunctions of conjunctions of anti-prenex normal forms of pure first-order logic (FOLDNFs) that do not contain V within the scope of quantifiers. The disjuncts of these FOLDNFs are equivalent to prenex normal forms whose quantifier-free parts are conjunctions of atomic and negated atomic formulae (= Herbrand formulae). In contrast to the usual algorithms for Herbrand formulae, neither skolemization nor unification algorithms with function symbols are applied. Instead, a procedure is (...) described that rests on nothing but equivalence transformations within pure first-order logic (FOL). This procedure involves the application of a calculus for negative normal forms (the NNF-calculus) with A -||- A & A (= &I) as the sole rule that increases the complexity of given FOLDNFs. The described algorithm illustrates how, in the case of Herbrand formulae, decision problems can be solved through a systematic search for proofs that reduce the number of applications of the rule &I to a minimum in the NNF-calculus. In the case of Herbrand formulae, it is even possible to entirely abstain from applying &I. Finally, it is shown how the described procedure can be used within an optimized general search for proofs of contradiction and what kind of questions arise for a &I-minimal proof strategy in the case of a general search for proofs of contradiction. (shrink)

This papers presents δ-resolution, a dual resolution calculus. It is based on standard resolution, and used appropriate formulae equivalent to disjunctive normal forms, instead of conjunctive normal ones, as it is the case for resolution. This duality is then useful to create a calculus for abductive process, as a way to construct a set of abductive solutions. The proposed calculus is compared to semantic tableaux, an standard logical framework, aslo illuminating when studying abduction.δ-resolution calculus is a (...) contribution to logic programming, and it further suggests new possibilities to explore abduction at a first order level, in the lines of those proposed in [9]. (shrink)

Deductive Logic is an introductory textbook in formal logic. The book is divided into four parts covering (i) truth-functional logic, (ii) monadic quantifi- cation, (iii) polyadic quantification and (iv) names and identity, and there are exercises for all these topics at the end of the book. In the truth-functional logic part, the reader learns to produce paraphrases of English statements and arguments in logical notation (this subsection is called “analysis”), then about the semantic properties of such paraphrased statements and arguments, (...) such as satisfiability, implication and equivalence (“logical assessment”) and finally (“reflection”) there is an axiomatic proof method and some important extras such as disjunctive normal form and expressive adequacy. Parts two and three mirror this analysis/assessment/reflection structure for monadic and polyadic quantification, though this time the proof system is a natural deduction one, and part three contains a completeness proof for that system. The fourth part of the book introduces names, the identity predicate and descriptions and examines the additional expressive power which these provide. (shrink)

The structure of derivations in natural deduction is analyzed through isomorphism with a suitable sequent calculus, with twelve hidden convertibilities revealed in usual natural deduction. A general formulation of conjunction and implication elimination rules is given, analogous to disjunction elimination. Normalization through permutative conversions now applies in all cases. Derivations in normal form have all major premisses of elimination rules as assumptions. Conversion in any order terminates.Through the condition that in a cut-free derivation of the sequent Γ⇒C, no inactive (...) weakening or contraction formulas remain in Γ, a correspondence with the formal derivability relation of natural deduction is obtained: All formulas of Γ become open assumptions in natural deduction, through an inductively defined translation. Weakenings are interpreted as vacuous discharges, and contractions as multiple discharges. In the other direction, non-normal derivations translate into derivations with cuts having the cut formula principal either in both premisses or in the right premiss only. (shrink)

Let A be a formula without implications, and Γ consist of formulas containing disjunction and falsity only negatively and implication only positively. Orevkov and Nadathur proved that classical derivability of A from Γ implies intuitionistic derivability, by a transformation of derivations in sequent calculi. We give a new proof of this result , where the input data are natural deduction proofs in long normal form involving stability axioms for relations; the proof gives a quadratic algorithm to remove the stability (...) axioms. This can be of interest for computational uses of classical proofs. (shrink)

Gentzen's “Untersuchungen” [1] gave a translation from natural deduction to sequent calculus with the property that normal derivations may translate into derivations with cuts. Prawitz in [8] gave a translation that instead produced cut-free derivations. It is shown that by writing all elimination rules in the manner of disjunction elimination, with an arbitrary consequence, an isomorphic translation between normal derivations and cut-free derivations is achieved. The standard elimination rules do not permit a full normal form, which explains (...) the cuts in Gentzen's translation. Likewise, it is shown that Prawitz' translation contains an implicit process of cut elimination. (shrink)

We study cut-elimination in first-order classical logic. We construct a sequence of polynomial-length proofs having a non-elementary number of different cut-free normal forms. These normal forms are different in a strong sense: they not only represent different Herbrand-disjunctions but also differ in their propositional structure. This result illustrates that the constructive content of a proof in classical logic is not uniquely determined but rather depends on the chosen method for extracting it.

I provide a proof method for First Order Monadic Predicate Logic. This method uses the Normal Form of Herbrand and the Disjunctive and Conjunctive Normal Forms for Propositional Logic. The validity is determined by mere inspection of the presence and arrangement of formulas that act as informational atoms. The exact relationship between First Order Monadic Predicate Logic and the extended syllogistic developed during the nineteenth century is established by the Normal Form of Herbrand.

A new reduction class is presented for the satisfiability problem for well-formed formulas of the first-order predicate calculus. The members of this class are closed prenex formulas of the form ∀ x∀ yC. The matrix C is in conjunctive normal form and has no disjuncts with more than three literals, in fact all but one conjunct is unary. Furthermore C contains but one predicate symbol, that being unary, and one function symbol which symbol is binary.

A notation for an ordinal using patterns of resemblance is based on choosing an isominimal set of ordinals containing the given ordinal. There are many choices for this set meaning that notations are far from unique. We establish that among all such isominimal sets there is one which is smallest under inclusion thus providing an appropriate notion of normal form notation in this context. In addition, we calculate the elements of this isominimal set using standard notations based on collapsing (...) functions. This provides a capstone to the results in [2, 6, 8, 9, 7], using further refinement of ordinal arithmetic developed in [8] which then both allows for a simple characterization of normal forms for patterns of order one and will play a key role in the arithmetical analysis of pure patterns of order two, [5]. (shrink)

Montague [7] translates English into a tensed intensional logic, an extension of the typed -calculus. We prove that each translation reduces to a formula without -applications, unique to within change of bound variable. The proof has two main steps. We first prove that translations of English phrases have the special property that arguments to functions are modally closed. We then show that formulas in which arguments are modally closed have a unique fully reduced -normal form. As a corollary, translations (...) of English phrases are contained in a simply defined proper subclass of the formulas of the intensional logic. (shrink)

The paper gives a simple result on the existence of normal forms for the following equivalence relation between objects of a category: A∼B if and only if there are maps A→B and B→A , under the hypothesis that the category has epi-mono factorizations and each object has finitely many sub-objects and quotient-objects. Applications to algebra, logic, automata theory, databases are presented.

Herbrand’s theorem is one of the most fundamental results about first-order logic. In the context of proof analysis, Herbrand-disjunctions are used for describing the constructive content of cut-free proofs. However, given a proof with cuts, the computation of a Herbrand-disjunction is of significant computational complexity, as the cuts in the proof have to be eliminated first.In this paper we prove a generalization of Herbrand’s theorem: From a proof with cuts, one can read off a small tautology composed of instances of (...) the end-sequent and the cut formulas. This tautology describes the proof in the following way: Each cut induces a formula stating that a disjunction of instances of the cut formula implies a conjunction of instances of the cut formula. All these cut-implications together then imply the already existing instances of the end-sequent. The proof that this formula is a tautology is carried out by transforming the instances in the proof to normal forms and using characteristic clause sets to relate them. These clause sets have first been studied in the context of cut-elimination.This extended Herbrand theorem is then applied to cut-elimination sequences in order to show that, for the computation of an Herbrand-disjunction, the knowledge of only the term substitutions performed during cut-elimination is already sufficient. (shrink)

Statman and Orevkov independently proved that cut-elimination is of nonelementary complexity. Although their worst-case sequences are mathematically different the syntax of the corresponding cut formulas is of striking similarity. This leads to the main question of this paper: to what extent is it possible to restrict the syntax of formulas and — at the same time—keep their power as cut formulas in a proof? We give a detailed analysis of this problem for negation normal form , prenex normal (...) form and monotone formulas. We show that proof reduction to NNF is quadratic, while PNF behaves differently: although there exists a quadratic transformation into a proof in PNF too, additional cuts are needed; the elimination of these cuts requires nonelementary expense in general. By restricting the logical operators to {,,,}, we obtain the type of monotone formulas. We prove that the elimination of monotone cuts can be of nonelementary complexity . On the other hand, we define a large class of problems where cut-elimination of monotone cuts is only exponential and show that this bound is tight. This implies that the elimination of monotone cuts in equational theories is at most exponential. Particularly, there are no short proofs of Statman's sequence with monotone cuts. (shrink)

We use connections between conjunctive game formulas and the theory of inductive definitions to define the notions of a coinductive formula and its approximations. Corresponding to the theory of conjunctive game formulas we develop a theory of coinductive formulas, including a covering theorem and a normal form theorem for many sorted languages. Applying both theorems and the results on "model interpolation" obtained in this paper, we prove a many-sorted interpolation theorem for ω 1 ω-logic, which considers interpolation with respect (...) to the language symbols, the quantifiers, the identity, and countably infinite conjunction and disjunction. (shrink)

After an introductory discussion on Martin-Löf's Intuitionistic Theory of Types , the paper introduces the notion of assumption of high-arity variable. Then the original theory is extended in a very uniform way by means of the new assumptions. Some improvements allowed by high-arity variables are shown. The main result of the paper is a normal form theorem for HITT. The detailed proof follows a computability method ‘a la Tait’. The main consequences of the normal form theorem are: the (...) consistency of HITT, which also implies the consistency of ITT, and the computability of any judgement derived within HITT. Besides that, a canonical form theorem is shown: to any derivable judgement we can associate a canonical one whose derivation ends with an introductory rule. The standard disjunction and existential properties follow. Moreover, by using the computational interpretation of types it immediately follows that the execution of any proved correct program terminates. (shrink)

Let $R$ be a convergent term rewriting system, and let $CR$-equality on combinatory logic terms be the equality induced by $\beta \eta R$-equality on terms of the lambda calculus under any of the standard translations between these two frameworks for higher-order reasoning. We generalize the classical notion of strong reduction to a reduction relation which generates $CR$-equality and whose irreducibles are exactly the translates of long $\beta R$-normal forms. The classical notion of strong normal form in combinatory (...) logic is also generalized, yielding yet another description of these translates. Their resulting tripartite characterization extends to the combined first-order algebraic and higher-order setting the classical combinatory logic descriptions of the translates of long $\beta$-normal forms in the lambda calculus. As a consequence, the translates of long $\beta R$-normal forms are easily seen to serve as canonical representatives for $CR$-equivalence classes of combinatory logic terms for non-empty, as well as for empty, $R$. (shrink)

The relationship between extensive and normal form analyses in non-cooperative game theory seems to be dominated, at least traditionally, by the so-called ‘sufficiency of the normal form principle’, according to which all that is necessary to analyse and ‘solve’ an extensive game is already in its normal form representation. The traditional defence of the sufficiency principle, that Myerson (1991, p. 50) attributes to von Neumann and Morgenstern, holds that, with respect to extensive games, it can be assumed (...) without loss of generality, that players formulate simultaneously and independently their strategic plans at the beginning of the game – a situation which, it is claimed, is exactly described by the normal representation of an extensive game. (shrink)

Functions of type n are characteristic functions on n-ary relations. Keenan [5] established their importance for natural language semantics, by showing that natural language has many examples of irreducible type n functions, i.e., functions of type n that cannot be represented as compositions of unary functions. Keenan proposed some tests for reducibility, and Dekker [3] improved on these by proposing an invariance condition that characterizes the functions with a reducible counterpart with the same behaviour on product relations. The present paper (...) generalizes the notion of reducibility (a quantifier is reducible if it can be represented as a composition of quantifiers of lesser, but not necessarily unary, types), proposes a direct criterion for reducibility, and establishes a diamond theorem and a normal form theorem for reduction. These results are then used to show that every positive n function has a unique representation as a composition of positive irreducible functions, and to give an algorithm for finding this representation. With these formal tools it can be established that natural language has examples of n-ary quantificational expressions that cannot be reduced to any composition of quantifiers of lesser degree. (shrink)

A Krom formula of pure quantification theory is a formula in conjunctive normal form such that each conjunct is a disjunction of at most two atomic formulas or negations of atomic formulas. Every class of Krom formulas that is determined by the form of their quantifier prefixes and which is known to have an unsolvable decision problem for satisfiability is here shown to be a conservative reduction class. Therefore both the general satisfiability problem, and the problem of satisfiability in (...) finite models, can be effectively reduced from arbitrary formulas to Krom formulas of these several prefix types. (shrink)

In this paper a proof of the normal form theorem for the closed terms of Girard's system F is given by using a computability method à la Tait. It is worth noting that most of the standard consequences of the normal form theorem can be obtained using this version of the theorem as well. From the proof-theoretical point of view the interest of the proof is that the definition of computable derivation here used does not seem to be (...) well founded. MSC: 03F05, 03B15. (shrink)

The original decision criterion and method of the combined calculus, presented by D. Hilbert and W. Ackermann, and applied by later logicians, are illuminating, but also go seriously awry and lead the universality and preciseness of the combined calculus to be damaged. The main error is that they confuse the two levels of the combined calculus in the course of calculating. This paper aims to resolve the problem through dividing the levels of the combined calculus, introducing a mixed operation mode, (...) and therefore finding a normal-form decision method approximated by that in sentential logic. Finally, this paper provides a more precise proof of Hauber’s theorem by using the normal-form decision method of the combined calculus. (shrink)

We describe a short model-theoretic proof of an extended normal form theorem for derivations in predicate logic which implies in PRA a normal form theorem for the arithmetic derivations . Consider the Gentzen-type formulation of predicate logic with invertible rules. A derivation with proper variables is one where a variable b can occur in the premiss of an inference L but not below this premiss only in the case when L is () or () and b is its (...) eigenvariable. Free variables of such derivation are eigenvariables and free variables of its last sequent. Then any sequent derivable in predicate logic has a cut-free derivation with proper variables where the main formula of any antecedent rule is underivable. The proof is by a simple modification of the construction of a countermodel of the formula from the open branch of its canonical proof-search tree. It extends to intuitionistic and higher order systems. The proof of the corresponding normalization theorem outlined in [8] uses the passage to the infinitary derivations enriched by finitary derivations. The normal form after a modification to make it decidable can be considered as a realization of Gentzen's idea stated at the end of [2], that his notion of reduction for arithmetic can be extended to other fields of mathematics. (shrink)

Akama et al. [1] systematically studied an arithmetical hierarchy of the law of excluded middle and related principles in the context of first-order arithmetic. In that paper, they first provide a prenex normal form theorem as a justification of their semi-classical principles restricted to prenex formulas. However, there are some errors in their proof. In this paper, we provide a simple counterexample of their prenex normal form theorem [1, Theorem 2.7], then modify it in an appropriate way which (...) still serves to largely justify the arithmetical hierarchy. In addition, we characterize a variety of prenex normal form theorems by logical principles in the arithmetical hierarchy. The characterization results reveal that our prenex normal form theorems are optimal. For the characterization results, we establish a new conservation theorem on semi-classical arithmetic. The theorem generalizes a well-known fact that classical arithmetic is $\Pi _2$ -conservative over intuitionistic arithmetic. (shrink)

We show that every formula of L ω 1p is equivalent to one which is a propositional combination of formulas with only one quantifier. It follows that the complete theory of a probability model is determined by the distribution of a family of random variables induced by the model. We characterize the class of distribution which can arise in such a way. We use these results together with a form of de Finetti's theorem to prove an almost sure interpolation theorem (...) for L ω 1p. (shrink)

It is well known that Nash equilibria may not be Pareto-optimal; worse, a unique Nash equilibrium may be Pareto-dominated, as in Prisoners’ Dilemma. By contrast, we prove a previously conjectured result: every finite normal-form game of complete information and common knowledge has at least one Pareto-optimal nonmyopic equilibrium (NME) in pure strategies, which we define and illustrate. The outcome it gives, which depends on where play starts, may or may not coincide with that given by a Nash equilibrium. We (...) use some simple examples to illustrate properties of NMEs—for instance, that NME outcomes are usually, though not always, maximin—and seem likely to foster cooperation in many games. Other approaches for analyzing farsighted strategic behavior in games are compared with the NME analysis. (shrink)

We show that derivations in the nonassociative and commutative Lambek calculus with product can be transformed to a normal form as it is the case with derivations in noncommutative calculi. As an application we obtain that the class of languages generated by categorial grammars based on the nonassociative and commutative Lambek calculus with product is included in the class of CF-languages. MSC: 68Q50, 03D15, 03B65.

A method is described for obtaining conjunctive normal forms for logics using Gentzen-style rules possessing a special kind of strong invertibility. This method is then applied to a number of prominent fuzzy logics using hypersequent rules adapted from calculi defined in the literature. In particular, a normal form with simple McNaughton functions as literals is generated for łukasiewicz logic, and normal forms with simple implicational formulas as literals are obtained for Gödel logic, Product logic, and (...) Cancellative hoop logic. (shrink)

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. (shrink)