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)

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)

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 (...) class='Hi'>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)

Akama et al. [1] introduced a hierarchical classification of first-order formulas for a hierarchical prenex normal form theorem in semi-classical arithmetic. In this paper, we give a justification for the hierarchical classification in a general context of first-order theories. To this end, we first formalize the standard transformation procedure for prenex normalization. Then we show that the classes $$\textrm{E}_k$$ and $$\textrm{U}_k$$ introduced in [1] are exactly the classes induced by $$\Sigma _k$$ and $$\Pi _k$$ respectively via the (...) transformation procedure in any first-order theory. (shrink)

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)

Contemporary sociosemiotics is a way to transcend borderlines between trends inside semiotics, and also other disciplines. Whereas semiotics has been considered as an interdisciplinary field of research par excellence, sociosemiotics can point directions at transdisciplinary research. The present article will try to conjoin the structural and the processual views on culture and society, binding them together with the notion of signification. The signification of space will illustrate the dynamic between both cultures and metacultures, and cultural mainstreams and subcultures. This paper (...) pays attention to the practice of sociocultural semiotisation of space and territorialisation by diverse examples and different sociocultural levels that imply semiotic cooperation between several members of groups that can be characterised as socii. We analyse territorialisation by graffiti, by furnishing spatial environment through artistic manners, by shaping the semiotic essence of cities through naming, renaming and translating street names, by pinning and structuring territories with monuments, by landmarking and mapping cultural space through individualisation of cities. We will see how principles of semiotisation of space are valid on different levels and how these principles form a transdisciplinary object of study as ‘semiotisation of space’, and how space can be regarded as a genuinely transdisciplinary research object. Individual, culture, and society are connected in such an object both as constituents and as a background of study. (shrink)

Contemporary sociosemiotics is a way to transcend borderlines between trends inside semiotics, and also other disciplines. Whereas semiotics has been considered as an interdisciplinary field of research par excellence, sociosemiotics can point directions at transdisciplinary research. The present article will try toconjoin the structural and the processual views on culture and society, binding them together with the notion of signification. The signification of space willillustrate the dynamic between both cultures and metacultures, and cultural mainstreams and subcultures. This paper pays attention (...) to the practice of sociocultural semiotisation of space and territorialisation by diverse examples and different sociocultural levels that imply semiotic cooperation between several members of groups that can be characterised as socii. We analyse territorialisation by graffiti, by furnishing spatial environment through artistic manners, by shaping the semiotic essence of cities through naming, renaming and translating street names, by pinning and structuring territories with monuments, by landmarking and mapping cultural space through individualisation of cities. We will see how principles of semiotisation of space are valid on different levels (individual and social, formal and informal, democratic and hegemonic, cultural and subcultural) and how these principles form a transdisciplinary object of study as ‘semiotisation of space’, and how space can be regarded as a genuinely transdisciplinary research object. Individual, culture, and society are connected in such an object both as constituents and as a background of study. (shrink)

The present paper has three objectives: Presenting an actualization of a proof of the decidability of monadic predicates logic in the contemporary model theory context; Show examples of decidable and undecidable fragments inside First order logic, offering an original proof of the following theorem: Any formula of First of order logic is decidable if its prenex normal form is in the following form: ∀x1,…,∀xn∃y1,…,∃ymφ; Presenting a theorem that characterizes the validity of First order logic by the tautologicity of (...) Propositional logic, said result is interesting since immediately arises the doubt of how to conciliate said characterization with Alonzo Church’s Undecidability Theorem for First Order Logic. (shrink)

Emotions normally include elements of feeling, motivation, and also intentionality; but the argument of this essay is that there can be emotion without feeling, emotion without corresponding motivation, and emotion without an intentional relation to an object such that the emotion is (among other things) a belief about or construal of it. Many recent writers have claimed that some form of intentionality is essential to emotion, and then have created lines of defence for this thesis. Thus, what look like troublesome (...) cases of emotions can be regarded as having a global intentionality or as being “mood-like”. Alternatively surges of non-intentional joy or ecstasy can be regarded as merely feelings rather than as emotions, and what people experience in response to absolute music can be treated similarly. A clear view of how we normally talk about moods, emotions, and feelings however undermines these defences; and in particular we can understand the role of emotions in relation to absolute music once we become clear about the way in which musical content stands in for intentional objects. (shrink)

One striking feature of pornographic images is that they emphasize what is depicted and underplay the way it is depicted: the experience of pornography rarely involves awareness of the picture’s composition or of visual rhyme. There are various ways of making this distinction between what is depicted in a picture and the way the depicted object is depicted in it. Following Richard Wollheim, I call these two aspects, the ‘what’ and ‘how’ of pictorial representation ‘recognitional’ and ‘configurational’, respectively. Some pictures (...) emphasize one of these aspects while underplaying the other. Pornographic pictures try to trigger as little attention to the ‘configurational’ aspect as possible. Instead of examining pornography, where the ‘configurational’ aspect of experience is underplayed, I focus on a historical attempt to create images of the female body where the ‘recognigional’ element is the one that is underplayed and the ‘configurational’ elements of the picture form an essential part of our experience. The pictures I have in mind are André Kertész’s series of photographs from 1933, called Distortions. I argue that Kertész’s Distortions are in this respect the counterpoint of pornography: they may be the least pornographic representations of the female nude. Instead of ignoring the ‘configurational aspects of the picture, making the picture transparent and fully at the service of showing the female body and thus to trigger arousal, Kertész aims to achieve the exact opposite. His photographs strip the female body of all its sexual connotations and draw our attention to the formal features of the picture – which is quite a feat in the light of the subject matter of these pictures that normally draw our attention away from the formal features of pictures. (shrink)

