Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
A Natural Interpretation of Classical Proofs
Stockholms universitet, Naturvetenskapliga fakulteten, Matematiska institutionen.
2006 (Engelska)Doktorsavhandling, monografi (Övrigt vetenskapligt)
Abstract [en]

In this thesis we use the syntactic-semantic method of constructive type theory to give meaning to classical logic, in particular Gentzen's LK.

We interpret a derivation of a classical sequent as a derivation of a contradiction from the assumptions that the antecedent formulas are true and that the succedent formulas are false, where the concepts of truth and falsity are taken to conform to the corresponding constructive concepts, using function types to encode falsity. This representation brings LK to a manageable form that allows us to split the succedent rules into parts. In this way, every succedent rule gives rise to a natural deduction style introduction rule. These introduction rules, taken together with the antecedent rules adapted to natural deduction, yield a natural deduction calculus whose subsequent interpretation in constructive type theory gives meaning to classical logic.

The Gentzen-Prawitz inversion principle holds for the introduction and elimination rules of the natural deduction calculus and allows for a corresponding notion of convertibility. We take the introduction rules to determine the meanings of the logical constants of classical logic and use the induced type-theoretic elimination rules to interpret the elimination rules of the natural deduction calculus. This produces an interpretation injective with respect to convertibility, contrary to an analogous translation into intuitionistic predicate logic.

From the interpretation in constructive type theory and the interpretation of cut by explicit substitution, we derive a full precision contraction relation for a natural deduction version of LK. We use a term notation to formalize the contraction relation and the corresponding cut-elimination procedure.

The interpretation can be read as a Brouwer-Heyting-Kolmogorov (BHK) semantics that justifies classical logic. The BHK semantics utilizes a notion of classical proof and a corresponding notion of classical truth akin to Kolmogorov's notion of pseudotruth. We also consider a second BHK semantics, more closely connected with Kolmogorov's double-negation translation.

The first interpretation reinterprets the consequence relation while keeping the constructive interpretation of truth, whereas the second interpretation reinterprets the notion of truth while keeping the constructive interpretation of the consequence relation. The first and second interpretations act on derivations in much the same way as Plotkin's call-by-value and call-by-name continuation-passing-style translations, respectively.

We conclude that classical logic can be given a constructive semantics by laying down introduction rules for the classical logical constants. This semantics constitutes a proof interpretation of classical logic.

Ort, förlag, år, upplaga, sidor
Stockholm: Matematiska institutionen , 2006. , s. 100
Nyckelord [en]
Brouwer-Heyting-Kolmogorov, classical logic, constructive type theory, constructive semantics, proof interpretation, double-negation, continuation-passing-style, natural deduction, sequent calculus, cut elimination, explicit substitution
Nationell ämneskategori
Algebra och logik
Identifikatorer
URN: urn:nbn:se:su:diva-913ISBN: 91-7155-206-5 (tryckt)OAI: oai:DiVA.org:su-913DiVA, id: diva2:200630
Disputation
2006-04-06, sal 14, hus 5, Kräftriket, Stockholm, 10:00
Opponent
Handledare
Tillgänglig från: 2006-03-07 Skapad: 2006-03-07Bibliografiskt granskad

Open Access i DiVA

fulltext(551 kB)750 nedladdningar
Filinformation
Filnamn FULLTEXT01.pdfFilstorlek 551 kBChecksumma SHA-1
6485eb8b061bda5df4e19cc6827eac0fd893fae8b0b95d35d175bac02e82e0a100319ea8
Typ fulltextMimetyp application/pdf

Av organisationen
Matematiska institutionen
Algebra och logik

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 750 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

isbn
urn-nbn

Altmetricpoäng

isbn
urn-nbn
Totalt: 1058 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf