Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Computability of Algebraic and Definable Closure Kapitel lesen Erstes Kapitel lesen

2020 | OriginalPaper | Buchkapitel

On the Tender Line Separating Generalizations and Boundary-Case Exceptions for the Second Incompleteness Theorem Under Semantic Tableaux Deduction

verfasst von : Dan E. Willard

Erschienen in: Logical Foundations of Computer Science

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Our previous research has studied the semantic tableaux deductive methodology, of Fitting and Smullyan, and observed that it permits boundary-case exceptions to the Second Incompleteness Theorem, when multiplication is viewed as a 3-way relation (rather than as a total function). It is known that tableaux methodologies do prove a schema of theorems, verifying all instances of the Law of the Excluded Middle. But yet we show that if one promotes this schema of theorems into formalized logical axioms, then the meaning of the pronoun “I” in our self-referencing engine changes, and our partial evasions of the Second Incompleteness Theorem come to a complete halt.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Lifting Recursive Counterexamples to Higher-Order Arithmetic
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
Some quotes from Sacks’s YouTube talk [38] are that Gödel “did not think” the objectives of Hilbert’s Consistency Program “were erased” by the Incompleteness Theorem, and Gödel believed (according to Sacks) it left Hilbert’s program “very much alive and even more interesting than it initially was”.
 
2
This is because all the common apparatuses satisfy the requirement of Gödel’s Completeness Theorem.
 
3
The Example 1 had provided three examples of Hilbert-Frege style deduction operators, called \(D_E\), \(D_H\) and \(D_M\). It explained how these deductive operators differ from a tableaux-style deductive apparatus by containing a modus ponens rule.
 
4
The exact meaning of this implication is subtle. This is because Peano Arithmetic (PA) cannot know whether \(\beta \) is consistent when \( \beta = PA\). Thus, unlike the quite different formalism of \(\text {IS}_{ Tab-1}(PA)~\), the system of PA shall linger in a state of self-doubt, about whether both PA and \(\text {IS}_{ Tab-1}(PA)~\) are consistent.
 
5
\(\text {IS}_{Xtab}(\beta )\) actually satisfies a requirement stronger than Item I because it recognizes addition as total.
 
6
The point is that proofs are compressed when theorems are transformed into logical axioms, and such compressions can produce diagonalizing contradictions under some Type-A logics using “I am consistent” axioms.
 
7
Actually, we will only need the “Locally 1-Closure” property to prove that \(\text {IS}_{Xtab}(\beta )\). cannot possibly be self-justifying.
 
