A Natural Interpretation of Classical Proofs

A Natural Interpretation of Classical Proofs

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...

Full description

Bibliographic Details
Main Author: Brage, Jens
Format: Doctoral Thesis
Language:English
Published: Stockholms universitet, Matematiska institutionen 2006
Subjects:
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
Mathematical logic
Matematisk logik
Online Access:http://urn.kb.se/resolve?urn=urn:nbn:se:su:diva-913
http://nbn-resolving.de/urn:isbn:91-7155-206-5

Internet

http://urn.kb.se/resolve?urn=urn:nbn:se:su:diva-913
http://nbn-resolving.de/urn:isbn:91-7155-206-5

Similar Items