24 found
Sort by:
  1. Oliver Fasching & Matthias Baaz (forthcoming). Monotone Operators on Gödel Logic. Archive for Mathematical Logic.
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  2. Matthias Baaz, Stefan Hetzl & Daniel Weller (2012). On the Complexity of Proof Deskolemization. Journal of Symbolic Logic 77 (2):669-686.
    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.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  3. Matthias Baaz (ed.) (2011). Kurt Gödel and the Foundations of Mathematics: Horizons of Truth. Cambridge University Press.
    Machine generated contents note: Part I. Historical Context - Gödel's Contributions and Accomplishments: 1. The impact of Gödel's incompleteness theorems on mathematics Angus Macintyre; 2. Logical hygiene, foundations, and abstractions: diversity among aspects and options Georg Kreisel; 3. The reception of Gödel's 1931 incompletabilty theorems by mathematicians, and some logicians, to the early 1960s Ivor Grattan-Guinness; 4. 'Dozent Gödel will not lecture' Karl Sigmund; 5. Gödel's thesis: an appreciation Juliette C. Kennedy; 6. Lieber Herr Bernays!, Lieber Herr Gödel! Gödel on (...)
    Direct download  
     
    My bibliography  
     
    Export citation  
  4. Matthias Baaz & Stefan Hetzl (2011). On the Non-Confluence of Cut-Elimination. Journal of Symbolic Logic 76 (1):313 - 340.
    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.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  5. Matthias Baaz (2009). Foreword. Annals of Pure and Applied Logic 157 (2-3):63.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  6. Matthias Baaz & Oliver Fasching (2009). Note on Witnessed Gödel Logics with Delta. Annals of Pure and Applied Logic 161 (2):121-127.
    Witnessed Gödel logics are based on the interpretation of () by minimum instead of supremum . Witnessed Gödel logics appear for many practical purposes more suited than usual Gödel logics as the occurrence of proper infima/suprema is practically irrelevant. In this note we characterize witnessed Gödel logics with absoluteness operator w.r.t. witnessed Gödel logics using a uniform translation.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  7. Matthias Baaz & Rosalie Iemhoff (2008). On Skolemization in Constructive Theories. Journal of Symbolic Logic 73 (3):969-998.
    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 (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  8. Matthias Baaz & Piotr Wojtylak (2008). Generalizing Proofs in Monadic Languages. Annals of Pure and Applied Logic 154 (2):71-138.
    This paper develops a proof theory for logical forms of proofs in the case of monadic languages. Among the consequences are different kinds of generalization of proofs in various schematic proof systems. The results use suitable relations between logical properties of partial proof data and algebraic properties of corresponding sets of linear diophantine equations.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  9. Richard Zach, Matthias Baaz & Norbert Preining (2007). First-Order Gödel Logics. Annals of Pure and Applied Logic 147 (1):23-47.
    First-order Gödel logics are a family of finite- or infinite-valued logics where the sets of truth values V are closed subsets of [0,1] containing both 0 and 1. Different such sets V in general determine different Gödel logics GV (sets of those formulas which evaluate to 1 in every interpretation into V). It is shown that GV is axiomatizable iff V is finite, V is uncountable with 0 isolated in V, or every neighborhood of 0 in V is uncountable. Complete (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  10. Matthias Baaz & Rosalie Iemhoff (2006). Gentzen Calculi for the Existence Predicate. Studia Logica 82 (1):7 - 23.
    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.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  11. Matthias Baaz & Rosalie Iemhoff (2006). The Skolemization of Existential Quantifiers in Intuitionistic Logic. Annals of Pure and Applied Logic 142 (1):269-295.
    In this paper an alternative Skolemization method is introduced that, for a large class of formulas, is sound and complete with respect to intuitionistic logic. This class extends the class of formulas for which standard Skolemization is sound and complete and includes all formulas in which all strong quantifiers are existential. The method makes use of an existence predicate first introduced by Dana Scott.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  12. Matthias Baaz & Georg Moser (2006). Herbrand's Theorem and Term Induction. Archive for Mathematical Logic 45 (4):447-503.
    We study the formal first order system TIND in the standard language of Gentzen's LK . TIND extends LK by the purely logical rule of term-induction, that is a restricted induction principle, deriving numerals instead of arbitrary terms. This rule may be conceived as the logical image of full induction.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  13. Matthias Baaz (2005). Controlling Witnesses. Annals of Pure and Applied Logic 136 (1-2):22-29.
    This paper presents a translation which allows one to describe constructive provability within classical first-order logic.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  14. Matthias Baaz, Petr Hájek, Franco Montagna & Helmut Veith (2001). Complexity of T-Tautologies. Annals of Pure and Applied Logic 113 (1-3):3-11.
    A t-tautology is a propositional formula which is a tautology in all fuzzy logics defined by continuous triangular norms. In this paper we show that the problem of recognizing t-tautologies is coNP complete, and thus decidable.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  15. Matthias Baaz & Alexander Leitsch (1999). Cut Normal Forms and Proof Complexity. Annals of Pure and Applied Logic 97 (1-3):127-177.
    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 normal form and (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  16. Matthias Baaz & Helmut Veith (1999). Interpolation in Fuzzy Logic. Archive for Mathematical Logic 38 (7):461-489.
    We investigate interpolation properties of many-valued propositional logics related to continuous t-norms. In case of failure of interpolation, we characterize the minimal interpolating extensions of the languages. For finite-valued logics, we count the number of interpolating extensions by Fibonacci sequences.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  17. Matthias Baaz, Christian G. Fermüller, Gernot Salzer & Richard Zach (1998). Labeled Calculi and Finite-Valued Logics. Studia Logica 61 (1):7-33.
    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 (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  18. Matthias Baaz, Petr Hájek, David Švejda & Jan Krajíček (1998). Embedding Logics Into Product Logic. Studia Logica 61 (1):35-47.
    We construct a faithful interpretation of ukasiewicz's logic in product logic (both propositional and predicate). Using known facts it follows that the product predicate logic is not recursively axiomatizable.We prove a completeness theorem for product logic extended by a unary connective of Baaz [1]. We show that Gödel's logic is a sublogic of this extended product logic.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  19. Matthias Baaz & Richard Zach (1998). Note on Generalizing Theorems in Algebraically Closed Fields. Archive for Mathematical Logic 37 (5-6):297-307.
    The generalization properties of algebraically closed fields $ACF_p$ of characteristic $p > 0$ and $ACF_0$ of characteristic 0 are investigated in the sequent calculus with blocks of quantifiers. It is shown that $ACF_p$ admits finite term bases, and $ACF_0$ admits term bases with primality constraints. From these results the analogs of Kreisel's Conjecture for these theories follow: If for some $k$ , $A(1 + \cdots + 1)$ ( $n$ 1's) is provable in $k$ steps, then $(\forall x)A(x)$ is provable.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  20. Norbert Brunner, Karl Svozil & Matthias Baaz (1996). The Axiom of Choice in Quantum Theory. Mathematical Logic Quarterly 42 (1):319-340.
    We construct peculiar Hilbert spaces from counterexamples to the axiom of choice. We identify the intrinsically effective Hamiltonians with those observables of quantum theory which may coexist with such spaces. Here a self adjoint operator is intrinsically effective if and only if the Schrödinger equation of its generated semigroup is soluble by means of eigenfunction series expansions.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  21. Sanjeev Arora, Matthias Baaz, Lenore Blum, Patrick Dehornoy, Solomon Feferman, Moti Gitik, Erich Grädel, Yuri Gurevich, Serge Grigorieff & David Harel (1995). Clermont-Ferrand, France, July 21–30, 1994. Bulletin of Symbolic Logic 1 (2).
    Direct download  
     
    My bibliography  
     
    Export citation  
  22. Matthias Baaz & Richard Zach (1995). Generalizing Theorems in Real Closed Fields. Annals of Pure and Applied Logic 75 (1-2):3-23.
    Jan Krajíček posed the following problem: Is there is a generalization result in the theory of real closed fields of the form: If A is provable in length k for all n ϵ ω , then A is provable? It is argued that the answer to this question depends on the particular formulation of the “theory of real closed fields.” Four distinct formulations are investigated with respect to their generalization behavior. It is shown that there is a positive answer to (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  23. Matthias Baaz & Alexander Leitsch (1992). Complexity of Resolution Proofs and Function Introduction. Annals of Pure and Applied Logic 57 (3):181-215.
    The length of resolution proofs is investigated, relative to the model-theoretic measure of Herband complexity. A concept of resolution deduction is introduced which is somewhat more general than the classical concepts. It is shown that proof complexity is exponential in terms of Herband complexity and that this bound is tight. The concept of R-deduction is extended to FR-deduction, where, besides resolution, a function introduction rule is allowed. As an example, consider the clause P Q: conclude P) Q, where a, f (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  24. Matthias Baaz (1986). Kripke-Type Semantics for da Costa's Paraconsistent Logic ${\Rm C}_\Omega$. Notre Dame Journal of Formal Logic 27 (4):523-527.