On Independence of Variants of the Weak Pigeonhole Principle

The principle states that no oracle circuit can compute a surjection of a onto b. We showthat is independent of for various choices of the parameters, , , P. We also improve the known separation of iWPHP(PV) from under cryptographic assumptions.     

Analytic Calculi for Logics of Ordinal Multiples of Standard t-Norms

For two propositional fuzzy logics, we present analytic proofcalculi, based on relational hypersequents. The logic consideredfirst, called M, is based on the finite ordinal sums of ukasiewiczt-norms. In addition to the usual connectives—the conjunction, the implication and the constant 0—we use a furtherunary connective interpreted by the function associating witheach truth value a the greatest -idempotent below a. M is aconservative extension of Basic Logic. The second logic, called M, is based on the finite ordinal sumsof the product t-norm on (0, 1]. Our connectives are in thiscase just the conjunction and the implication.     

The {omega}-Enumeration Degrees

In the present article we initiate the study of the partialordering of the -enumeration degrees. This ordering is a semi-latticewhich extends the semi-lattice of the enumeration degrees. Themain results include a jump inversion theorem, a density theoremfor the -enumeration degrees below the first jump of the leastdegree and the lack of minimal -enumeration degrees.     

A Jump Inversion Theorem for the Degree Spectra

In the present article, we continue the study of the propertiesof the spectra of structures as sets of degrees initiated in[11]. Here, we consider the relationships between the spectraand the jump spectra. Our first result is that every jump spectrumis also a spectrum. The main result sounds like a Jump inversiontheorem. Namely, we show that if a spectrum is contained inthe set of the jumps of the degrees in some spectrum then thereexists a spectrum such that and is equal to the set of thejumps of the degrees in .     

On a Problem of J. Paris

We give alternative proofs for results of T. Slaman and N. Thapen,concerning the problem whether or not | ₁ implies B ₁. Our proofsisolate structures that could disprove this implication.     

The Settling Time Reducibility Ordering and {Delta}Formula Sets

The settling time reducibility ordering gives an ordering oncomputably enumerable sets based on their enumerations. The<_st ordering is in fact an ordering on c.e. sets, since itis independent of the particular enumeration chosen. In thisarticle, we show that it is not possible to extend this orderingin an approximation-independent way to sets in general, or even to n-c.e. sets for anyfixed n 3.     

Embedding Alternating-time Temporal Logic in Strategic Logic of Agency

Seeing To It That ()logic is a logic of agency, proposed in the 1990s in the domainof philosophy of action. It is the logic of constructions ofthe form ‘agent a sees to it that ’. We believethat theory can contributeto the logical analysis of multiagent systems. To support thisclaim, we show that there is a close relationship with morerecent logics for multiagent systems. This work extends Broersenet al. (2006, Electron Notes Theor. Comput. Sci., Vol. 157,pp. 23–35) where we presented a translation from Pauly'sCoalition Logic to Chellas' logic. Here we focus on Alur, Henzinger and Kupferman's Alternating-timeTemporal Logic , andthe logic of the ‘fused’ _s[_scstit : _] operatorfor strategic ability, as described by Horty. After a briefpresentation of ATL and the definition of a discrete-time strategic framework slightly adaptedfrom Horty, we give a translation from ATL to the framework, and prove that it determines correctembedding.     

Epistemic Actions as Resources

We provide an algebraic semantics together with a sound andcomplete sequent calculus for information update due to epistemicactions. This semantics is flexible enough to accommodate incompleteas well as wrong information e.g. due to secrecy and deceit,as well as nested knowledge. We give a purely algebraic treatmentof the muddy children puzzle, which moreover extends to situationswhere the children are allowed to lie and cheat. Epistemic actions,that is, information exchanges between agents , are modeled as elements of a quantale. The quantale acts on an underlying Q-rightmodule of epistemic propositions and facts. The epistemic content is encoded by appearance maps,one pair and of (lax) morphisms for each agent , which preserve the module and quantale structurerespectively. By adjunction, they give rise to epistemic modalities,capturing the agents' knowledge on propositions and actions.The module action is epistemic update and gives rise to dynamicmodalities—cf. weakest precondition. This model subsumesthe crucial fragment of Baltag, Moss and Solecki's dynamic epistemiclogic, abstracting it in a constructive fashion while introducingresource-sensitive structure on the epistemic actions.     

Complexity Issues in Axiomatic Extensions of Lukasiewicz Logic

In this article, the computational complexity of all axiomaticextensions of ukasiewicz propositional logic and the arithmeticalcomplexity of both the general and standard semantics of theircorresponding predicate logics is determined.     

Isolation, Infima and Diamond Embeddings

