On formalization of model-theoretic proofs of gödel’s theorems

Makoto Kikuchi; Kazuyuki Tanaka

doi:10.1305/ndjfl/1040511346

On formalization of model-theoretic proofs of gödel’s theorems

Makoto Kikuchi, Kazuyuki Tanaka

Research output: Contribution to journal › Article › peer-review

10 Citations (Scopus)

Abstract

Within a weak subsystem of second-order arithmetic WKL₀, that is П⁰₂-conservative over PRA, we reformulate Kreisel’s proof of the Second Incompleteness Theorem and Boolos’ proof of the First Incompleteness Theorem.

Original language	English
Pages (from-to)	403-412
Number of pages	10
Journal	Notre Dame Journal of Formal Logic
Volume	35
Issue number	3
DOIs	https://doi.org/10.1305/ndjfl/1040511346
Publication status	Published - 1994
Externally published	Yes

ASJC Scopus subject areas

Logic

Access to Document

10.1305/ndjfl/1040511346

Cite this

@article{87da578d78914c37bc68457b3858a76b,

title = "On formalization of model-theoretic proofs of g{\"o}del{\textquoteright}s theorems",

abstract = "Within a weak subsystem of second-order arithmetic WKL0, that is П02-conservative over PRA, we reformulate Kreisel{\textquoteright}s proof of the Second Incompleteness Theorem and Boolos{\textquoteright} proof of the First Incompleteness Theorem.",

author = "Makoto Kikuchi and Kazuyuki Tanaka",

year = "1994",

doi = "10.1305/ndjfl/1040511346",

language = "English",

volume = "35",

pages = "403--412",

journal = "Notre Dame Journal of Formal Logic",

issn = "0029-4527",

publisher = "Duke University Press",

number = "3",

}

TY - JOUR

T1 - On formalization of model-theoretic proofs of gödel’s theorems

AU - Kikuchi, Makoto

AU - Tanaka, Kazuyuki

PY - 1994

Y1 - 1994

N2 - Within a weak subsystem of second-order arithmetic WKL0, that is П02-conservative over PRA, we reformulate Kreisel’s proof of the Second Incompleteness Theorem and Boolos’ proof of the First Incompleteness Theorem.

AB - Within a weak subsystem of second-order arithmetic WKL0, that is П02-conservative over PRA, we reformulate Kreisel’s proof of the Second Incompleteness Theorem and Boolos’ proof of the First Incompleteness Theorem.

UR - http://www.scopus.com/inward/record.url?scp=84972499822&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84972499822&partnerID=8YFLogxK

U2 - 10.1305/ndjfl/1040511346

DO - 10.1305/ndjfl/1040511346

M3 - Article

AN - SCOPUS:84972499822

VL - 35

SP - 403

EP - 412

JO - Notre Dame Journal of Formal Logic

JF - Notre Dame Journal of Formal Logic

SN - 0029-4527

IS - 3

ER -

On formalization of model-theoretic proofs of gödel’s theorems

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this