Abstract
Frames are a concept in knowledge representation that explains how the receiver, using background information, completes the information conveyed by the sender. This concept is used in different disciplines, most notably in cognitive linguistics and artificial intelligence. This paper argues that frames can serve as the basis for describing mathematical proofs. The usefulness of the concept is illustrated by giving a partial formalisation of proof frames, specifically focusing on induction proofs, and relevant parts of the mathematical theory within which the proofs are conducted; for the latter, we look at natural numbers and trees specifically.
Original: Mark.Howison at English Wikipedia This version: CheChe • CC BY-SA 4.0
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
Notes
- 1.
- 2.
- 3.
Schank and Abelson (1977) develop the related concept of scripts, which adds a temporal dimension. Though we do not model temporal progression explicitly, our use of frames also resembles scripts, if one reads the constituents of a proof frame as a plan for linear text organisation.
- 4.
This shows a certain kind of freedom we have in defining frames; we could also define the circle based on the centre and the diameter, of course.
- 5.
Our feature structures will employ subtyping and inheritance for this purpose.
- 6.
See, e.g., Ruppenhofer et al. (2006) and the project’s website at https://framenet.icsi.berkeley.edu
- 7.
Even core roles can be omitted sometimes, as in John finally sold his car.
- 8.
If there is more than one induction step, each of them can have a different successor function. As several base cases and induction steps are possible, the BASE-CASES and INDUCTION-STEPS features should be considered list-valued in principle, even if we use a simplified singleton notation (with features BASE-CASE and INDUCTION-STEP, but see Appendix A for a more complete version of the frame) in most examples.
- 9.
In this and in the following proofs the subdivision by small Latin letters has been added by the authors of this paper. References to equations have been renumbered according to the scheme used in the rest of this article.
- 10.
The original text reads: f k−1(v) = 0. The misprint was corrected here in 4.
- 11.
ex(n, H) means the number of edges of a graph \(G\nsupseteq H\) that is extremal for n and H, i.e., the maximal amount of edges a graph on n vertices could have, without having a subgraph (isomorphic to) H.
References
Azzouni, J. (2004). The derivation-indicator view of mathematical practice. Philosophia Mathematica, 12(2), 81–106.
Azzouni, J. (2009). Why do informal proofs conform to formal norms? Foundations of Science, 14(1–2), 9–26.
Bollobás, B. (1995). Extremal graph theory. In R. L. Graham, M. Grotschel, & L. Lovasz (Eds.), Handbook of combinatorics (Vol. 2, pp. 1231–1292). Amsterdam/New York: Elsevier.
Carl, M., & Koepke, P. (2010). Interpreting Naproche—An algorithmic approach to the derivation-indicator view. In Proceedings of the International Symposium on Mathematical Practice and Cognition (pp. 7–10).
Carpenter, B. (1992). The logic of typed feature structures (Cambridge tracts in theoretical computer science). Cambridge: Cambridge University Press.
Coq Development Team. (2017). The Coq proof assistant: Reference manual, version 8.7.2. INRIA. https://coq.inria.fr/refman/index.html
Cramer, M. (2013). Proof-checking mathematical texts in controlled natural language. Ph.D. thesis, Rheinische Friedrich-Wilhelms-Universität Bonn.
Cramer, M., et al. (2009). The Naproche project: Controlled natural language proof checking of mathematical texts. In N. E. Fuchs (Ed.), Controlled natural language (Lecture notes in computer science, Vol. 5972, pp. 170–186). Heidelberg: Springer.
Diestel, R. (2006). Graph theory. Heidelberg: Springer.
Fillmore, C. (1968). The case for case. In E. Bach & R. T. Harms (Eds.), Universals in linguistic theory (pp. 1–88). London: Holt, Rinehart, and Winston.
Kowalski, E. (2016). Linear algebra (Lecture notes). ETH Zurich, published at https://people.math.ethz.ch/~kowalski/script-la.pdf.
Marlow, S. (Ed.). (2010). Haskell 2000 language report. Haskell 2010 Committee. https://www.haskell.org/onlinereport/haskell2010/.
Minsky, M. (1974). A framework for representing knowledge. Technical report. Cambridge, MA: MIT.
Rav, Y. (2007). A critique of a formalist-mechanist version of the justification of arguments in mathematicians’ proof practices. Philosophia Mathematica, 15(3), 291–320. https://doi.org/10.1093/philmat/nkm023
Roberts, R. B., & Ira, P. Goldstein (1977a). The FRL manual. Technical report. Cambridge, MA: MIT.
Roberts, R. B., & Ira, P. Goldstein (1977b). The FRL primer. Technical report. Cambridge, MA: MIT.
Ruppenhofer, J., et al. (2006). FrameNet II: Extended theory and practice. Distributed with the frameNet data. Berkeley: International Computer Science Institute.
Schank, R. C., & Abelson, R. P. (1977). Scripts, plans, goals and understanding: An inquiry into human knowledge structures. Hillsdale: L. Erlbaum.
Tanswell, F. (2015). A problem with the dependence of informal proofs on formal proofs. Philosophia Mathematica, 23(3), 295–310. https://doi.org/10.1093/philmat/nkv008
Túrán, P. (1941). Egy gráfelméleti szélsőértékfeladatról – Eine Extremalaufgabe aus der Graphentheorie. Matematikai és Fizikai Lapok, 48, 436–452.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Fisseni, B., Sarikaya, D., Schmitt, M., Schröder, B. (2019). How to Frame a Mathematician. In: Centrone, S., Kant, D., Sarikaya, D. (eds) Reflections on the Foundations of Mathematics. Synthese Library, vol 407. Springer, Cham. https://doi.org/10.1007/978-3-030-15655-8_19
Download citation
DOI: https://doi.org/10.1007/978-3-030-15655-8_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-15654-1
Online ISBN: 978-3-030-15655-8
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)