Gödel Logics: Propositional Quantifiers and Concurrency
Gödel Logics: Propositional Quantifiers and Concurrency
Disciplines
Computer Sciences (30%); Mathematics (70%)
Keywords
-
Gödel logics,
Propositional quantifiers,
Analytic Calculi,
Cantor-Bendixon rank,
Proofs-as-programs
Gödel logics have been introduced by Gödel in 1933 to investigate intuitionistic logic. These logics naturally arise in a number of different areas within logic, mathematics and computer science. In particular, Gödel logics are closely related to fuzzy logic. By choosing subsets of the real unit interval [0, 1] as the underlying set of truth-values, many different Gödel logics have been defined. Propositional Gödel logics are well understood: Any infinite set of truth-values characterizes the same set of tautologies. When Gödel logic is extended beyond pure propositional logic, however, the situation is more complex. More precisely, one can consider two different forms of quantification: first-order quantifiers (universal and existential quantification over object domains) and propositional or fuzzy quantifiers (universal and existential quantification over propositions). First-order Gödel logics have been extensively investigated in the FWF Project "First-order Gödel Logic" (and continue to be part of the EC Marie Curie fellowship "Proof Theory of First-order Fuzzy Logic"). The research program proposed is intended to focus on propositional quantifiers which are essential for the understanding of quantifiers, their expressability and the relations to concurrent computation. The most important goals of this investigation are, in short: - A complete characterization of quantified propositional Gödel logics in various aspects. In particular we are interested in their expressive power and classification according to topological properties of the set of truth-values. - The development of extensions of first-order Gödel logics (especially the one based on [0,1]) to include propositional quantifiers. This will allow a general construction of provably equivalent prenex normal forms for arbitrary formulas, as in the case of classical logic. - Suitable interpretations of derivations in various formalizations of first-order Gödel logics (with and without propositional quantifiers) as concurrent computations.
The project had the following main targets: (1) A complete characterization of quantified propositional Gödel logics in various aspects; in particular their expressive power and classification according to topological properties of the set of truth-values. (2) The development of extensions of first-order Gödel logics (in particular the one based on the real interval [0,1]) in order to include propositional quantifiers. (3) Suitable interpretations of derivations in various formalizations of first-order Gödel logics as concurrent computations. The aims described above were met as follows. For the first aim, a complete characterization of quantified propositional Gödel logics was obtained, extending the analysis of quantified propositional Gödel logics corresponding to Kripke frames of type omega. The method of classification is based on the construction of the correspondence of Gödel logics with linear Kripke frames (this correspondence being fully established for first- order Gödel logics by Preining and Beckmann). The second aim was given a negative solution as a consequence of the result that all infinite-valued first-order Gödel logics are not recursively enumerable if propositional quantifiers are added. For the third target a shift of emphasis led to the consideration of parallel dialogue games to represent concurrency in Gödel logics. In the course of the project two other main results were achieved: (1) the proof that there are only countably many Gödel logics, and (2) the full proof-theoretic analysis of first-order MTL (the logic of left-continuous t-norms): as a syntactic and semantic subsystem of standard first-order Gödel logic. The first result is interesting because under almost all circumstances there are uncountably many intermediate logics. The importance of the second result comes from the fact that first-order MTL is one of the few fuzzy logics complete with respect to its intended semantics.
- Technische UniversitÀt Wien - 100%
- Hajek Petr, Czech Academy of Science - Czechia
- Michel Parigot, Universite de Paris - France
- Arnon Avron, Tel Aviv University - Israel
- Franco Montagna, Universita degli Studi di Siena - Italy
- Daniele Mundici, University of Florence - Italy
- Gaisi Takeuti, The University of Tsukuba - Japan
Research Output
- 12 Citations
- 2 Publications
-
2006
Title Completeness of a Hypersequent Calculus for Some First-order Gödel Logics with Delta DOI 10.1109/ismvl.2006.16 Type Conference Proceeding Abstract Author Baaz M Pages 9-14 -
2003
Title Characterization of the Axiomatizable Prenex Fragments of First-Order Gödel Logics DOI 10.1109/ismvl.2003.1201403 Type Conference Proceeding Abstract Author Baaz M Pages 175-180 Link Publication