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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 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.
- 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:
.
- 15.
See http://mally.stanford.edu/cm/concepts/theorem40a.p and theorem40b.p.
- 16.
- 17.
- 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.
References
Alama, J.: Complete independence of an axiom system for central translations. Note di Matematica 33, 133–142 (2013)
Alama, J.: The simplest axiom system for hyperbolic geometry revisited, again. Stud. Logica 102(3), 609–615 (2014)
Couturat, L. (ed.): Opuscules et fragments inédits de Leibniz. F. Alcan, Paris (1903)
Fitelson, B., Zalta, E.: Steps toward a computational metaphysics. J. Philos. Logic 36(2), 227–247 (2007)
Gerhardt, C.I. (ed.): Die Philosophischen Schriften von Gottfried Wilhelm Leibniz, vol. i–vii. Weidmann, Berlin (1875–1990)
Henkin, L.: Completeness in the theory of types. J. Symb. 15(2), 81–91 (1950)
Kripke, S.: A completeness theorem in modal logic. J. Symb. Logic 24(1), 1–14 (1959)
Kripke, S.: Semantical considerations on modal logic. Acta Philos. Fennica 16, 83–94 (1963)
Leibniz, G.W.: A study in the calculus of real addition. In: Parkinson, G. (ed.) Leibniz Logical Papers, pp. 131–144. Clarendon, Oxford (1996)
Leibniz, G.W.: Theodicy. Yale University Press, New Haven (1952)
Lewis, D.: Counterpart theory and quantified modal logic. J. Philos. 54(5), 113–126 (1968)
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)
Nodelman, U., Zalta, E.: Foundations for mathematical structuralism. Mind 123(489), 39–78 (2014)
Oppenheimer, P., Zalta, E.: Relations versus functions at the foundations of logic: type-theoretic considerations. J. Logic Comput. 21, 351–374 (2011)
Parkinson, G. (ed.): Leibniz: Logical Papers. Clarendon, Oxford (1966)
Parkinson, G. (ed.): Leibniz: Philosophical Writings. Dent & Sons, London (1973)
Pelletier, F., Zalta, E.: How to say goodbye to the third man. Noûs 34(2), 165–202 (2000)
Russell, B.: On denoting. Mind 14, 479–493 (1905)
Zalta, E.: Abstract Objects: An Introduction to Axiomatic Metaphysics. D. Reidel, Dordrecht (1983)
Zalta, E.: Intensional Logic and the Metaphysics of Intentionality. MIT Press, Cambridge (1988)
Zalta, E.: Logical and analytic truths that are not necessary. J. Philos. 85(2), 57–74 (1988)
Zalta, E.: Twenty-five basic theorems in situation and world theory. J. Philos. Logic 22(4), 385–428 (1993)
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)
Zalta, E.: A (Leibnizian) theory of concepts. Philosophiegeschichte logische Analyse/Logical Anal. Hist. Philos. 3, 137–183 (2000)
Acknowledgments
The second and third authors would like to thank Branden Fitelson for collaborating on an earlier automated reasoning project and making us aware of the advances in theorem-proving technology.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Alama, J., Oppenheimer, P.E., Zalta, E.N. (2015). Automating Leibniz’s Theory of Concepts. In: Felty, A., Middeldorp, A. (eds) Automated Deduction - CADE-25. CADE 2015. Lecture Notes in Computer Science(), vol 9195. Springer, Cham. https://doi.org/10.1007/978-3-319-21401-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-21401-6_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-21400-9
Online ISBN: 978-3-319-21401-6
eBook Packages: Computer ScienceComputer Science (R0)