Literatur
1.
Adamowicz, Z., Bigorajska, T.: Existentially closed structures and Gödel’s second incompleteness theorem. JSL 66(1), 349–356 (2001)MATH
2.
Adamowicz, Z., Zbierski, P.: On Herbrand consistency in weak theories. Arch. Math. Log. 40(6), 399–413 (2001)CrossRef
3.
Artemov, S.: Explicit provablity and constructive semantics. Bull. Symb. Log. 7(1), 1–36 (2001)CrossRef
4.
Artemov, S.: The provability of consistency. Cornell Archives arXiv Report 1902.07404v4 (2019)
5.
Artemov, S., Beklemishev, L.D.: Provability logic. In: Handbook on Philosophical Logic, 2nd edn, pp. 189-360 (2005)
6.
Beklemishev, L.D.: Reflection principles and provability algebras in formal arithmetic. Russ. Math. Surv. 60(2), 197–268 (2005)CrossRef
7.
Beklemishev, L.D.: Positive provability for uniform reflection principles. APAL 165(1), 82–105 (2014)MathSciNetMATH
8.
Bezboruah, A., Shepherdson, J.C.: Gödel’s second incompleteness theorem for Q. JSL 41(2), 503–512 (1976)MATH
9.
Buss, S.R.: Bounded arithmetic. Studies in Proof Theory, Lecture Notes 3, disseminated by Bibliopolis as revised version of Ph.D. thesis (1986)
10.
Buss, S.R., Ignjatović, A.: Unprovability of consistency statements in fragments of bounded arithmetic. APAL 74(3), 221–244 (1995)MathSciNetMATH
11.
Dawson, J.W.: Logical Dilemmas: The Life and Work of Kurt Gödel. AKPeters Press (1997)
12.
Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press (2001)
13.
Feferman, S.: Arithmetization of mathematics in a general setting. FundMath 49, 35–92 (1960)MATH
14.
15.
16.
Friedman, H.M.: On the consistency, completeness and correctness problems. Ohio State Tech Report (1979). See also Pudlák [36]’s summary of this result
17.
Friedman, H.M.: Translatability and relative consistency. Ohio State Tech Report (1979). See also Pudlák [36]’s summary of this result
18.
Friedman, H.M.: Gödel’s blessing and Gödel’s curse. (This is “Lecture 4” within a 5-part Ohio State YouTube lecture series, dated 14 March 2014)
19.
Gentzen, G.: Die Wiederpruchsfreiheit der reinen Zahlentheorie. Math. Ann. 112, 439–565 (1936)CrossRef
20.
Gödel, K.: Über formal unentscheidbare sätze der Principia Mathematica und verwandte systeme I. Monatshefte für Mathematik und Physik 38, 349–360 (1931)MATH
21.
Gödel, K.: The present situation in the foundations of mathematics. In: Feferman, S., Dawson, J. W., Goldfarb, W., Parsons, C., Solovay, R.M. (eds.) Collected Works Volume III: Unpublished Essays and Lectures, pp. 45–53, Oxford University Press (2004)
22.
Goldstein, R.: Incompleteness: The Proof and Paradox of Kurt Gödel. Norton Press (2005)
23.
24.
25.
Hájek, P., Pudlák, P.: Metamathematics of First Order Arithmetic. Springer, Heidelberg (1991)MATH
26.
27.
28.
29.
Kreisel, G., Takeuti, G.: Formally self-referential propositions for cut-free classical analysis. Dissertationes Mathematicae 118, 1–50 (1974)MathSciNetMATH
30.
Mendelson, E.: Introduction to Mathematical Logic. CRC Press (2010)
31.
Nelson, E.: Predicative Arithmetic. Mathematics Notes. Princeton University Press, Princeton (1986)CrossRef
32.
33.
Paris, J.B., Dimitracopoulos, C.: A note on the undefinability of cuts. JSL 48(3), 564–569 (1983)MathSciNetMATH
34.
Parsons, C.: On \(n-\)quantifier elimination. JSL 37(3), 466–482 (1972)MATH
35.
36.
37.
Rogers, H.A.: Theory of Recursive Functions and Effective Compatibility. McGrawHill (1967)
38.
Sacks, G.: Some detailed recollections about Kurt Gödel during a June 2, 2014 YouTube lecture given by Gerald Sacks at the University of Pennsylvania. This lecture records the experiences of Sacks when he was a 1-year assistant for Gödel at the Institute of Advanced Studies. Some quotes from this talk are that Gödel “did not think” the goals of Hilbert’s Consistency Program “were erased” by the Incompleteness Theorem, and that Gödel believed (according to Sacks) that it left Hilbert’s program “very much alive and even more interesting than it initially was”
39.
Smullyan, R.: First Order Logic. Dover Books (1995)
40.
41.
Solovay, R.M.: Private Telephone conversations during April of 1994 between Dan Willard and Robert M. Solovay. During those conversations Solovay described an unpublished generalization of one of Pudlák’s theorems [35], using some methods of Nelson and Wilkie-Paris [31,44]. (The Appendix A of [46] offers a 4-page summary of our interpretation of Solovay’s remarks. Several other articles [10,25,31,33,35,44] have also noted that Solovay often has chosen to privately communicate noteworthy insights that he has elected not to formally publish)
42.
Švejdar, V.: An interpretation of Robinson arithmetic in its Grzegorczjk’s weaker variant. Fundamenta Informaticae 81, 347–354 (2007)MathSciNetMATH
43.
44.
Wilkie, A.J., Paris, J.B.: On the scheme of induction for bounded arithmetic. APAL 35, 261–302 (1987)MathSciNetMATH
45.
46.
Willard, D.E.: Self-verifying systems, the incompleteness theorem and the tangibiltiy reflection principle. JSL 66(2), 536–596 (2001)MATH
47.
Willard, D.E.: How to extend the semantic tableaux and cut-free versions of the second incompleteness theorem almost to Robinson’s arithmetic Q. JSL 67(1), 465–496 (2002)MathSciNetMATH
48.
Willard, D.E.: A version of the second incompleteness theorem for axiom systems that recognize addition but not multiplication as a total function. In: Hendricks, V., Neuhaus, F., Pedersen, S.A., Sheffler, U., Wansing, H. (eds.) First Order Logic Revisited, pp. 337–368, Logos Verlag, Berlin (2004)
49.
Willard, D.E.: An exploration of the partial respects in which an axiom system recognizing solely addition as a total function can verify its own consistency. JSL 70(4), 1171–1209 (2005)MathSciNetMATH
50.
Willard, D.E.: A generalization of the second incompleteness theorem and some exceptions to it. APAL 141(3), 472–496 (2006)MathSciNetMATH
51.
Willard, D.E.: On the available partial respects in which an axiomatization for real valued arithmetic can recognize its consistency. JSL 71(4), 1189–1199 (2006)MathSciNetMATH
52.
Willard, D.E.: Passive induction and a solution to a Paris-Wilkie open question. APAL 146(2), 124–149 (2007)MathSciNetMATH
53.
Willard, D.E.: Some specially formulated axiomizations for I\(\Sigma _0\) manage to evade the Herbrandized version of the second incompleteness theorem. Inf. Comput. 207(10), 1078–1093 (2009)CrossRef
54.
Willard, D.E.: On how the introducing of a new \(~\theta ~\) function symbol into arithmetic’s formalism is germane to devising axiom systems that can appreciate fragments of their own Hilbert consistency. Cornell Archives arXiv Report 1612.08071 (2016)
55.
Yourgrau, P.: A World Without Time: The Forgotten Legacy of Gödel and Einstein. (See page 58 for the passages we have quoted.) Basic Books (2005)
Metadaten
Titel
On the Tender Line Separating Generalizations and Boundary-Case Exceptions for the Second Incompleteness Theorem Under Semantic Tableaux Deduction
verfasst von
Dan E. Willard
Copyright-Jahr
2020
Buch
Logical Foundations of Computer Science

Print ISBN: 978-3-030-36754-1

Electronic ISBN: 978-3-030-36755-8

Copyright-Jahr: 2020

DOI
https://doi.org/10.1007/978-3-030-36755-8_17