Zobrazeno 1 - 10
of 101
pro vyhledávání: '"Gentzen's consistency proof"'
Autor:
Yuta Takahashi
Publikováno v:
Kagaku tetsugaku. 49:49-66
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::755f5ef0567bd25321d769724da83166
https://doi.org/10.4216/jpssj.49.1-49
https://doi.org/10.4216/jpssj.49.1-49
Autor:
Annika Siders
Publikováno v:
Archive for Mathematical Logic. 54:921-940
A proof of normalization for a classical system of Peano Arithmetic formulated in natural deduction is given. The classical rule of the system is the rule for indirect proof restricted to atomic formulas. This rule does not, due to the restriction, i
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::139c83b727c49b09183a360f5167091c
https://doi.org/10.1007/s00153-015-0450-y
https://doi.org/10.1007/s00153-015-0450-y
Publikováno v:
Journal of Symbolic Computation. 69:129-158
Kirby and Paris (1982) proved in a celebrated paper that a theorem of Goodstein (1944) cannot be established in Peano arithmetic. We present an encoding of Goodstein's theorem as a termination problem of a finite rewrite system. Using a novel impleme
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::438f07533f92eab68d7a6636d8776457
https://doi.org/10.1016/j.jsc.2014.09.033
https://doi.org/10.1016/j.jsc.2014.09.033
Autor:
Torkel Franzen
Publikováno v:
Inexhaustibility: A Non-Exhaustive Treatment
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9b08e1b4980c762b727be80b80183413
https://doi.org/10.1017/9781316755969.010
https://doi.org/10.1017/9781316755969.010
Autor:
Alex Simpson
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783662544570
FoSSaCS
FoSSaCS
Cyclic proof provides a style of proof for logics with inductive and coinductive definitions, in which proofs are cyclic graphs representing a form of argument by infinite descent. It is easily shown that cyclic proof subsumes proof by coinduction. S
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a033b1b378a27cc9f8e548364ede338f
https://doi.org/10.1007/978-3-662-54458-7_17
https://doi.org/10.1007/978-3-662-54458-7_17
Autor:
Gyesik Lee
Publikováno v:
Journal of the Korean Mathematical Society. 51:383-402
We expose a pattern for establishing Friedman-Weiermann style independence results according to which there are thresholds of prov- ability of some parameterized variants of well-partial-ordering. For this purpose, we investigate an ordinal notation
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::696c93acf1d164b28fe8460ddc84c4dc
https://doi.org/10.4134/jkms.2014.51.2.383
https://doi.org/10.4134/jkms.2014.51.2.383
Autor:
Annika Siders
Publikováno v:
Archive for Mathematical Logic. 52:449-468
This paper gives a Gentzen-style proof of the consistency of Heyting arithmetic in an intuitionistic sequent calculus with explicit rules of weakening, contraction and cut. The reductions of the proof, which transform derivations of a contradiction i
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f4765823cfc71d6e3b5b45f4b751183a
https://doi.org/10.1007/s00153-013-0324-0
https://doi.org/10.1007/s00153-013-0324-0
Autor:
Ryota Akiyoshi, Yuta Takahashi
Publikováno v:
Journal of the Japan Association for Philosophy of Science. 41:1-22
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::88f0c05da1085b54a4fcb5a8e6698190
https://doi.org/10.4288/kisoron.41.1_1
https://doi.org/10.4288/kisoron.41.1_1
Autor:
Ján Komara
Publikováno v:
Archive for Mathematical Logic. 50:617-624
We give a novel proof that primitive recursive functions are closed under nested simple recursion. This new presentation is supplied with a detailed proof which can be easily formalized in small fragments of Peano Arithmetic.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c1afc52f2d974abef2ef8e7495f8e0b8
https://doi.org/10.1007/s00153-011-0236-9
https://doi.org/10.1007/s00153-011-0236-9
Autor:
Gyesik Lee
Publikováno v:
Annals of Pure and Applied Logic. 147:48-70
We consider five ordinal notation systems of e 0 which are all well-known and of interest in proof-theoretic analysis of Peano arithmetic: Cantor’s system, systems based on binary trees and on countable tree-ordinals, and the systems due to Schutte
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::255a1e7958505821b36b595aab894a41
https://doi.org/10.1016/j.apal.2007.03.004
https://doi.org/10.1016/j.apal.2007.03.004