Department of Philosophy
(with Gerhard Widmer and Robert Trappl.) Art/ificial Intelligence. A Short Bibliography on AI and the Arts.ÖFAI Report TR-90-14, Austrian Research Institute for Artificial Intelligence, 1990.
(with Matthias Baaz.) "Algorithmic Structuring of Cut-free Proofs."
In Egon Borger, et al., eds., Computer Science Logic: 6th Workshop, CSL '92, San Miniato, Italy,
September 28-October 2, 1992: Selected Papers, pp.
29-42. Lecture Notes in Computer Science, 702. Berlin & New York: Springer, 1993.
Abstract:
We investigate the problem of algorithmic structuring of proofs in the sequent
calculi LK and LKB (LK where blocks of quantifiers can be introduced in one step),
where we distinguish between linear proofs and proofs in tree form.
In this framework, structuring coincides with the introduction of cuts into a proof. The algorithmic solvability of this problem can be reduced to the question of k/l-compressibility: "Given a proof of P |- L of length k, and l < k: Is there is a proof of P |- L of length < l?" When restricted to proofs with universal or existential cuts, this problem is shown to be
1. undecidable for linear or tree-like LK-proofs,
2. undecidable for linear LKB-proofs, and
3. decidable for tree-like LKB-proofs.
(1) corresponds to the undecidability of second order unification, (2) to the undecidability of semi-unification, and (3) to the decidability of a subclass of semi-unification.
(with Matthias Baaz and Christian G. Fermüller.)
"Dual Systems of Sequents and Tableaux." Bulletin of the EATCS (1993), 51:192-197.
Workshop on Tableau-based Deduction, Marseille, 1993.
Proof Theory of Finite-Valued Logics.
Diploma Thesis, Technische Universität Wien, Vienna, 1993.
Abstract:
Several people have, since the 1950's, proposed ways to generalize proof theoretic formalisms
(sequent calculus, natural deduction, resolution) from the classical to the many-valued case.
One particular method for systematically obtaining calculi for all finite-valued logics was
invented independently by several researchers, with slight variations in design and
presentation. The main aim of this report is to develop the proof theory of finite-valued
first order logics in a general way, and to present some of the more important results in
this area. This report is actually a template, from which all results can be specialized to
particular logics.
The main results of this report are: the use of signed formula expressions and partial normal forms to provide a unifying framework in which clause translation calculi, sequent calculi, natural deduction, and also tableaux can be represented; bounds for partial normal forms for general and induced quantifiers; and negative resolution. The cut-elimination theorems extend previous results, and the midsequent theorem, natural deduction systems for many-valued logics as well as results on approximation of axiomatizable propositional logics by many-valued logics are all new.
(with Matthias Baaz, Christian G. Fermüller, and Arie Ovrutcki.) "MULTILOG: A System for Axiomatizing Many-Valued Logics." In Andrei Voronkov, ed., Logic Programming and Automated Reasoning: 4th International Conference LPAR '93, St. Petersburg, Russia, July 13-20, 1993: Proceedings , pp. 345-347. Lecture Notes in Computer Science. Lecture Notes in Artificial Intelligence, 698. Berlin & New York: Springer, 1993.
(with Matthias Baaz and Christian G. Fermüller.) "Systematic Construction of
Natural Deduction Systems for Many-Valued Logics." In The Twenty-Third International
Symposium on Multiple-Valued Logic, May 24-27, 1993, Sacramento, California, pp. 208-213.
Los Alamitos, Calif.: IEEE Computer Society Press; New York: Institute of Electrical and Electronics
Engineers, 1993.
Sponsored by IEEE Computer Society, IEEE Computer
Society Technical Committee on Multiple-Valued Logic, Center for Image Processing and
Integrated Computing at University of California, Davis.
(with Matthias Baaz.) "Approximating Propositional Calculi by Finite-Valued Logics."
In Proceedings / The Twenty-Fourth International Symposium on Multiple-Valued Logic,
May 25-27, 1994, Boston, Massachusetts,
pp. 257-263. Los Alamitos, Calif.: IEEE Computer Science Press, 1994.
Sponsored by IEEE Computer Society, IEEE Computer Society
Technical Committee on Multiple-Valued Logic, University of
Massachusetts at Boston.
Abstract:
The problem of approximating a propositional calculus is to find many-valued logics
which are sound for the calculus (i.e., all theorems of the calculus are tautologies)
with as few tautologies as possible. This has potential applications for representing
(computationally complex) logics used in AI by (computationally easy) many-valued logics.
It is investigated how far this method can be carried using (1) one or
(2) an infinite sequence of many-valued logics.
It is shown that the optimal candidate matrices for (1) can be computed from the calculus.
(with Matthias Baaz and Christian G. Fermüller.) "Elimination of Cuts in First Order Many-Valued Logics."
Journal of Information Processing and Cybernetics (1994), 29:333-355.
Abstract:
A uniform construction for sequent calculi for finite-valued first-order logics with
distribution quantifiers is exhibited. Completeness, cut-elimination and midsequent theorems
are established. As an application, an analog of Herbrand's theorem for the four-valued
knowledge-representation logic of Belnap and Ginsberg is presented. It is indicated how this
theorem can be used for reasoning about knowledge bases with incomplete and inconsistent
information.
(with Petr Hájek.) Review of Leonard Bolc and Piotr Borowik's Many-Valued Logics: 1. Theoretical Foundations. Journal of Applied Non-Classical Logics (1994), 4:215-220.
(with Matthias Baaz.) "Short Proofs of Tautologies Using the Schema of Equivalence."
In Egon Borger, Yuri Gurevich, and Karl Meinke, eds., Computer Science Logic.
7th Workshop, CSL '93, Swansea, United Kingdom, September 13-17, 1993: Selected Papers,
pp. 33-35. Lecture Notes in Computer Science, 832. Berlin & New York: Springer, 1994. QA76.9.M35 W67 1993 Bar
Abstract:
It is shown how the schema of equivalence can be used to obtain short proofs of
tautologies A, where the depth of proofs is linear in the number of variables in A.
(with Matthias Baaz.) "Generalizing Theorems in Real Closed Fields."
Annals of Pure and Applied Logic (September 12, 1995), 75(1-2):3-23.
Abstract:
Jan Krajicek posed the following problem: Is there is a generalization result in the theory of
real closed fields of the form: If A(1 + ... + 1) (n occurrences of 1) is provable
in length k for all n = 0, 1, 2, ..., then (x)A(x) 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 Krajicek's question for
(1) the axiom system RCF of Artin-Schreier with Gentzen's LK as underlying logical calculus,
(2) RCF with the variant LKB of LK allowing introduction of several quantifiers of the same
type in one step, (3) LKB and the first-order schemata corresponding to Dedekind cuts and the
supremum principle. A negative answer is given for (4) any system containing the schema of
extensionality.
(with Matthias Baaz.) "Generalizing Theorems in Real Closed Fields." [Abstract] Bulletin of Symbolic Logic (1995), 1:361.
(with Matthias Baaz and Christian G. Fermüller.) "Proof Theory of Finite-Valued Logics." [Abstract] Bulletin of Symbolic Logic (1995), 1:221-222.
(with Matthias Baaz and Alexander Leitsch.) "Completeness of a First-Order Temporal Logic of
with Time-Gaps." Theoretical Computer Science
(June 10, 1996), 160(1-2):241-270.
Abstract:
The first-order temporal logics with [] and o of time structures isomorphic to omega
(discrete linear time) and trees of omega-segments (linear time with branching gaps) and
some of its fragments are compared: The first is not recursively axiomatizable.
For the second, a cut-free complete sequent calculus is given, and from this,
a resolution system is derived by the method of Maslov.
(with Matthias Baaz and Alexander Leitsch.) "Incompleteness of an Infinite-Valued
First-Order Gödel Logic and Some Temporal Logics of Programs." In Hans Kleine Buning, ed.,
Computer Science Logic: 9th International Workshop, CSL '95, Annual
Conference of the EACSL, Paderborn, Germany, September 22-29, 1995: Selected Papers, pp. 1-15.
Lecture Notes in Computer Science, 1092. CSL'95 was the fourth to be held as the Annual Conference of the
EACSL. Berlin & New York: Springer, 1996. QA76.9.M35 W67 1995 Bar
Abstract:
It is shown that the infinite-valued first-order Gödel logic G0 based on the set of
truth values {0; 1/k : k = 1, 2, 3, ...} is not r.e. The logic G0 is the same as that
obtained from the Kripke semantics for first-order intuitionistic logic with constant
domains and where the order structure of the model is linear.
From this, the unaxiomatizability of Kröger's temporal logic of programs
(even of the fragment without the nexttime operator) and of the authors' temporal logic of
linear discrete time with gaps follows.
(with Matthias Baaz.) "Compact Propositional Gödel Logics." In
1998 28th International Symposium on Multiple-Valued Logic: Proceedings: May 27-29, 1998,
Fukuoka, Japan, , pp. 108-113. Los Alamitos, Calif.: IEEE Computer Society Press, 1998.
Sponsored by IEEE Computer Society Technical Committee
on Multiple-Valued Logic, Japan Research Group on Multiple-Valued Logic.
Abstract:
Entailment in propositional Gödel logics can be defined in a natural way.
While all infinite sets of truth values yield the same sets of tautologies,
the entailment relations differ. It is shown that there is a rich structure of
infinite-valued Gödel logics, only one of which is compact.
It is also shown that the compact infinite-valued Gödel logic is the only one which
interpolates, and the only one with an r.e. entailment relation.
(with Matthias Baaz, Christian G. Fermüller, and Gernot Salzer.)
"Labeled Calculi and Finite-Valued Logics." Studia Logica (1998), 61(1):7-33.
Abstract:
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
finitevalued logic if the labels are interpreted as sets of truth values (setsassigns).
Furthermore, it is shown that any finitevalued 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.
(with Matthias Baaz.) "Note on Generalizing Theorems in Algebraically Closed Fields."
Archive for Mathematical Logic (July 1997), 37(5-6):297-307.
Abstract:
The generalization properties of algebraically closed fields ACFp of characteristic p > 0 and
ACF0 of characteristic 0 are investigated in the sequent calculus with blocks of quantifiers.
It is shown that ACFp admits finite term bases, and ACF0 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 + ... + 1) (n 1's) is provable in k steps, then (x)A(x) is provable.
"Numbers and Functions in Finitism." Taiwanese Journal for Philosophy and History
of Science (1998), 10:33-60.
Logic Colloquium '95 (Haifa).
Abstract:
David Hilbert's finitistic standpoint is a conception of elementary number theory designed to
answer the intuitionist doubts regarding the security and certainty of mathematics.
Hilbert was unfortunately not exact in delineating what that viewpoint was,
and Hilbert himself changed his usage of the term through the 1920s and 30s.
The purpose of this paper is to outline what the main problems are in understanding
Hilbert and Bernays on this issue, based on some publications by them which have so far
received little attention, and on a number of philosophical reconstructions and criticisms
of the viewpoint (in particular, by Hand, Kitcher, Parsons, and Tait).
"Completeness before Post: Bernays, Hilbert, and the Development of Propositional Logic."
Bulletin of Symbolic Logic (1999), 5(3):331-336.
Abstract:
Some of the most important developments of symbolic logic took place in the 1920s.
Foremost among them are the distinction between syntax and semantics and the formulation of
questions of completeness and decidability of logical systems. David Hilbert and his students
played a very important part in these developments. Their contributions can be traced to
unpublished lecture notes and other manuscripts by Hilbert and Bernays dating to the period
1917-1923. The aim of this paper is to describe these results, focussing primarily on
propositional logic, and to put them in their historical context. It is argued that
truthvalue semantics, syntactic ("Post") and semantic completeness, decidability, and other
results were first obtained by Hilbert and Bernays in 1918, and that Bernays's role in their
discovery and the subsequent development of mathematical logic is much greater than has so
far been acknowledged.
(with Matthias Baaz and Agata Ciabattoni.) "Quantified Propositional Gödel Logics."
In Andrei Voronkov and Michel Parigot, eds., Logic Programming and Automated Reasoning:
7th International Conference, LPAR 2000. Proceedings, pp. 240-256. Berlin: Springer, 2000.
Abstract:
It is shown that G^, the quantified propositional Gödel logic based on the truth-values
set V^ = {1 - 1/n : n = 1, 2, . . .} u {1}, is decidable.
This result is obtained by reduction to Büchi's theory S1S.
An alternative proof based on elimination of quantifiers is also given,
which yields both an axiomatization and a characterization of G^ as the intersection of all
finite-valued quantified propositional Gödel logics.
(with Matthias Baaz.) "Hypersequents and the Proof Theory of Intuitionistic Fuzzy Logic."
In Peter G. Clote and Helmut Schwichtenberg, eds.,
Computer Science Logic. 14th International Workshop, CSL 2000. Fischbachau, Germany,
August 21-26, 2000. Proceedings, pp. 187-201.
Berlin: Springer, 2000.
Abstract:
Takeuti and Titani have introduced and investigated a logic they called intuitionistic
fuzzy logic. This logic is characterized as the first-order Gödel logic based on the truth
value set [0, 1]. The logic is known to be axiomatizable, but no deduction system amenable to
proof-theoretic, and hence, computational treatment, has been known.
Such a system is presented here, based on previous work on hypersequent calculi for
propositional Gödel logics by Avron.
It is shown that the system is sound and complete, and allows cut-elimination.
A question by Takano regarding the eliminability of the Takeuti-Titani density rule is
answered affirmatively.
"Hilbert's Finitism: Historical and Philosophical Perspectives."
Ph.D. Dissertation, University of California, Berkeley.
Abstract:
In putting forth one of the most influential positions in the philosophy of mathematics,
David Hilbert set out to provide a foundation for mathematics by first formalizing it
entirely, and then showing the formalization to be consistent on "finitistic" grounds.
I focus on two particular aspects of this enterprise: (1) the instrumentalist view ascribed to
Hilbert, and (2) the concept of finitism that he proposed. Hilbert's instrumentalism is
usually thought to entail that only the "real," finitistic part of mathematics has meaning and
the "ideal" part (the formalized part that involves assumptions of infinity) is a meaningless
game of signs. I criticize this interpretation and offer a more nuanced "methodological''
instrumentalism, both as an interpretation of Hilbert and as a view that may be contrasted with
other recent instrumentalist proposals in the philosophy of mathematics, such as those of
Field and Papineau.
Hilbert's concept of finitism is an integral part of his program. I am interested in two central issues in this connection. The first is this: What is the notion of intuition that Hilbert thought to be at work in our grasp of finite objects (signs, formulas)? Charles Parsons has written a series of papers on what he calls "rational intuition," which he takes to be at work when we speak of intuition in mathematics. I argue that the although Parsons is correct in ascribing to Hilbert a view similar to his own, the area of finitistic knowledge which such a notion of intuition can underwrite is broader than he supposes.
The second issue I deal with is the strength of finitist reasoning. In addition to Parson's position, I consider two proposed explications of finitism, those of Kreisel and Tait. I argue that Kreisel's proposal is more in tune with the characterization of finitism given by Hilbert himself, but that only Tait's has a chance of serving the purpose Hilbert intended for the finitist standpoint.
I preface these philosophical studies with an historical investigation of Hilbert's Program. Making extensive use of unpublished archival sources, I first trace the development of central metalogical notions such as completeness and decidability. One of my findings is that a completeness proof for propositional logic was found by Hilbert and his assistant Paul Bernays already in 1917-18, two years before Emil Post's. I also describe the formal mathematical theories developed by Hilbert and his collaborators and the partial results they obtained in the area of consistency proofs. Specifically, I give a detailed analysis of Ackermann's consistency proofs for formal systems based on the epsilon-calculus.