
Authors:
George TOURLAKIS and Francisco KIBEDI
Title:A Modal Extension of First Order Classical Logic, Part II
Pages:110
File:bibtex
Abstract ( + )
We define the semantics of the modal predicate logic introduced in Part I and prove its soundness and strong completeness with respect to appropriate structures. These semantical tools allow us to give a simple proof that the main conservation requirement articulated in Part I, Section 1, is met as it follows directly from Theorem 5.1 below. Section numbering is consecutive to that of Part I.

Authors:
Katsumi SASAKI and Shigeo OHAMA
Title:A Sequent System of the Logic R^{} for Rosser Sentences
Pages:1121
File:bibtex
Abstract ( + )
To discuss Rosser sentences, Guaspari and Solovay axiomatized modal logics R^{}, R and R^{ω}, each of which satisfies a kind of arithmetic completeness theorem. Among these three logics, R^{} is the most preliminary one and provability of the other logics can be described by the provability of R^{}. Here we introduce a sequent system for R^{} with a kind of subformula property.

Authors:
Alexej P. PYNKO
Title:Sequential Calculi for Manyvalued Logics with Equality Determinant
Pages:2332
File:bibtex
Abstract ( + )
We propose a general method of constructing sequential calculi with cut elimination property for propositional finitelyvalued logics with equality determinant. We then prove the nonalgebraizability of the consequence operations of cutfree versions of such sequential calculi.

Authors:
F.A.DORIA and N.C.A.da COSTA
Title:On Set Theory as a Foundation for Computer Science
Pages:3340
File:bibtex
Abstract ( + )
We show how to axiomatize computer science within ZFC in a reasonably natural way, and discuss two examples of interesting properties of recursive functions which are intuitively true but lead to undecidable sentences within that axiom system.

Authors:
Szymon FRANKOWSKI
Title:Formalization of a Plausible Inference
Pages:4152
File:bibtex
Abstract ( + )
The key intuition behind plausibility in the sense of Ajdukiewicz is that it admits reasonings wherein the degree of strength of the conclusion (i.e. the conviction it is true) is smaller then that of the premises. In consequence in the formal description of plausible inference, the standard notions of consequence and rule of inference cannot be countenanced as entirely suitable. Accordingly, for a formal description of plausible inference, the notions of rule of inference and consequence adequate for the deductive case are not fully appropriate. The main difference between the deductive and the plausible inferences lies in the fact that the condition:
if X  α^{1},..., X  α^{n} and {α^{1},...,α^{n}}  α, then X  α
holds for the former but is dispensable for the latter. In terms of the operations on the set of formulas, this means that the condition "C(C(X)) is a subset of C(X)" may not hold for a proper plausible consequence relation. Nothwithstanding, nothing prevents us from accepting other Tarski conditions, the notion of plausible consequence being a generalization of Tarskian consequence operation. On the other hand, the notion of pconsequence operation turns out to be closely related to the socalled quasiconsequence (qconsequence) operation considered by Malinowski. Single matrices for the operations of both types contain two sets of designated values: one of possible values (degrees of truth) for the premisses, the other for the conclusion. In a matrix determining a pconsequence operation, the set of possible values for a conclusion is included

Authors:
Andrei KOUZNETSOV
Title:Deduction Chains and DClike Decision Procedure for Guarded Logic
Pages:5365
File:bibtex
Abstract ( + )
The notion of Deduction Chain (DC) was suggested by K.Schutte to prove the completeness of first order logic (FOL). There is a question whether it is possible to provide the decision procedure for the guarded fragment of FOL (GF) on the basis of DCrules. We propose here the decision procedure, or DCL algorithm, for the GF of FOL which rules are close to the ones of DC. DCL algorithm can be viewed as a "mirrow" of the tableau algorithm with the use of the so called blocking technique.