
Authors:
George TOURLAKIS
Title:A basic formal equational predicate logic. Part II
Pages:7587
File:bibtex
Abstract ( + )
We continue our exploration of the ``Basic Formal Equational Predicate Logic'' of Part I. Section numbering is consecutive to that of Part I. We show that a strong ``nocapture'' Leibniz, and a weak ``fullcapture'' version are derived rules (both access the interior of quantifier scopes). We derive general rules MON (monotonicity) and AMON (antimonotonicity) that are ``as strong as possible'' for our logic. Finally, we show that our logic is sound and complete. The bibliography at the end applies to Part II only.

Authors:
Paulo A.S.VELOSO
Title:On the power of ultrafilter logic
Pages:8997
File:bibtex
Abstract ( + )
We examine the expressive and deductive powers of ultrafilter logic, an extension of classical firstorder logic by a generalised quantifier, whose intended interpretation is ``almost all". We characterise a simple class of formulae from which the quantifier can be eliminated, and establish that ultrafilter logic has more expressive power than classical firstorder logic. We also show that, in the absence of almost universal information, the only almost universal sentences that can be derived are the universal ones.

Authors:
David MILLER
Title:Extremal consequence operations
Pages:99107
File:bibtex
Abstract ( + )
Dzik gives a direct proof of the axiom of choice from the generalized Lindenbaum extension theorem LET. Inspection of Dzik's proof shows that its premise Let assumes only that LET holds for those consequence operations, here called extremal, for which Cn(Y)=Y or Cn(Y)=S. A direct proof, not using the axiom of choice, is given for the conditional Let > LET.

Authors:
Teresa BIEGANSKA and Katarzyna HALKOWSKA
Title:Minimal generic of externally compatible varieties
Pages:107114
File:bibtex
Abstract ( + )
[Abstract]

Authors:
Dale JACQUETTE
Title:An internal determinacy metatheorem for Lukasiewicz's Aussagenkalkuls
Pages:115124
File:bibtex
Abstract ( + )
An internal determinacy metatheorem is proved for Lukasiewicz's threevalued propositional calculus. The metatheorem establishes that no sentences of the logic are logically undetermined in truth value. The result is extended to Kleene's threevalued logic and related systems, but the significance of the metatheorem is shown by the fact that it does not apply indiscriminately to any and all threevalued logics. Implications of the metatheorem for five philosophical topics are indicated.

Authors:
Branden FITELSON and Larry WOS
Title:Axiomatic proofs through automated reasoning
Pages:125136
File:bibtex
Abstract ( + )
A search of the seminal papers and significant books devoted to the study of various types of logic reveals that many proofs are missing. Indeed, if one seeks an axiomatic proof (of the type that Hilbert enjoyed) relying solely on, say, condensed detachment, in many cases one finds that none is offered by the literature. In part prompted by this discovery, we embarked on an intense study designed to find the missing proofs. In this article, we list many of our successes and discuss the methodologies used to obtain them. We also show how OTTER has proved valuable in finding proofs that avoid both the use of perhapsthoughttobeindispensable lemmas and the use of an unexpected class of terms. Because crucial to our attack was the use of the automated reasoning program OTTER, we include an intuitive introduction to the subject. OTTER may well prove useful as an assistant in the research of others.