Until recently, First-Order Temporal Logic (FOTL) has been only
partially understood. While it is well known that the full logic has
no finite axiomatisation, a more detailed analysis of fragments of the
logic was not previously available. However, a breakthrough by
Hodkinson et.al., identifying a finitely axiomatisable fragment,
termed the monodic fragment, has led to improved understanding
of FOTL. Yet, in order to utilise these theoretical advances, it is
important to have appropriate proof techniques for this monodic
fragment.
In this talk, we modify and extend the clausal temporal resolution
technique, originally developed for propositional temporal logics, to
enable its use in such monodic fragments. We develop a specific normal
form for monodic formulae in FOTL, and provide a complete
resolution calculus for formulae in this form. Not only is this
clausal resolution technique useful as a practical proof technique for
certain monodic classes, but the use of this approach provides us with
increased understanding of the monodic fragment. In particular, we
here show how several features of monodic FOTL can be established
as corollaries of the completeness result for the clausal temporal
resolution method. These include definitions of new decidable monodic
classes, simplification of existing monodic classes by reductions,
and completeness of clausal temporal resolution in the case of monodic
logics with expanding domains, a case with much significance in both
theory and practice.
The article presents the complete first-order theory of the complex field expanded with a Liouville Function H. These functions are characterized by a very fast decrease of Taylor coefficients. The theory is a first example of a stable theory that admits an analytical model.
All existing proofs of strong normalization in the presence of disjunction, existence and permutative conversions are much more complicated than similar proofs for the negative fragment. Recently W. Tait published a partial normalization proof for a stronger language containing realizing terms. Using this apparatus and some recent ideas of the authors we provide a simple strong normalization proof for a standard formulation of second order natural deduction with disjunction, existential quantification, and permutative conversions.
In this talk, we will explain how methods from higher recursion theory can be used to prove independence results for first-order Peano Arithmetic (PA). The talk will consist primarily of a detailed discussion of such an independence proof. The proof in question leads to an extension of a previous independence result of ours, answering a question asked by Harrington and Knight. This new result has been applied recently by D'Aquino and Knight to prove a result about the metamathematics of a weak fragment of PA. We will also discuss briefly another application of this kind of independence proof, concerning consistency sentences for PA. This second proof answers a question asked by Goncharov, Gaifman, and others, though unlike the first case, here the answer to the question was already known. Lastly, we will remark on the philosophical significance of this type of proof: namely, that the use of higher recursion theory in proving arithmetic independence results might seem to be an instance of impurity.
In their 1963 book, "The Mathematics of Metamathematics", Rasiowa and Sikorski present an approach to completeness theorems of various logics using algebraic methods. This idea can of course be traced back to Boole, but it was revived and generalized by Stone and Tarski in the 1930s; however, the most direct influence on their work came from their well-known colleague, Andrzej Mostowski, after WW II. Mostowski's interpretation of quantification can as well be given for intutionistic as classical logic. The talk will briefly review the history and content of these ideas and raise the question of why there was at that time no generalization made to higher-order logic and set theory. Entirely new light on this kind of algebraic semantics has more recently been thrown by the development of topos theory in category theory. Reasons for pursuing this generalization will also be discussed.
A Frege system for a given propositional logic is a standard
formulation with axioms and modes ponens plus maybe other schematic
rules. A basic bootstrapping result for investigating NP and co-NP
completeness (due to S. Cook and R. Reckow) is polynomial equivalence
of every two Frege systems for classical logic. The proof used in an
essential way the fact that every classically admissible schematic
rule A/B is derivable: A->B is a tautology. The equivalence of
admissibility and derivability fails for the intuitionistic logic that
bears the same relation to PSPACE as classical logic to NP.
It turned out possible however to simulate polynomially (in a Frege
system) every intuitionistically admissible schematic rule [stated
with standard connectives &,v,~,->]. Therefore any two intuitionistic
Frege
systems polynomially simulate each other.
This is a joint work with A. Kozhevnikov (Steklov Institute of
Mathematics, St. Petersburg)