Catalogue Search | MBRL
Are you sure you want to remove the book from the shelf?
{{itemTitle}}
29
result(s) for
"Baaz, Matthias"
Sort by:
Kurt Gödel and the foundations of mathematics : horizons of truth
\"This volume commemorates the life, work, and foundational views of Kurt Gödel (1906-1978), most famous for his hallmark works on the completeness of first-order logic, the incompleteness of number theory, and the consistency - with the other widely accepted axioms of set theory - of the axiom of choice and of the generalized continuum hypothesis. It explores current research, advances, and ideas for future directions not only in the foundations of mathematics and logic, but also in the fields of computer science, artificial intelligence, physics, cosmology, philosophy, theology, and the history of science. The discussion is supplemented by personal reflections from several scholars who knew Gödel personally, providing some interesting insights into his life. By putting his ideas and life's work into the context of current thinking and perceptions, this book will extend the impact of Gödel's fundamental work in mathematics, logic, philosophy, and other disciplines for future generations of researchers\"-- Provided by publisher.
BOOK
UNSOUND INFERENCES MAKE PROOFS SHORTER
We give examples of calculi that extend Gentzen’s sequent calculus LK by unsound quantifier inferences in such a way that (i) derivations lead only to true sequents, and (ii) proofs therein are nonelementarily shorter than LK-proofs.
Journal Article
Finite-valued Semantics for Canonical Labelled Calculi
We define a general family of
canonical labelled calculi
, of which many previously studied sequent and labelled calculi are particular instances. We then provide a uniform and modular method to obtain finite-valued semantics for every canonical labelled calculus by introducing the notion of
partial non-deterministic matrices
. The semantics is applied to provide simple
decidable
semantic criteria for two crucial syntactic properties of these calculi: (strong) analyticity and cut-admissibility. Finally, we demonstrate an application of this framework for a large family of paraconsistent logics.
Journal Article
Gentzen Calculi for the Existence Predicate
We introduce Gentzen calculi for intuitionistic logic extended with an existence predicate. Such a logic was first introduced by Dana Scott, who provided a proof system for it in Hilbert style. We prove that the Gentzen calculus has cut elimination in so far that all cuts can be restricted to very simple ones. Applications of this logic to Skolemization, truth value logics and linear frames are also discussed.
Journal Article
On the non-confluence of cut-elimination
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.
Journal Article
On the complexity of proof deskolemization
We consider the following problem: Given a proof of the Skolemization of a formula F, what is the length of the shortest proof of F? For the restriction of this question to cut-free proofs we prove corresponding exponential upper and lower bounds.
Journal Article
On Skolemization in constructive theories
In this paper a method for the replacement, in formulas, of strong quantifiers by functions is introduced that can be considered as an alternative to Skolemization in the setting of constructive theories. A constructive extension of intuitionistic predicate logic that captures the notions of preorder and existence is introduced and the method, orderization, is shown to be sound and complete with respect to this logic. This implies an analogue of Herbrand's theorem for intuitionistic logic. The orderization method is applied to the constructive theories of equality and groups.
Journal Article
Goedel logics: Prenex fragments
In this paper, we provide a complete classification for the first-order Goedel logics concerning the property that the formulas admit logically equivalent prenex normal forms. We show that the only first-order Goedel logics that admit such prenex forms are those with finite truth value sets since they allow all quantifier-shift rules and the logic \\(G_\\uparrow\\) with only one accumulation point at 1 in the infinite truth value set. In all the other cases, there are generally no logically equivalent prenex normal forms. We will also see that \\(G_\\uparrow\\) is the intersection of all finite first-order Goedel logics. The second part of this paper investigates the existence of effective equivalence between the validity of a formula and the validity of some prenex normal form. The existence of such a normal form is obvious for finite valued Goedel logic and \\(G_\\uparrow\\). Goedel logics with an uncountable truth value set admit the prenex normal forms if and only if every surrounding of 0 is uncountable or 0 is an isolated point. Otherwise, uncountable Goedel logics are not recursively enumerable, however, the prenex fragment is always recursively enumerable. Therefore, there is no effective translation between the valid formula and the valid prenex normal form. However, the existence of effectively constructible validity equivalent prenex forms for the countable case is still up for debate.
Paper
Labeled Calculi and Finite-Valued Logics
A general class of labeled sequent calculi is investigated, and necessary and sufficient conditions are given for when such a calculus is sound and complete for a finite-valued logic if the labels are interpreted as sets of truth values (sets-as-signs). Furthermore, it is shown that any finite-valued logic can be given an axiomatization by such a labeled calculus using arbitrary \"systems of signs,\" i.e., of sets of truth values, as labels. The number of labels needed is logarithmic in the number of truth values, and it is shown that this bound is tight.
Journal Article