Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
History and Prospects for First-Order Automated Deduction Read chapter Read first chapter

2015 | OriginalPaper | Chapter

Automating Leibniz’s Theory of Concepts

Authors : Jesse Alama, Paul E. Oppenheimer, Edward N. Zalta

Published in: Automated Deduction - CADE-25

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Our computational metaphysics group describes its use of automated reasoning tools to study Leibniz’s theory of concepts. We start with a reconstruction of Leibniz’s theory within the theory of abstract objects (henceforth ‘object theory’). Leibniz’s theory of concepts, under this reconstruction, has a non-modal algebra of concepts, a concept-containment theory of truth, and a modal metaphysics of complete individual concepts. We show how the object-theoretic reconstruction of these components of Leibniz’s theory can be represented for investigation by means of automated theorem provers and finite model builders. The fundamental theorem of Leibniz’s theory is derived using these tools.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
previous chapter Automated Reasoning in the Wild
next chapter Confluence Competition 2015
Footnotes
1
If we were to allow a predicate of the form \( [\lambda x\, \exists F(xF \, \& \, \lnot Fx)]\), then an abstract object that encodes such a property would exemplify the property if and only if it doesn’t. The paradox is avoided by banishing encoding from \(\lambda \)-expressions.
 
2
Note that since \(\lambda \)-expressions may not contain encoding subformulas, the comprehension principle for relations derivable from \(\beta \)-Conversion becomes similarly restricted. \(\beta \)-Conversion asserts that \([\lambda x_1\ldots x_n\, \phi ]y_1\ldots y_n \equiv \phi ^{y_1,\ldots ,y_n}_{x_1,\ldots ,x_n}\). We can universally generalize on each of the \(y_i\)s to obtain:
  • \(\forall y_1\ldots \forall y_n([\lambda x_1\ldots x_n\, \phi ]y_1\ldots y_n \equiv \phi ^{y_1,\ldots ,y_n}_{x_1,\ldots ,x_n})\)
Then we apply the Rule of Necessitation and existential generalization to obtain:
  • \(\exists F^n\Box \forall y_1\ldots \forall y_n(F^ny_1\ldots y_n \equiv \phi )\), provided \(F^n\) doesn’t occur free in \(\phi \) and \(\phi \) has no encoding subformulas.
This comprehension principle doesn’t guarantee that there are any relations definable in terms of encoding predications.
 
3
The informal construction “In Peano Number Theory, F0” can be analyzed in object theory as well. A theory is analyzed as an abstract object that encodes propositions p by encoding the propositional properties of the form \([\lambda y\, p]\) (read this predicate as: being such that p). Then we can define “In theory T, F0” as \(T[\lambda y\, F0]\), i.e., as T encodes the property being such that 0 exemplifies F. This analysis applies to any other mathematical individual \(\kappa \), mathematical theory T, and constructions of the form “In theory T, \(F\kappa \)”. For a full discussion of the analysis of mathematics within object theory, see [13].
 
4
It is an easy logical theorem that \(\Box \forall F(xF \equiv xF)\). But then, when x is a concept, it is abstract, and so it follows from the definition of identity that \(x=x\). Using the principle of substitution of identicals, we can then derive the symmetry and transitivity of identity for abstract objects.
 
5
Note we say condition here rather than relation because the definition of \(\preceq \) has encoding subformulas and, as such, \(\preceq \) is not guaranteed to be a relation.
 
6
See http://​mally.​stanford.​edu/​cm/​leibniz/​ for a description of this work and links to all the input and output files.
 
7
Indeed, if we define ‘the concept of every person’ as the concept that encodes exactly the properties F such that every person exemplifies F, then the containment theory of truth described below will offer a unified ‘subject-predicate’ analysis of the sentences ‘Alexander is happy’ and ‘Every person is happy’. On the containment theory of truth, the former is true because the concept of Alexander contains the concept of being happy, while the latter is true because the concept of every person contains the concept of being happy.
 
8
Leibniz asserts his containment theory of truth in the following passage taken from the translation in [15], 18–19 (the source is [3], 51):
...every true universal affirmative categorical proposition simply shows some connection between predicate and subject (a direct connexion, which is what is always meant here). This connexion is, that the predicate is said to be in the subject, or to be contained in the subject; either absolutely and regarded in itself, or at any rate, in some instance; i.e., that the subject is said to contain the predicate in a stated fashion. This is to say that the concept of the subject, either in itself or with some addition, involves the concept of the predicate.
The translator titled the fragment from which this passage is taken as ‘Elements of a Calculus’.
 
9
It is interesting to note that for some properties G, the proof that \({\varvec{c}}_u\) encodes G will rest on a contingency (namely, when G is a property contingently exemplified by u), but the proof that \(c_F\) encodes G doesn’t. That’s because it is provable that if \(F\Rightarrow G\) then \(\Box (F\Rightarrow G)\).
 
