Do you want to publish a course? Click here

On the logical strengths of partial solutions to mathematical problems

145   0   0.0 ( 0 )
 Added by Ludovic Patey
 Publication date 2014
  fields
and research's language is English




Ask ChatGPT about the research

We use the framework of reverse mathematics to address the question of, given a mathematical problem, whether or not it is easier to find an infinite partial solution than it is to find a complete solution. Following Flood, we say that a Ramsey-type variant of a problem is the problem with the same instances but whose solutions are the infinite partial solutions to the original problem. We study Ramsey-type variants of problems related to Konigs lemma, such as restrictions of Konigs lemma, Boolean satisfiability problems, and graph coloring problems. We find that sometimes the Ramsey-type variant of a problem is strictly easier than the original problem (as Flood showed with weak Konigs lemma) and that sometimes the Ramsey-type variant of a problem is equivalent to the original problem. We show that the Ramsey-type variant of weak Konigs lemma is robust in the sense of Montalban: it is equivalent to several perturbations of itself. We also clarify the relationship between Ramsey-type weak Konigs lemma and algorithmic randomness by showing that Ramsey-type weak weak Konigs lemma is equivalent to the problem of finding diagonally non-recursive functions and that these problems are strictly easier than Ramsey-type weak Konigs lemma. This answers a question of Flood.



rate research

Read More

213 - Jonas Reitz 2016
This paper explores how a pluralist view can arise in a natural way out of the day-to-day practice of modern set theory. By contrast, the widely accepted orthodox view is that there is an ultimate universe of sets $V$, and it is in this universe that mathematics takes place. From this view, the purpose of set theory is learning the truth about $V$. It has become apparent, however, that the phenomenon of independence - those questions left unresolved by the axioms - holds a central place in the investigation. This paper introduces the notion of independence, explores the primary tool (soundness) for establishing independence results, and shows how a plurality of models arises through the investigation of this phenomenon. Building on a familiar example from Euclidean geometry, a template for independence proofs is established. Applying this template in the domain of set theory leads to a consideration of forcing, the tool par excellence for constructing universes of sets. Fifty years of forcing has resulted in a profusion of universes exhibiting a wide variety of characteristics - a multiverse of set theories. Direct study of this multiverse presents technical challenges due to its second-order nature. Nonetheless, there are certain nice local neighborhoods of the multiverse that are amenable to first-order analysis, and emph{set-theoretic geology} studies just such a neighborhood, the collection of grounds of a given universe $V$ of set theory. I will explore some of the properties of this collection, touching on major concepts, open questions, and recent developments.
70 - Arnold W. Miller 1996
This is a set of 288 questions written for a Moore-style course in Mathematical Logic. I have used these (or some variation) four times in a beginning graduate course. Topics covered are: propositional logic axioms of ZFC wellorderings and equivalents of AC ordinal and cardinal arithmetic first order logic, and the compactness theorem Lowenheim-Skolem theorems Turing machines, Churchs Thesis completeness theorem and first incompleteness theorem undecidable theories second incompleteness theorem
Finite-domain constraint satisfaction problems are either solvable by Datalog, or not even expressible in fixed-point logic with counting. The border between the two regimes coincides with an important dichotomy in universal algebra; in particular, the border can be described by a strong height-one Maltsev condition. For infinite-domain CSPs, the situation is more complicated even if the template structure of the CSP is model-theoretically tame. We prove that there is no Maltsev condition that characterizes Datalog already for the CSPs of first-order reducts of (Q;<); such CSPs are called temporal CSPs and are of fundamental importance in infinite-domain constraint satisfaction. Our main result is a complete classification of temporal CSPs that can be expressed in one of the following logical formalisms: Datalog, fixed-point logic (with or without counting), or fixed-point logic with the Boolean rank operator. The classification shows that many of the equivalent conditions in the finite fail to capture expressibility in Datalog or fixed-point logic already for temporal CSPs.
In this paper, we will discuss three semantically distinct scope assignment strategies: traditional movement strategy, polyadic approach, and continuation-based approach. As a generalized quantifier on a set X is an element of C(X), the value of continuation monad C on X, in all three approaches QPs are interpreted as C-computations. The main goal of this paper is to relate the three strategies to the computational machinery connected to the monad C (strength and derived operations). As will be shown, both the polyadic approach and the continuation-based approach make heavy use of monad constructs. In the traditional movement strategy, monad constructs are not used but we still need them to explain how the three strategies are related and what can be expected of them wrt handling scopal ambiguities in simple sentences.
129 - Bernd R. Schuh 2009
For formulas F of propositional calculus I introduce a metavariable MF and show how it can be used to define an algorithm for testing satisfiability. MF is a formula which is true/false under all possible truth assignments iff F is satisfiable/unsatisfiable. In this sense MF is a metavariable with the meaning F is SAT. For constructing MF a group of transformations of the basic variables ai is used which corresponds to flipping literals to their negation. The whole procedure corresponds to branching algorithms where a formula is split with respect to the truth values of its variables, one by one. Each branching step corresponds to an approximation to the metatheorem which doubles the chance to find a satisfying truth assignment but also doubles the length of the formulas to be tested, in principle. Simplifications arise by additional length reductions. I also discuss the notion of logical primes and show that each formula can be written as a uniquely defined product of such prime factors. Satisfying truth assignments can be found by determining the missing primes in the factorization of a formula.
comments
Fetching comments Fetching comments
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا