Eine Termlogik mit Auswahloperator
- PDF / 2,095,641 Bytes
- 46 Pages / 439.37 x 666.142 pts Page_size
- 112 Downloads / 224 Views
Hans Hermes
Eine Termlogik mit Auswahloperator
6
123
Lecture Notes in Mathematics An informal se ries of special lectures, seminars and reports on mathematical topics Edited by A. Dold, Heidelberg and B. Eckmann, Zürich
6 Hans Hermes Universität Münster Institut für mathematische Logik und Grundlagenforschung
Eine Termlogik mit Auswah loperator
1965
Springer-Verlag Berlin Heidelberg GmbH
Schrift: Fräulein T. Hessling
ISBN 978-3-540-36203-6 (eBook) ISBN 978-3-540-04899-2 DOI 10.1007/978-3-540-36203-6 All rights, espedally that of translation inta foreign languages, reserved. It 15 also forbidden to reproduce this book, either whole or in part, by photomechanical means (photostat, microfilm and/or microcard) or by other procedure without written permission from Springer Verlag.
© by Springer-Verlag Berlin Heidelberg 1965.
U!Sprilnglich e!Schienen bei Springer-VerIag Berlin· Heidelberg 1965 Library of Congress Catalog Card Number 65-17845.
Title No. 7326
Inhaltsübersicht
1.
Einlei tung .""""""""""""""""""""""""""""""""""""""""""""""
2.
Prädikatenlogik mit Auswahloperator ••••••••••••••.••••••••••••••••
4
3.
Termlogik ••..•••••••••••••••.•..••.••
7
4.
Zusammenhang zwischen der Prädikatenlogik und der Termlogik •••••••
10
5.
Rang, freies Vorkommen einer Variablen, Substitution ••••••••••••••
15
6.
Ein Kalkül für die Termlogik •••••••••
00.0.........................
17
7.
Gleichwettigkeit von ~ und
8.
Gbersicht über den Vollständigkeitsbeweis •••••••••••••••••••••••••
23
Termisomorphismen
• • • • • • • • • • • • • • • 00 • • • • • • 0 • • • • • • • • • • 0 0 0 0 • • • • 0011
24
~~ •••••••••••••••••••••••••••••••••••••••••••
26
~
10. Maximalisierung von
t
0
••••••••••••••••••••••••••• 0
•••••••••••••••••••••••••••••••
11. Verallgemeinerte Substitution ••••••••••••••••• 12q Erfüllbarkeit von
0" " "" " "" "
~* •....•.....•....•
00.0..
21
0 •••••••••••••••••• 0
28
0 •••••••••••••••••••••••••• 0
35
Li tera tur ................................................................................................
40
Verzeichnis der Symbol e .................................................................... ..
41
.............................................................................................
42
Sachverzeichnis
-1_
Der Kennzeichnungsoperator wurde im Rahmen der formalen Logik zuerst von Whitehead und Russell
[6] behandelt.
In Hilbert-Bernays [4J
wird statt des Kennzeichnungsoperators allgemeiner ein Auswahloperator t
zu Grunde gelegt, und ein Eliminationstheorem für diesen Operator
bewiesen. Man verglo auch Rosser [5J. Man kann bekanntlich die gewöhnliche Prädikatenlogik der ersten Stufe zunächst auf semantischer Grundlage aufbauen und dann ein
Regel~
system angeben, für welches die Korrektheit (soundness) und die
Voll-
ständigkeit (completeness) bewiesen werden kann. Es wäre erwünscht, auch die Prädikatenlogik mit Auswahloperator in dieser Weise aufzubauen. In Nr. 2 wird eine derartige Logik aufgebaut. Es stellt sich nun heraus (Nr.3), dass
Data Loading...
