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:
A Survey on Ordinal Notations Around the Bachmann-Howard Ordinal Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Lindenbaum’s Lemma via Open Induction

verfasst von : Francesco Ciraulo, Davide Rinaldi, Peter Schuster

Erschienen in: Advances in Proof Theory

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

With Raoult’s Open Induction in place of Zorn’s Lemma, we do a perhaps more perspicuous proof of Lindenbaum’s Lemma for not necessarily countable languages of first-order predicate logic. We generally work for and with classical logic, but say what can be achieved for intuitionistic logic, which prompts the natural generalizations for distributive and complete lattices.

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 About Truth and Types
Nächstes Kapitel Ordinal Analysis of Intuitionistic Power and Exponentiation Kripke Platek Set Theory
Fußnoten
1
The authors are most grateful to the anonymous referee for hinting at this issue.
 
2
This and other choices of terminology typical for constructive settings are made to prepare for Sect. 3.3.
 
3
We could equally have worked for and with propositional logic, with arbitrary formulas in place of sentences.
 
Literatur
1.
U. Berger, A computational interpretation of open induction, in Proceedings of the Ninetenth Annual IEEE Symposium on Logic in Computer Science (IEEE Computer Society, 2004), pp. 326–334
2.
3.
4.
5.
T. Coquand, Constructive topology and combinatorics, in Constructivity in Computer Science (San Antonio, TX, 1991), ed. by J.P. Myers Jr., M.J. O’Donnell. Lecture Notes in Computer Science, vol. 613 (Springer, Berlin, 1992), pp. 159–164
6.
T. Coquand, H. Persson, Gröbner bases in type theory, in Types for Proofs and Programs (Irsee, 1998), ed. by T. Altenkirch, W. Naraschewski, B. Reus. Lecture Notes in Computer Science, vol. 1657 (Springer, Berlin, 1999), pp. 33–46
7.
T. Coquand, J.M. Smith, An application of constructive completeness, in Types for Proofs and Programs (Torino, 1995), ed. by S. Berardi, M. Coppo. Lecture Notes in Computer Science, vol. 1158 (Springer, Berlin, 1996), pp. 76–84
8.
A.G. Drágalin, A completeness theorem for higher-order intuitionistic logic: an intuitionistic proof, in Mathematical Logic and Its Applications (Druzhba, 1986), ed. by D. Skordev (Plenum, New York, 1987), pp. 107–124
9.
A. Enayat, A. Visser, New constructions of satisfaction classes. Logic Group Preprint Series 303 (Utrecht University, 2013)
10.
M. Hendtlass, P. Schuster, A direct proof of Wiener’s theorem, in How the World Computes. Turing Centenary Conference and Eighth Conference on Computability in Europe (Cambridge, 2012), ed. by S.B. Cooper, A. Dawar, B. Löwe. Lecture Notes in Computer Science, vol. 7318 (Springer, Berlin, 2012), pp. 294–303
11.
12.
S. Huber, P. Schuster, Maximalprinzipien und Induktionsbeweise (Forthcoming)
13.
H. Ishihara, Constructive reverse mathematics: compactness properties, in From Sets and Types to Analysis and Topology, ed. by L. Crosilla, P. Schuster. Oxford Logic Guides 48 (Oxford University Press, 2005), pp. 245–267
14.
H. Kotlarski, S. Krajewski, A.H. Lachlan, Construction of satisfaction classes for nonstandard models. Can. Math. Bull. 24, 283–293 (1981)MathSciNetCrossRefMATH
15.
16.
17.
H. Persson, An application of the constructive spectrum of a ring, in Type Theory and the Integrated Logic of Programs, Ph.D. thesis (Chalmers University, University of Göteborg, 1999)
18.
19.
H. Rasiowa, R. Sikorski, The Mathematics of Metamathematics. Monografie Matematyczne 41. Panstwowe Wydawnictwo Naukowe, Warszawa (1963)
20.
D. Rinaldi, P. Schuster, A universal Krull-Lindenbaum theorem. J. Pure Appl. Algebra (to appear)
21.
D. Rinaldi, P. Schuster, Eliminating disjunctions by disjunction elimination (Forthcoming)
22.
23.
D. Scott, Completeness and axiomatizability in many-valued logic, in Proceedings of the Tarski Symposium (Berkeley, CA., 1971), ed. by L. Henkin et al. (American Mathematical Society, Providence, R.I., 1974), pp. 411–435
24.
P. Schuster, Induction in algebra: a first case study. in 27th Annual ACM/IEEE Symposium on Logic in Computer Science (Dubrovnik, 2012) (IEEE Computer Society Publications, 2012), pp. 581–585. Journal version: Log. Methods Comput. Sci. 3(20), 9 (2013)
25.
J.R. Shoenfield, Mathematical Logic (Association for Symbolic Logic, 2000)
26.
A. Tarski, Fundamentale Begriffe der Methodologie der deduktiven Wissenschaften. I. Monatsh. Math. Phys. 37, 361–404 (1930)MathSciNetCrossRef
Metadaten
Titel
Lindenbaum’s Lemma via Open Induction
verfasst von
Francesco Ciraulo
Davide Rinaldi
Peter Schuster
Copyright-Jahr
2016
Buch
Advances in Proof Theory

Print ISBN: 978-3-319-29196-3

Electronic ISBN: 978-3-319-29198-7

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-29198-7_3