Beweisbarkeitslogik für Rosser-Sätze

Lade...
Vorschaubild
Dateien
CvBdipl.pdf
CvBdipl.pdfGröße: 914.01 KBDownloads: 193
Datum
1998
Herausgeber:innen
Kontakt
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
DOI (zitierfähiger Link)
ArXiv-ID
Internationale Patentnummer
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz
Gesperrt bis
Titel in einer weiteren Sprache
Provability Logic for Rosser-Sentences
Forschungsvorhaben
Organisationseinheiten
Zeitschriftenheft
Publikationstyp
Masterarbeit/Diplomarbeit
Publikationsstatus
Published
Erschienen in
Zusammenfassung

Kurt Gödel zeigte 1931 in seiner klassischen Arbeit 'Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I', dass die wahren Sätze der Mathematik nicht als die Theoreme irgendeines formalen Systems erhalten werden können. Zum Beweis dieses Satzes konstruierte Gödel arithmetische Aussagen, die von sich selbst behaupten: 'Ich bin (im betrachteten System) nicht beweisbar.' Solche Gödel-Sätze sind dann tatsächlich nicht beweisbar. Somit sind sie aber wahr und belegen daher die Unvollständigkeit des betrachteten formalen Systems.

John Barkley Rosser verbesserte 1936 in 'Extensions of Some Theorems of Gödel and Church' Gödels Ergebnis, wobei er statt Gödel-Sätzen so genannte Rosser-Sätze betrachtete, die ungefähr besagen: 'Wenn ich beweisbar bin, dann auch meine Negation.'

Nun kann man Formeln der modalen Aussagenlogik in die Sprache der Arithmetik 'übersetzen', indem man Aussagevariablen durch arithmetische Aussagen ersetzt und den Notwendigkeitsoperator als formalisiertes Beweisbarkeitsprädikat liest.
1976 bewies Robert M. Solovay ('Provability Interpretations of Modal Logic'), dass das modallogische System GL gerade diejenigen Formeln liefert, die unter allen solchen Übersetzungen beweisbar sind. Dadurch wird es möglich, das formalisierte Beweisbarkeitsprädikat mit modallogischen Mitteln zu untersuchen, d.h. Beweisbarkeitslogik zu treiben.

1979 machten Solovay und D. Guaspari in 'Rosser Sentences' auch Rosser-Phänomene zugänglich für modallogische Methoden.

In der vorliegenden Arbeit werden diese Resultate von Guaspari und Solovay, zusammen mit den nötigen prädikaten- und modallogischen Grundlagen, ausgeführt und etwas verallgemeinert. Ich habe versucht, den Gegenstand so darzustellen, dass er auch für interessierte LeserInnen mit Grundkenntnissen in Mathematischer Logik leicht zugänglich wird. Die Kapitel I, II und IV können für sich genommen auch als Einführung in die Beweisbarkeitslogik dienen.

Zusammenfassung in einer weiteren Sprache

In his classical paper 'Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I' (1931), Kurt Gödel showed that the true sentences of mathematics could not be obtained as the theorems of any formal system. To prove this, Gödel constructed arithmetical sentences which state about themselves: 'I am not provable (in the system considered).' These Gödel sentences then are in fact not provable. But thus they are true, and therefore exemplify the system's incompleteness.

John Barkley Rosser, in his 'Extensions of Some Theorems of Gödel and Church' (1936), improved Gödel's result by using, instead of Gödel sentences, so-called Rosser sentences, which roughly say: 'If I am provable then my negation is provable as well.'

Now, formulae of propositional modal logic can be 'translated' into the language of arithmetic by replacing propositional variables with arithmetical sentences and interpreting the necessity operator as a formalized provability predicate. In 1976, Robert M. Solovay demonstrated (in 'Provability Interpretations of Modal Logic') that the modal system GL yielded exactly those formulae which are provable under all such translations. Thus it is possible to investigate the formalized provability predicate by modal-logical means, i.e., to engage in provability logic.

In their 1979 'Rosser Sentences', Solovay and D. Guaspari made Rosser-like phenomena accessible to modal-logical methods, too.

In this work, Guaspari's and Solovay's results, together with the necessary fundamentals from predicate and modal logic, are developed and slightly generalized. I tried to present the subject so as to be easily accessible even for readers with only basic knowledge in mathematical logic. Chapters I, II and IV by themselves can serve as an introduction to provability logic.

