Formalisieren und Beweisen: Logik für Informatiker

گریگوری بیتسون - زیست‌شناس، انسان‌شناس، روان‌پزشک، نظریه‌پرداز سیستم‌ها - در مقدمه کتاب ذهن و طبیعت خود داستانی را بیان می‌کند: مردی این سوال را در رایانه‌اش وارد می‌کند: "آیا هرگز مانند یک انسان فکر خواهید کرد؟ محاسبه کنید آن را بررسی کنید. !\" کامپیوتر محاسبه می کند و محاسبه می کند و در نهایت خروجی می دهد: داستانی برایم پیش می آید. داستان این کتاب درباره مردم است. رالف-دتلف کوتچه هنگامی که در سال 1982 به همراه پیتر پادوویتز، سیمون پریبنو و آندریاس شولزه برای برگزاری دوره منطق برای دانشمندان کامپیوتر به من کمک کرد، «اما هر بخش را با یک مثال شروع کنید»، پیشنهاد کرد. «پرسش‌ها و تکالیف بهتر از اصطلاحات و جملات کار را تحریک می‌کنند.» به همین دلیل است که هر بخش از این کتاب با داستانی آغاز می‌شود که به عنوان ماده‌ی کار عمل می‌کند: مقدمه‌ای با مشکل میمون با موز، منطق گزاره‌ای با logelei پرتاب توپ، منطق مرتبه اول باز با مثال معمار و منطق کامل مرتبه اول با هندسه اقلیدس. بنابراین، هر بخش با وظایف و سوالاتی که برای درک ضروری است، به پایان می رسد. به همین دلیل است که وقتی آن را ورق می‌زنید، دلیل بسیار کمی می‌بینید: من ترجیح می‌دهم به جای شروع با قضیه، یک برهان را از یک سؤال توسعه دهم و نتیجه را به صورت یک قضیه فرموله کنم. بنابراین، موضوعات کتاب، حوزه های رسمی سازی و فهم، فعالیت ها و نه منطق و علوم کامپیوتری است. من در کتاب عمدتاً به مباحث پایه کلاسیک منطق ریاضی می پردازم: نتیجه گیری منطقی، اشتقاق، کامل بودن، نظریه منطقی، سیستم بدیهیات. با این حال، من علاقه ای به ارائه این اصطلاحات و ویژگی های آنها ندارم.

Gregory Bateson -Biologe, Anthropologe, Psychiater, Systemtheoretiker -erzählt in der Ein­ l leitung zu seinem Buch Geist und Natur eine Geschichte: Ein Mann gibt in seinen Computer die Frage ein: "Wirst Du jemals denken wie ein Mensch? Rechne mal nach!" Der Computer rechnet und rechnet und gibt schließlich aus: Dabei fallt mir eine Geschichte ein. Die Geschichte dieses Buches handelt von Menschen. "Fangt doch jeden Abschnitt mit einem Beispiel an", schlug Ralf-Detlef Kutsche vor, als er mir 1982 zusammen mit Peter Padawitz, Simone Pribbenow und Andreas Schulze half, die Lehrveranstaltung Logik für Informatiker durchzuführen. "Fragen und Aufgaben regen besser zum Arbeiten an als Begriffe und Sätze. " Deswegen beginnt jeder Teil dieses Buches mit einer Geschichte, die als Arbeitsmaterial dient: Die Einführung mit dem Problem des Affen mit der Banane, die Aussagenlogik mit der Ballwurf­ logelei, die Offene Prädikatenlogik mit dem Architektenbeispiel und die volle Prädikatenlogik mit der Geometrie Euklids. Deswegen endet jeder Abschnitt mit Aufgaben und Fragen, die wesentlich fürs Verstehen sind. Deswegen sieht man beim Blättern so wenig Beweise: Ich ent­ wickle einen Beweis lieber aus einer Fragestellung und formuliere das Ergebnis als Satz, statt mit dem Satz zu beginnen. Deswegen sind die Themen des Buches Formalisieren und Verstehen, Tätigkeiten, und nicht Logik und Informatik, Gebiete. Ich behandle in dem Buch im wesentlichen die klassischen Grundthemen der mathematischen Logik: logische Folgerung, Ableitung, Vollständigkeit, logische Theorie, Axiomensystem. Es geht mir aber nicht darum, diese Begriffe und ihre Eigenschaften darzustellen.