



LEADER 
03174nmm a2200289 u 4500 
001 
EB000678011 
003 
EBX01000000000000000531093 
005 
00000000000000.0 
007 
cr 
008 
140122  eng 
020 


a 9783642867187

100 
1 

a Smullyan, Raymond R.

245 
0 
0 
a FirstOrder Logic
h Elektronische Ressource
c by Raymond R. Smullyan

250 


a 1st ed. 1968

260 


a Berlin, Heidelberg
b Springer Berlin Heidelberg
c 1968, 1968

300 


a XII, 160 p
b online resource

505 
0 

a I. Propositional Logic from the Viewpoint of Analytic Tableaux  I. Preliminaries  II. Analytic Tableaux  III. Compactness  II. FirstOrder Logic  IV. FirstOrder Logic. Preliminaries  V. FirstOrder Analytic Tableaux  VI. A Unifying Principle  VII. The Fundamental Theorem of Quantification Theory  VIII. Axiom Systems for Quantification Theory  IX. Magic Sets  X. Analytic versus Synthetic Consistency Properties  III. Further Topics in FirstOrder Logic  XI. Gentzen Systems  XII. Elimination Theorems  XIII. Prenex Tableaux  XIV. More on Gentzen Systems  XV. Craig’s Interpolation Lemma and Beth’s Definability Theorem  XVI. Symmetric Completeness Theorems  XVII. Systems of Linear Reasoning  References

653 


a Mathematical logic

653 


a Mathematical Logic and Foundations

710 
2 

a SpringerLink (Online service)

041 
0 
7 
a eng
2 ISO 6392

989 


b SBA
a Springer Book Archives 2004

490 
0 

a Ergebnisse der Mathematik und ihrer Grenzgebiete. 2. Folge, A Series of Modern Surveys in Mathematics

856 


u https://doi.org/10.1007/9783642867187?nosfx=y
x Verlag
3 Volltext

082 
0 

a 511.3

520 


a Except for this preface, this study is completely selfcontained. It is intended to serve both as an introduction to Quantification Theory and as an exposition of new results and techniques in "analytic" or "cutfree" methods. We use the term "analytic" to apply to any proof procedure which obeys the subformula principle (we think of such a procedure as "analysing" the formula into its successive components). Gentzen cutfree systems are perhaps the best known example of ana lytic proof procedures. Natural deduction systems, though not usually analytic, can be made so (as we demonstrated in [3]). In this study, we emphasize the tableau point of view, since we are struck by its simplicity and mathematical elegance. Chapter I is completely introductory. We begin with preliminary material on trees (necessary for the tableau method), and then treat the basic syntactic and semantic fundamentals of propositional logic. We use the term "Boolean valuation" to mean any assignment of truth values to all formulas which satisfies the usual truthtable conditions for the logical connectives. Given an assignment of truthvalues to all propositional variables, the truthvalues of all other formulas under this assignment is usually defined by an inductive procedure. We indicate in Chapter I how this inductive definition can be made explicitto this end we find useful the notion of a formation tree (which we discuss earlier)
