Change search
ReferencesLink to record
Permanent link

Direct link
A Natural Interpretation of Classical Proofs
Stockholm University, Faculty of Science, Department of Mathematics.
2006 (English)Doctoral thesis, monograph (Other academic)
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.

Place, publisher, year, edition, pages
Stockholm: Matematiska institutionen , 2006. , 100 p.
Keyword [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
National Category
Algebra and Logic
URN: urn:nbn:se:su:diva-913ISBN: 91-7155-206-5OAI: diva2:200630
Public defence
2006-04-06, sal 14, hus 5, Kräftriket, Stockholm, 10:00
Available from: 2006-03-07 Created: 2006-03-07Bibliographically approved

Open Access in DiVA

fulltext(551 kB)624 downloads
File information
File name FULLTEXT01.pdfFile size 551 kBChecksum MD5
Type fulltextMimetype application/pdf

By organisation
Department of Mathematics
Algebra and Logic

Search outside of DiVA

GoogleGoogle Scholar
Total: 624 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 865 hits
ReferencesLink to record
Permanent link

Direct link