Fachgebiet (DDC)
510 Mathematik
Schlagwörter
Beweisbarkeitslogik, arithmetische Vollständigkeit, Solovay, Robert M., Rosser, John Barkley, Guaspari, D., provability logic, arithmetical completeness, GL (modal system), R (modal system)
Konferenz
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690BÜLOW, Christopher von, 1998. Beweisbarkeitslogik für Rosser-Sätze [Master thesis]
BibTex
@mastersthesis{Bulow1998Bewei-528,
  year={1998},
  title={Beweisbarkeitslogik für Rosser-Sätze},
  author={Bülow, Christopher von}
}
RDF
<rdf:RDF
    xmlns:dcterms="http://purl.org/dc/terms/"
    xmlns:dc="http://purl.org/dc/elements/1.1/"
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:bibo="http://purl.org/ontology/bibo/"
    xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
    xmlns:foaf="http://xmlns.com/foaf/0.1/"
    xmlns:void="http://rdfs.org/ns/void#"
    xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > 
  <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/528">
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-22T17:44:56Z</dc:date>
    <dc:creator>Bülow, Christopher von</dc:creator>
    <dcterms:abstract xml:lang="deu">Kurt Gödel zeigte 1931 in seiner klassischen Arbeit 'Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I', dass die wahren Sätze der Mathematik nicht als die Theoreme irgendeines formalen Systems erhalten werden können. Zum Beweis dieses Satzes konstruierte Gödel arithmetische Aussagen, die von sich selbst behaupten: 'Ich bin (im betrachteten System) nicht beweisbar.' Solche Gödel-Sätze sind dann tatsächlich nicht beweisbar. Somit sind sie aber wahr und belegen daher die Unvollständigkeit des betrachteten formalen Systems.&lt;br /&gt;&lt;br /&gt;John Barkley Rosser verbesserte 1936 in 'Extensions of Some Theorems of Gödel and Church' Gödels Ergebnis, wobei er statt Gödel-Sätzen so genannte Rosser-Sätze betrachtete, die ungefähr besagen: 'Wenn ich beweisbar bin, dann auch meine Negation.'&lt;br /&gt;&lt;br /&gt;Nun kann man Formeln der modalen Aussagenlogik in die Sprache der Arithmetik 'übersetzen', indem man Aussagevariablen durch arithmetische Aussagen ersetzt und den Notwendigkeitsoperator als formalisiertes Beweisbarkeitsprädikat liest.&lt;br /&gt;1976 bewies Robert M. Solovay ('Provability Interpretations of Modal Logic'), dass das modallogische System GL gerade diejenigen Formeln liefert, die unter allen solchen Übersetzungen beweisbar sind. Dadurch wird es möglich, das formalisierte Beweisbarkeitsprädikat mit modallogischen Mitteln zu untersuchen, d.h. Beweisbarkeitslogik zu treiben.&lt;br /&gt;&lt;br /&gt;1979 machten Solovay und D. Guaspari in 'Rosser Sentences' auch Rosser-Phänomene zugänglich für modallogische Methoden.&lt;br /&gt;&lt;br /&gt;In der vorliegenden Arbeit werden diese Resultate von Guaspari und Solovay, zusammen mit den nötigen prädikaten- und modallogischen Grundlagen, ausgeführt und etwas verallgemeinert. Ich habe versucht, den Gegenstand so darzustellen, dass er auch für interessierte LeserInnen mit Grundkenntnissen in Mathematischer Logik leicht zugänglich wird. Die Kapitel I, II und IV können für sich genommen auch als Einführung in die Beweisbarkeitslogik dienen.</dcterms:abstract>
    <dc:format>application/pdf</dc:format>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/39"/>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/528/1/CvBdipl.pdf"/>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-22T17:44:56Z</dcterms:available>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/528"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/39"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/528/1/CvBdipl.pdf"/>
    <dc:contributor>Bülow, Christopher von</dc:contributor>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:language>deu</dc:language>
    <dcterms:issued>1998</dcterms:issued>
    <dcterms:alternative>Provability Logic for Rosser-Sentences</dcterms:alternative>
    <dcterms:title>Beweisbarkeitslogik für Rosser-Sätze</dcterms:title>
    <dc:rights>terms-of-use</dc:rights>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
  </rdf:Description>
</rdf:RDF>
Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Kontakt
URL der Originalveröffentl.
Prüfdatum der URL
Prüfungsdatum der Dissertation
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Begutachtet
Diese Publikation teilen