There are several areas in applied logic where deletion from databases is involved in one way or another:Belief contraction Triggers of the form ‘If condition then remove A’, which are extensively used in database management systemsResource considerations as in relevance and linear logics, where addition or removal of resource can affect provabilityFree logic and the like, where existence and non-existence of individuals affects quantification.All of these areas have certain logical difficulties relating to the removal of elements. These difficulties are normally (...) overcome by working on the meta-level. This paper offers a comprehensive model in which the various forms of removal are treated on the object level, i.e., as connectives of the object language. (shrink)

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)

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 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)

We start with a simple proof of Leivant's normal form theorem for ∑11 formulas over finite successor structures. Then we use that normal form to prove the following:1. over all finite structures, every ∑21 formula is equivalent to a ∑21 formula whose first-order part is a Boolean combination of existential formulas, and2. over finite successor structures, the Kolaitis-Thakur hierarchy of minimization problems collapses completely and the Kolaitis-Thakur hierarchy of maximization problems collapses partially.The normal form theorem for ∑21 (...) fails if ∑21 is replaced with ∑11 or if infinite structures are allowed. (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)

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.

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)

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)

Formulas of n variables of Łukasiewicz sentential calculus can be represented, via McNaughton’s theorem, by piecewise linear functions, with integer coefficients, from hypercube [0,1] n to [0,1], called McNaughton functions. As a consequence of the McNaughton representation of a formula it is obtained a canonical form of a formula. Indeed, up to logical equivalence, any formula can be written as an infimum of finite suprema of formulas associated to McNaughton functions which are truncated functions to $[0,1]$ of the restriction to (...) [0,1] n of single hyperplanes, for short, called simple McNaughton functions. In the present paper we will concern with the problem of presenting formulas of Lukasiewicz sentential calculus in normal form. Here we list the main results we obtained: a) we give an axiomatic description of some classes of formulas having the property to be canonically mapped one-to-one onto the class of simple Mc Naughton functions; b) we provide normal forms for Lukasiewicz sentential calculus, making use of formulas defined in a); c) we prove the polynomial complexity of formulas, in normal form, coming from a certain class described as in a); d) we extend the results described in a), b) and c) to Rational Lukasiewicz 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.

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)

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)

The Feferman–Vaught theorem provides a way of evaluating a first order sentence \(\varphi \) on a disjoint union of structures by producing a decomposition of \(\varphi \) into sentences which can be evaluated on the individual structures and the results of these evaluations combined using a propositional formula. This decomposition can in general be non-elementarily larger than \(\varphi \). We introduce a “tree” generalization of the prenex normal form (PNF) for first order sentences, and show that for an (...) input sentence in this form having a fixed number of quantifier alternations, a Feferman–Vaught decomposition can be obtained in time elementary in the size of the sentence. The sentences in the decomposition are also in tree PNF, and further have the same number of quantifier alternations and the same quantifier rank as the input sentence. We extend this result by considering binary operations other than disjoint union, in particular sum-like operations such as join, ordered sum and NLC-sum, that are definable using quantifier-free translation schemes. (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)

Using representations of nonflat Scott domains to model type systems, it is natural to wish that they be “linear”, in which case the complexity of the fundamental test for entailment of information drops from exponential to linear, the corresponding mathematical theory becomes much simpler, and moreover has ties to models of computation arising in the study of sequentiality, concurrency, and linear logic. Earlier attempts to develop a fully nonflat semantics based on linear domain representations for a rich enough type system (...) allowing inductive types, were designed in a way that felt rather artificial, as it featured certain awkward and counter‐intuitive properties; eventually, the focus turned on general, nonlinear representations. Here we try to turn this situation around, by showing that we can work linearly in a systematic way within the nonlinear model, and that we may even restrict to a fully linear model whose objects are in a bijective correspondence with the ones of the nonlinear and are easily seen to form a prime algebraic domain. To obtain our results we study mappings of finite approximations of objects that can be used to turn approximations into normal and linear forms. (shrink)

We are concerned with showing how ‘labelled’ Natural Deduction presentation systems based on an extension of the so-called Curry-Howard functional interpretation can help us understand and generalise most of the deduction calculi designed to deal with the logical notion of existential quantification. We present the labelling mechanism for ‘’ using what we call ‘ɛ-terms’, which have the form of ‘a’) in a dual form to the ‘Ax.f’ terms of in the sense that the ‘witness’ is chosen at the time of (...) assertion/introduction.With the intention of demonstrating the generality of our framework, we provide a brief comparison with some other calculi of existentials, including the model-theoretic interpretations of Skolem and Herbrand, indicating the way in which some of the classical results on prenex normal forms can be extended to a wide range of logics. The essential ingredient is to look at the conceptual framework of labelled natural deduction as an attempted reconstruction of Frege's functional calculus where the devices of the Begriffsschrift work separately from, yet in harmony with, those of the Grundgesetze 1. (shrink)

We prove a local normal form theorem of the Gaifman type for the infinitary logic L∞ωω whose formulas involve arbitrary unary quantifiers but finite quantifier rank. We use a local Ehrenfeucht-Fraïssé type game similar to the one in [9]. A consequence is that every sentence of L∞ωω of quantifier rank n is equivalent to an infinite Boolean combination of sentences of the form ψ, where ψ has counting quantifiers restricted to the -neighborhood of y.

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.