Hostname: page-component-cd9895bd7-q99xh Total loading time: 0 Render date: 2024-12-25T02:28:21.208Z Has data issue: false hasContentIssue false
  • English
  • Français

In the Shadows of the Löwenheim-Skolem Theorem: Early Combinatorial Analyses of Mathematical Proofs

Published online by Cambridge University Press:  15 January 2014

Jan von Plato
Jan von Plato*
Affiliation:
Department of Philosophy, PL 9, Siltavuorenpenger 20 A, 00014, University of Helsinki, FinlandE-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

The Löwenheim–Skolem theorem was published in Skolem's long paper of 1920, with the first section dedicated to the theorem. The second section of the paper contains a proof-theoretical analysis of derivations in lattice theory. The main result, otherwise believed to have been established in the late 1980s, was a polynomial-time decision algorithm for these derivations. Skolem did not develop any notation for the representation of derivations, which makes the proofs of his results hard to follow. Such a formal notation is given here by which these proofs become transparent. A third section of Skolem's paper gives an analysis for derivations in plane projective geometry. To clear a gap in Skolem's result, a new conservativity property is shown for projective geometry, to the effect that a proper use of the axiom that gives the uniqueness of connecting lines and intersection points requires a conclusion with proper cases (logically, a disjunction in a positive part) to be proved.

The forgotten parts of Skolem's first paper on the Löwenheim–Skolem theorem are the perhaps earliest combinatorial analyses of formal mathematical proofs, and at least the earliest analyses with profound results.

