Generalized quantifiers and well orderings.
Hercules and Hydra
Hercules and Hydra, a game on rooted finite trees
Hercules versus Hidden Hydra Helper
L. Kirby and J. Paris introduced the Hercules and Hydra game on rooted trees as a natural example of an undecidable statement in Peano Arithmetic. One can show that Hercules has a “short” strategy (he wins in a primitively recursive number of moves) and also a “long” strategy (the finiteness of the game cannot be proved in Peano Arithmetic). We investigate the conflict of the “short” and “long” intentions (a problem suggested by J. Nešetřil). After each move of Hercules (trying to kill Hydra fast)...
Indécidabilité de la théorie des anneaux de séries formelles à plusieurs indéterminées
Karp-Miller trees for a branching extension of VASS.
Kleine unentscheidbare Klassen der Prädikatenlogik mit Identität und Funktionszeichen.
L'axiomatisation de la syntaxe et le second theorem de Gödel
Logics for stable and unstable mereological relations
In this paper we present logics about stable and unstable versions of several well-known relations from mereology: part-of, overlap and underlap. An intuitive semantics is given for the stable and unstable relations, describing them as dynamic counterparts of the base mereological relations. Stable relations are described as ones that always hold, while unstable relations hold sometimes. A set of first-order sentences is provided to serve as axioms for the stable and unstable relations, and representation...
Metamathematical discussion of some affine geometries
Model-interpretability into trees and applications.
Model-theoretic properties of cause-and-effect structures
Natural limitations of decisions procedures for arithmetic with bounded quantifiers.
Nice local global fields. IV.
Normal forms in partial modal logic
A "partial" generalization of Fine's definition [Fin] of normal forms in normal minimal modal logic is given. This means quick access to complete axiomatizations and decidability proofs for partial modal logic [Thi].
Normalisation of the theory of Cartesian closed categories and conservativity of extensions of
Normalisation of the Theory T of Cartesian Closed Categories and Conservativity of Extensions T[x] of T
Using an inductive definition of normal terms of the theory of Cartesian Closed Categories with a given graph of distinguished morphisms, we give a reduction free proof of the decidability of this theory. This inductive definition enables us to show via functional completeness that extensions of such a theory by new constants (“indeterminates”) are conservative.
Notes on a class of tiling problems
Objects in relational database schemes with functional, inclusion, and exclusion dependencies