10
Instead of stating this logical axiom in its full generality, here is an example of an instance:
  • \( F\imath xGx \equiv \exists x(Gx \, \& \, \forall y(Gy \rightarrow y\! =\!x) \, \& \, Fx)\)
This is a version of Russell’s analysis of definite description, first described in [18]. If the description \(\imath xGx\) rigidly denotes the object that is uniquely G at the actual world (assuming there is one), then the above principle will fail to be necessarily true if there is a unique G at the actual world that is F at a world \(w_1\), but where nothing is G at \(w_1\) or where two distinct things are G.
 
11
See, for example, the Theodicy ([10], 371 = [5], vi, 363), where he talks about the ‘several Sextuses’, and in a letter to Hessen-Rheinfels, where he talks about the ‘many possible Adams’ ([16], 51 = [5], ii, 20).
 
12
The definition of o_equal_wrt is:
his says that X and Y are o_equal with respect to point D just in case X and Y are both ordinary objects and at every point D2, they exemplify the same properties. A similar definition defines: X and Y are a_equal with respect to point D just in case X and Y are both abstract objects and at every point D2, they encode the same properties.
 
13
It is important to note here that, in contrast to the concept of an individual, we need not have linked Y to the concept of F at the distinguished point d, given what we said in footnote 9.
 
14
The definition is: .
 
18
In general, we adopted the policy of proving necessitations of theorems only when they were required for the proof of another theorem. For example, the following necessary truth was needed for the proof of Theorem 40a: This asserts that for every point D, if X and Y are both concepts of the individual U with respect to D, then X and Y are identical abstract objects with respect to D.
 
Literature
1.
Alama, J.: Complete independence of an axiom system for central translations. Note di Matematica 33, 133–142 (2013)MathSciNetMATH
2.
3.
Couturat, L. (ed.): Opuscules et fragments inédits de Leibniz. F. Alcan, Paris (1903)
4.
5.
Gerhardt, C.I. (ed.): Die Philosophischen Schriften von Gottfried Wilhelm Leibniz, vol. i–vii. Weidmann, Berlin (1875–1990)
6.
7.
8.
9.
Leibniz, G.W.: A study in the calculus of real addition. In: Parkinson, G. (ed.) Leibniz Logical Papers, pp. 131–144. Clarendon, Oxford (1996)
10.
Leibniz, G.W.: Theodicy. Yale University Press, New Haven (1952)MATH
11.
Lewis, D.: Counterpart theory and quantified modal logic. J. Philos. 54(5), 113–126 (1968)CrossRef
12.
Montague, R.: The proper treatment of quantification in ordinary English. In: Hintikka, K.J.J., Moravcsik, J.M.E., Suppes, P. (eds.) Approaches to Natural Language, pp. 221–242. D. Reidel, Dordrecht (1973)CrossRef
13.
14.
Oppenheimer, P., Zalta, E.: Relations versus functions at the foundations of logic: type-theoretic considerations. J. Logic Comput. 21, 351–374 (2011)MathSciNetCrossRefMATH
15.
Parkinson, G. (ed.): Leibniz: Logical Papers. Clarendon, Oxford (1966)
16.
Parkinson, G. (ed.): Leibniz: Philosophical Writings. Dent & Sons, London (1973)
17.
Pelletier, F., Zalta, E.: How to say goodbye to the third man. Noûs 34(2), 165–202 (2000)CrossRef
18.
19.
Zalta, E.: Abstract Objects: An Introduction to Axiomatic Metaphysics. D. Reidel, Dordrecht (1983)CrossRef
20.
Zalta, E.: Intensional Logic and the Metaphysics of Intentionality. MIT Press, Cambridge (1988)
21.
22.
23.
Zalta, E.: Natural numbers and natural cardinals as abstract objects: a partial reconstruction of Frege’s Grundgesetze in object theory. J. Philos. Logic 28(6), 619–660 (1999)MathSciNetCrossRefMATH
24.
Zalta, E.: A (Leibnizian) theory of concepts. Philosophiegeschichte logische Analyse/Logical Anal. Hist. Philos. 3, 137–183 (2000)MATH
Metadata
Title
Automating Leibniz’s Theory of Concepts
Authors
Jesse Alama
Paul E. Oppenheimer
Edward N. Zalta
Copyright Year
2015
Book
Automated Deduction - CADE-25

Print ISBN: 978-3-319-21400-9

Electronic ISBN: 978-3-319-21401-6

Copyright Year: 2015

DOI
https://doi.org/10.1007/978-3-319-21401-6_4

Premium Partner

    Image Credits