Type
Articles
Information
Bulletin of Symbolic Logic , Volume 13 , Issue 2 , June 2007 , pp. 189 - 225
Copyright
Copyright © Association for Symbolic Logic 2007

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Ackermann, W. [1932], Review of Skolem (1932a), Jahresbericht über die Fortschritte der Mathematik, vol. 58, pp. 65–66.Google Scholar
Ackermann, W. [1954], Solvable cases of the decision problem, North-Holland, Amsterdam.Google Scholar
Bernays, P. [1945], Review of Ketonen (1944), The Journal of Symbolic Logic, vol. 10, pp. 127–130.CrossRefGoogle Scholar
Birkhoff, G. [1937], Review of Skolem (1936), The Journal of Symbolic Logic, vol. 2, p. 50.Google Scholar
Birkhoff, G. [1940], Lattice theory, American Mathematical Society, Providence, Rhode Island, Second edition 1948.Google Scholar
Burris, S. [1995], Polynomial time uniform word problems, Mathematical Logic Quarterly, vol. 41, pp. 173–182.CrossRefGoogle Scholar
Cosmadakis, S. [1988], The word and generator problem for lattices, Information and Computation, vol. 77, pp. 192–217.CrossRefGoogle Scholar
Dummett, M. [1959], A logic with a denumerable matrix, The Journal of Symbolic Logic, vol. 24, pp. 96–107.CrossRefGoogle Scholar
Dyckhoff, R. and Negri, S. [2006], Decision methods for linearly ordered Heyting algebras, Archive for Mathematical Logic, vol. 45, pp. 411–422.CrossRefGoogle Scholar
Freese, R., Jezek, J., and Nation, J. [1995], Free lattices, American Mathematical Society, Providence, Rhode Island.CrossRefGoogle Scholar
Gentzen, G. [1932], Über die Existenz unabhangiger Axiomensysteme zu unendlichen Satzsysteme, Mathematische Annalen, vol. 107, pp. 329–250.CrossRefGoogle Scholar
Gödel, K. [2003], Collected works V, Oxford University Press.Google Scholar
Heyting, A. [1930], Die formalen Regeln der intuitionistischen Logik, Sitzungsberichte der Preussischen Akademie von Wissenschaften, Physikalisch-mathematische Klasse, pp. 42–56.Google Scholar
Ketonen, O. [1944], Untersuchungen zum Prädikatenkalkül, Annales Academiæ Scientiarium Fennicae. Series A.I. 23.Google Scholar
Lange-Nielsen, F. [1922], Review of Skolem (1920), Jahresbericht über die Fortschritte der Mathematik, vol. 48, pp. 1121–1122.Google Scholar
Löwenheim, L. [1915], Über Möglichkeiten im Relativkalkül, Mathematische Annalen, vol. 76, pp. 447–470, English translation in Heijenoort, van 1967.CrossRefGoogle Scholar
McKinsey, J. and Tarski, A. [1946], On closed elements in closure algebras, Annals of Mathematics, vol. 47, pp. 122–161.CrossRefGoogle Scholar
McKinsey, J. and Tarski, A. [1948], Some theorems on the sentential calculi of Lewis and Heyting, The Journal of Symbolic Logic, vol. 13, pp. 1–15.CrossRefGoogle Scholar
Mehrtens, H. [1979], Die Entstehung der Verbandstheorie, Gerstenberg Verlag, Hildesheim.Google Scholar
Negri, S. [1999], Sequent calculus proof theory of intuitionistic apartness and order relations, Archive for MathematicalLogic, vol. 38, pp. 521–547.Google Scholar
Negri, S. [2003], Contraction-free sequent calculi for geometric theories with an application to Barr's theorem, Archive for Mathematical Logic, vol. 42, pp. 389–401.CrossRefGoogle Scholar
Negri, S. and von Plato, J. [1998], Cut elimination in the presence of axioms, this Bulletin, vol. 4, pp. 418–435.Google Scholar
Negri, S. and von Plato, J. [2001], Structural proof theory, Cambridge University Press.CrossRefGoogle Scholar
Negri, S. and von Plato, J. [2002], Permutability of rules in lattice theory, Algebra Universalis, vol. 48, pp. 473–477.CrossRefGoogle Scholar
Negri, S. and von Plato, J. [2004], Proof systems for lattice theory, Mathematical Structures in Computer Science, vol. 14, pp. 507–526.CrossRefGoogle Scholar
Schroeder-Heister, P. [2002], Resolution and the origins of structural reasoning: early proof-theoretic ideas of Hertz and Gentzen, this Bulletin, vol. 8, pp. 246–265.Google Scholar
Scott, D. [1958], Review of Skolem (1958), Mathematical Reviews, vol. 18, p. 000.Google Scholar
Skolem, T. [1913], Om konstitutionen av den identiske kalkuls grupper, Proceedings of the 3rd Scandinavian mathematical congress, Kristiania, English translation in Skolem 1970, pp. 53–65, pp. 149–163.Google Scholar
Skolem, T. [1919], Untersuchungen über die Axiome des Klassenkalküls und über Produktations- und Summationsprobleme, welche gewisse Klassen von Aussagen betreffen, as reprinted in Skolem 1970, pp. 67–101.Google Scholar
Skolem, T. [1920], Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Satze, nebst einem Theoreme uber dichte Mengen, as reprinted in Skolem 1970, pp. 103–136.Google Scholar
Skolem, T. [1923], Einige Bemerkungen zur axiomatischen Begründung der Mengenlehre, as reprinted in Skolem 1970, pp. 137–152.Google Scholar
Skolem, T. [1928], Über die mathematische Logik, as reprinted in Skolem 1970, pp. 189–206.Google Scholar
Skolem, T. [1929], Über einige Grundlagenfragen der Mathematik, as reprinted in Skolem 1970, pp. 227–273.Google Scholar
Skolem, T. [1931a], Über die symmetrisch allgemeinen Lösungen im Klassenkalkul, Fundamenta mathematicae, vol. 18, pp. 61–76.CrossRefGoogle Scholar
Skolem, T. [1931b], Über die symmetrisch allgemeinen Lösungen im identischen Kalkul, as reprinted in Skolem 1970, pp. 307–336.Google Scholar
Skolem, T. [1932], Review of Gentzen (1932), Jahresbericht über die Fortschritte der Mathematik, vol. 58, pp. 63–64.Google Scholar
Skolem, T. [1936], Über gewisse ‘Verbände’ oder ‘Lattices’, as reprinted in Skolem 1970, pp. 412–424.Google Scholar
Skolem, T. [1936a], Utvalgte kapitler av den matematiske logikk, Chr. Michelsens Institutt, Bergen.Google Scholar
Skolem, T. [1941], Sur la portée du théorème de Löwenheim–Skolem, as reprinted in Skolem 1970, pp. 455–482.Google Scholar
Skolem, T. [1952–1953], Consideraciones sobre los fundamentos de la matematica, Revista Matematica Hispano–Americana, vol. 12, pp. 169–200, and vol. 13, pp. 149–174.Google Scholar
Skolem, T. [1958], Remarks on the connection between intuitionistic logic and a certain class of lattices, as reprinted in Skolem 1970, pp. 639–644.Google Scholar
Skolem, T. [1970], Selected works in logic (Fenstad, J. E., editor), Universitetsforlaget, Oslo.Google Scholar
Stone, M. [1937], Topological representations of distributive lattices and Brouwerian logics, Casopis Pro Pestovani Matematiky a Fysiki Cast Matematicka, vol. 67, pp. 1–25.Google Scholar
Tarski, A. [1938], Der Aussagenkalkül und die Topologie, Fundamenta Mathematicae, vol. 31, pp. 103–134.CrossRefGoogle Scholar
Tarski, A. [1949], On essential undecidability, The Journal of Symbolic Logic, vol. 14, pp. 75–76.Google Scholar
Thiel, C. [1994], Schröders zweiter Beweis für die Unabhängigkeit der zweiten Subsumption des Distributivgesetzes im logischen Kalkül, Modern Logic, vol. 4, pp. 382–391.Google Scholar
Heijenoort, J. van (editor) [1967], From Frege to Gödel, A source book in mathematical logic, 1879–1931, Harvard University Press.Google Scholar
Plato, J. von [1995], The axioms of constructive geometry, Annals of Pure and Applied Logic, vol. 76, pp. 169–200.CrossRefGoogle Scholar
Plato, J. von [2001], Natural deduction with general elimination rules, Archive for Mathematical Logic, vol. 40, pp. 541–567.CrossRefGoogle Scholar
Plato, J. von [2003], Skolem's discovery of Gödel–Dummett logic, Studia Logica, vol. 73, pp. 153–157.CrossRefGoogle Scholar
Plato, J. von [2004], Ein Leben, ein Werk – Gedanken über das wissenschaftliche Schaffen des finnischen Logikers Oiva Ketonen, Form, Zahl, Ordnung: Studien zur Wissenschafts- und Technikgeschichte (Seising, R., editor), Franz Steiner Verlag, Stuttgart, pp. 427–435.Google Scholar
Plato, J. von [2005], Combinatorial analysis of proofs in elementary geometry, ms.Google Scholar
Plato, J. von [2007], Gentzen s logic, Handbook of the history and philosophy of logic, vol. 5, in press.Google Scholar
Wang, H. [1970], A survey of Skolem's work in logic, pp. 17–52 in Skolem, (1970).Google Scholar