
Authors:
George TOURLAKIS and Francisco KIBEDI
Title:A Modal Extension of First Order Classical Logic, Part I
Pages:165177
File:bibtex
Abstract ( + )
Extension of First Order Classical Logic, Part I We formalize a fragment of the metatheory of classical first order logic by adding a new connective, the modal L, whose intended interpretation is the (classical) metalogical predicate "is a theorem" (). We then illustrate how to employ this modal extension of classical logic to write equational proofs of classical theorems, and prove (in Part II) its completeness and soundness with respect to Kripke models. We also prove that the extension meets our objective: For any classical formulae A and B, we can prove LA > LB modally iff we can prove A  B classically.

Authors:
Janusz KACZMAREK
Title:Positive and Negative Properties. A Logical Interpretation
Pages:179189
File:bibtex
Abstract ( + )
In the paper we construct a simple sentential logic (L_{BK}). L_{BK} has internal and external strata, which yield a double characterization of the connectives. This leads to the correspondence of L_{BK} to Bochvar's and Kleene's logics. The connectives of the internal level correspond to the connectives of Bochvar's internal logic and of Kleene's weak logic, while the connectives of the external level correspond to those of Bochvar's external logic and of Kleene's strong logic. The ontological interpretation shows that the former represent the socalled connectives "de re", the latter the connectives "de dicto".

Authors:
Christian J.RENTERIA, Edward Hermann HAEUSLER, Paulo A.S.VELOSO
Title:NUL: Natural Deduction for Ultrafilter Logic
Pages:191199
File:bibtex
Abstract ( + )
Ultrafilter logic is an extension of first order logic that uses a new quantifier to express a meaning of "almost all", that is, to express sentences like: "Almost all elements of our universe have the property P". Such a logic had previously been presented only in an axiomatic version. We give here a natural deduction version, which is correct, complete and normalizable.

Authors:
Toshimasa MATSUMOTO
Title:Time Complexity of Proof search Procedure for K4
Pages:201211
File:bibtex
Abstract ( + )
In this paper, we will give the time complexity of the proof search procedure given by a sequent system for K4. Here, time complexity is regarded as the total number of applications of rules in all proof figures of any given formula. Here, the time complexity means the total number of applications of rules in the proof search in the worst case for a given formula. We estimate the time complexity by using a certain order which guarantees termination of the proof search procedure. We show the strict value of the time complexity of the proof search procedure for k4 with the order.

Authors:
M.I. GOLOVANOV, Vladimir V.RYBAKOV, E.M. YURASOVA
Title:A Necessary Condition for Rules to be Admissible in Temporal TomorrowLogic
Pages:213220
File:bibtex
Abstract ( + )
We provide a necessary condition for inference rules to be admissible in the temporal TomorrowLogic. Our conjecture is that this condition must be also sufficient.