In (1993, Annals of Pure and Applied Logic, 62, 207–263),Kaddah pointed out that there are two d.c.e. degrees a,b forminga minimal pair in the d.c.e. degrees, but not in the degrees. Kaddah's; result shows thatLachlan's; theorem, stating that the infima of two c.e. degreesin the c.e. degrees and in the degrees coincide, cannot be generalized to the d.c.e. degrees. In this article, we apply Kaddah's; idea to show that thereare two d.c.e. degrees c,d such that c cups d to 0', and capsd to 0 in the d.c.e. degrees, but not in the degrees. As a consequence, the diamond embedding{0,c,d,0'} is different from the one first constructed by Downeyin 1989 in [5]. To obtain this, we will construct c.e. degreesa,b, d.c.e. degrees c > a,d > b and a non-zero -c.e. degreee c,d such that (i) a,b form a minimal pair, (ii) a isolatesc, and (iii) b isolates d. From this, we can have that c,d forma minimal pair in the d.c.e. degrees, and Kaddah's; result followsimmediately. In our construction, we apply Kaddah's; originalidea to make e below both c and d. Our construction allows usto separate the minimal pair argument (ab = 0), the splittingof 0' (cd = 0'), and the non-minimal pair of c,d (in the degrees), into several parts, to avoiddirect conflicts that could be involved if only c,d and e areconstructed. We also point out that our construction allowsus to make a,b above (and hence c,d) high.     

Call-by-Value {lambda}-calculus and LJQ

LJQ is a focused sequent calculus for intuitionistic logic,with a simple restriction on the first premiss of the usualleft introduction rule for implication. In a previous paperwe discussed its history (going back to about 1950, or beyond)and presented its basic theory and some applications; here wediscuss in detail its relation to call-by-value reduction inlambda calculus, establishing a connection between LJQ and theCBV calculus _C of Moggi. In particular, we present an equationalcorrespondence between these two calculi forming a bijectionbetween the two sets of normal terms, and allowing reductionsin each to be simulated by reductions in the other.     

Axiomatizing the Monodic Fragment of

As we can show that the two-variable monadic fragment of thefull first-order extension of the propositional branching time logic is not recursively enumerable, we show in thisarticle that the monodic fragment of can be axiomatized.     

Undecidability in Some Structures Related to Computation Theory

We show that many of the so called discrete weak semilatticesconsidered earlier in a series of author's publications havehereditary undecidable first-order theories. Since such structuresappear naturally in some parts of computation theory, we obtainseveral new undecidability results. This applies e.g. to thestructures of complete numberings, of m-degrees of index setsand of the Wadge degrees of k-partitions in the Baire spaceand -algebraic domains. Whenever possible, we try to determinealso the exact degrees of undecidability of the theories underdiscussion.     

Contraction Based on Sentential Selection

The properties of full meet contraction are investigated, andit is shown to be a useful building-block in the constructionof composite contraction operators. This is followed by a detailedinvestigation of specified meet contraction, i.e. the operation÷ such that K ÷ p = K f(p), where is full meetcontraction and f is a function from sentences to sentences.A number of realistic examples of belief contraction are discussed,and it is shown how the properties of contraction differ accordingto how the sentence to be contracted is situated in the structureof the belief state. Some plausible properties of f are proposed,and it is shown how they correspond to properties of the contractionoperator.     

On Realization of -modality by Evidence Terms

We introduce a logic of evidence-based knowledge in which the evidence part is based on logicof proofs with negative checker . The later is obtained from the Logic of proofs by adding a new unary operation of negativechecker ‘?’ and the corresponding axiom. We defineKripke-style models for and prove the completeness with respect to this semantics. Wealso define the logic of justified knowledge for .     

On Representing Sentential Connectives of Lesniewski's Elementary Protothetic

After a brief presentation of Leniewski's notation for 1- and2-place sentential connectives of protothetic, the article discussesa method of extending this method to n 3-place sentential connectives.Such a method has been hinted at by Luschei, but in fact, nogeneral effective method of defining such functors has beenclearly and explicitly given. The purpose of this article isto provide such a method.     

Reference Constructions in the Single-conclusion Proof Logic

We propose an extension of the propositional proof logic languageby the second-order variables denoting the reference constructors(like ‘the formula which is proven by x’). The prooflogic in this weak second-order language is axiomatized viathe calculus _ref, the (Functional)Logic of Proofs with References. It is supplied with the formalarithmetical semantics: we prove that _ref is sound with respect to arithmetical interpretationsand is a conservative extension of propositional single-conclusionproof logic . Finally,we demonstrate how the language of _ref can be used as a scheme language for arithmetic and providethe corresponding proof conversion method.     

Undecidability in the Homomorphic Quasiorder of Finite Labelled Forests

We prove that the homomorphic quasiorder of finite k-labelledforests has a hereditary undecidable first-order theory fork 3, in contrast to the known decidability result for k = 2.We establish also hereditary undecidability (again for everyk 3) of first-order theories of two other relevant structures:the homomorphic quasiorder of finite k-labelled trees, and offinite k-labelled trees with a fixed label of the root element.Finally, all three first-order theories are shown to be computablyisomorphic to the first-order arithmetic.     

On Weakly Cancellative Fuzzy Logics

Starting from a decomposition result of monoidal t-norm-basedlogic (MTL)-chains as ordinal sums, we focus our attention ona particular kind of indecomposable semihoops, namely weaklycancellative semihoops. The weak cancellation property is provedto be the difference between cancellation and pseudocomplementation,so it gives a new axiomatization of product logic and MTL. Byadding this property, some new fuzzy logics (propositional andfirst-order) are defined and studied obtaining some resultsabout their (finite) strong standard completeness and otherlogical and algebraic properties.     

Generalized Strong Preservation by Abstract Interpretation

Standard abstract model checking relies on abstract Kripke structureswhich approximate concrete models by gluing together indistinguishablestates, namely by a partition of the concrete state space. Strongpreservation for a specification language amounts to the equivalence of concrete and abstractmodel checking of formulas in . We show how abstract interpretation can be used to designgeneric abstract models that allow to view standard abstractKripke structures as particular instances. Accordingly, strongpreservation is generalized to abstract interpretation-basedmodels and precisely related to the concept of completenessin abstract interpretation. The problem of minimally refiningan abstract model in order to make it strongly preserving forsome language can be formulatedas a minimal domain refinement in abstract interpretation inorder to get completeness w.r.t. the logical/temporal operatorsof . It turns out thatthis refined strongly preserving abstract model always existsand can be characterized as a greatest fixed point. As a consequence,some well-known behavioural equivalences, like bisimulation,simulation and stuttering, and their corresponding partitionrefinement algorithms can be elegantly characterized in abstractinterpretation as completeness properties and refinements.