Abstract
Epistemology includes in large part investigation of the conditions by which rational human knowledge and belief, of the propositional variety, can be secured. Our particular instance of this investigation arises from the stipulation that a human (a) receives a partial or complete formal argument/proof (\(\mathcal {A}\)) for/of a conclusion ϕ, where some computing machine \(\mathcal {M}\) “stands between” or mediates a’s receiving \(\mathcal {A}\) and ϕ. The mediation can take any number of forms, ranging from the simple and mundane (e.g., a is a teacher who types in to a text-editing system a proof of some easy theorem for a math class, and then prints out the proof for subsequent study and presentation to the class) to the exotic and famous (e.g., a receives a too-big-to-survey printout of a computer-generated proof of the four-color theorem). Under what conditions is it rational for a to believe ϕ? Once we have erected at least a reasonably precise framework for understanding the structure of arguments and proofs, classifying computing machines, ranking strength of knowledge and belief, and distinguishing at least roughly between types of computer mediation, this result, as we indicated, is a framework in which this pair of questions (and other, related ones) can eventually be answered.
We are deeply grateful for the vision (and patience!) of, and guidance provided by, editor Sven Ove Hansson. We are also indebted to both ONR and AFOSR for support that has made the investigation of forms of advanced logicist learning (of conclusions of proofs and arguments) possible.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
We are sorry to disappoint those readers who will wish to have this different question addressed as well or instead:
-
(QK)
Where \(\mathcal {M}\) mediates as provisionally described above, under what conditions does a in our instance really know that ϕ?
We leave (QK) aside in favor of (QB) and its variants because the conditions under which rational belief becomes knowledge have been notoriously difficult to set out to the satisfaction of most, let alone nearly all, thinkers. The most efficient way to confirm this is to read any decent overview of the “Gettier Problem” (GP) a problem generated by consideration of ingenious thought-experiments from Gettier (1963) in which an agent seems to know some proposition, but by any of the traditional accounts of knowledge as justified (= rational) true belief going back to Plato, doesn’t. E.g. see this cogent overview: (Ichikawa and Steup 2012). Plato’s original defense can be found in the Theaetetus, which can in turn be found in (Hamilton and Cairns 1961). A final word related to the GP conundrum: We encourage readers to join us in resisting the affirmation of any such principle as that if an agent a believes but doesn’t know ϕ, the agent can’t have learned ϕ—this being resistance that protects the position that a learns ϕ in the computer-mediated arrangement considered in the present paper, at least in cases in which the strength of the belief that ϕ on the part of a is high.
-
(QK)
- 2.
And eventually (QK) as well.
- 3.
An elegant example is infinite-time Turing machines; see (Hamkins and Lewis 2000). For a list of hypercomputing devices (in the context of a case, entirely separate from purposes driving the present chapter, for the proposition that human persons can hypercompute), see (Bringsjord and Arkoudas 2004).
- 4.
Not invariably. See our coverage of infinitary logic in Sect. 8.6.1.
- 5.
The second of these papers uses a scheme that generalizes, expands, and relaxes the scheme set out and employed in the first.
- 6.
Sanguine, skeptical readers can see some very recent publications which reveal that even today the role of probability in supporting rational belief, whether or not that belief is about arguments, proofs, and the conclusions therefrom, is highly controversial. E.g., the recently released Argument & Inference: An Introduction to Inductive Logic (Johnson 2016) divides the non-deductive basis for rational belief and decision-making into one part that leaves probability (in any guise) aside, and then another side that embraces and employs probability—and yet on the other hand, other overviews of this non-deductive basis assume that it must be probabilistic in nature (e.g. see Hawthorne 2004/2012).
- 7.
There are purely technical reasons for opting herein to use a streamlined multi-valued continuum for graded belief, given the current state of inductive logic, and for that matter of contemporary fields that also draw directly from probability, such as artificial intelligence (AI). (Bayesian reasoning in the AI of today is central to the field. For an overview, see Russell and Norvig 2009.) One reason is that today inductive logic, AI, and other probability-infused fields invariably make use of formal languages that are too inexpressive in the context of real-world proofs. Real-world proofs routinely make use of constructions that are infinitary in nature, and hence, taken at face value, these proofs, in the context of computer-mediation and epistemology, explode the bounds of formal languages that are the bases for probabilistic processing today. This is true because these languages are rooted in the space running from the propositional calculus to fragments of simple extensional logics like first-order logic (FOL) to FOL itself. This is despite seminal work long ago in the assignment of probabilities to formulae in infinitary formal languages of logics; (e.g. see Scott and Krauss 1966).
- 8.
- 9.
Specifically, for the proof, take ϕ to be a theorem established by some valid proof known to be valid by an arbitrary agent a, and stipulate that the second conjunct of the antecedent in this axiom is cashed out as both that {ψ}⊢⊥, and that a knows this.
- 10.
- 11.
One still in existence and available is OSCAR, created by John Pollock, and revived after his passing by our laboratory’s Kevin O’Neill. Resurrected (and improved) OSCAR can be obtained here: http://rair.cogsci.rpi.edu/projects/automated-reasoners/oscar.
- 12.
The proof can be obtained from http://www.cs.unm.edu/~mccune/papers/robbins/
- 13.
Many theorem provers also support what are called rewrite codes. These are computer functions that rewrite complex function expressions to simpler forms. Since function expressions can be written using just relation symbols, our discussion covers this too. See SNARK’s documentation for examples of procedural attachments and rewrite codes in action: http://www.ai.sri.com/~stickel/snark.html.
- 14.
- 15.
A fully technical, elegant version of GI based explicitly on The Liar can be found in (Ebbinghaus et al. 1994).
- 16.
See Footnote 8 if you haven’t done so already.
- 17.
A nice theory Γ is one that allows representations (it can prove facts about the primitive-recursive relations and functions), is decidable (for any ϕ, it is decidable whether Γ ⊢ ϕ) and is consistent. See Smith (2013) for a good introduction to the two Gödelian incompleteness theorems.
- 18.
- 19.
One specimen in the family is the Deontic Cognitive Event Calculus. See http://www.cs.rpi.edu/~govinn/dcec.pdf for an overview.
- 20.
References
Arkoudas, K., & Bringsjord, S. (2007). Computers, justification, and mathematical knowledge. Minds and Machines, 17(2), 185–202. http://kryten.mm.rpi.edu/ka_sb_proofs_offprint.pdf
Arkoudas, K., & Bringsjord, S. (2008). Toward formalizing common-sense psychology: An analysis of the false-belief task. In T.-B. Ho & Z.-H. Zhou (Eds.), Proceedings of the Tenth Pacific Rim International Conference on Artificial Intelligence (PRICAI 2008) (Lecture notes in artificial intelligence (LNAI), Vol. 5351, pp. 17–29). Springer. http://kryten.mm.rpi.edu/KA_SB_PRICAI08_AI_off.pdf
Baker, S., Ireland, A., & Smaill, A. (1992). On the use of the constructive omega-rule within automated deduction. In A. Voronkov (Ed.), Logic programming and automated reasoning (Lecture notes in computer science (LNCS), Vol. 624, pp. 214–225). Berlin: Springer.
Boolos, G. S., Burgess, J. P., & Jeffrey, R. C. (2003). Computability and logic (5th ed.). Cambridge: Cambridge University Press.
Bringsjord, S. (2015). A vindication of program verification. History and Philosophy of Logic, 36(3), 262–277. This URL goes to a preprint. http://kryten.mm.rpi.edu/SB_progver_selfref_driver_final2_060215.pdf
Bringsjord, S., & Arkoudas, K. (2004). The modal argument for hypercomputing minds. Theoretical Computer Science, 317, 167–190.
Bringsjord, S., & Govindarajulu, N. S. (2011). In defense of the unprovability of the church-turing thesis. Journal of Unconventional Computing, 6, 353–373. Preprint available at the URL given here. http://kryten.mm.rpi.edu/SB_NSG_CTTnotprovable_091510.pdf
Bringsjord, S., & Govindarajulu, N. S. (2012). Given the web, what is intelligence, really? Metaphilosophy, 43(4), 361–532. This URL is to a preprint of the paper. http://kryten.mm.rpi.edu/SB~NSG~Real~Intelligence~040912.pdf
Bringsjord, S., & Taylor, J. (2017). Logic: A modern approach: Beginning deductive logic, advanced. Troy, Motalen. This is an e-book edition of 23 Jan 2017. The book is accompanied by the Slate software system, ISBN of 978-0-692-60734-3, and version of 25 Jan 2016.
Bringsjord, S., & van Heuveln, B. (2003). The mental eye defense of an infinitized version of Yablo’s paradox. Analysis, 63(1), 61–70.
Bringsjord, S., Taylor, J., Shilliday, A., Clark, M., & Arkoudas, K. (2008). Slate: An argument-centered intelligent assistant to human reasoners. In F. Grasso, N. Green, R. Kibble, & C. Reed (Eds.), Proceedings of the 8th International Workshop on Computational Models of Natural Argument (CMNA 8) (pp. 1–10). Patras, University of Patras. http://kryten.mm.rpi.edu/Bringsjord_etal_Slate_cmna_crc_061708.pdf
Bringsjord, S., Govindarajulu, N., Thero, D., & Si, M. (2014). Akratic Robots and the computational logic thereof. In Proceedings of ETHICS 2014 (2014 IEEE Symposium on Ethics in Engineering, Science, and Technology), Chicago (pp. 22–29). IEEE Catalog Number: CFP14ETI-POD. Papers from the Proceedings can be downloaded from IEEE at URL provided here. http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6883275
Bringsjord, S., Licato, J., Govindarajulu, N., Ghosh, R., & Sen, A. (2015). Real robots that pass tests of self-consciousness. In Proceedings of the 24th IEEE International Symposium on Robot and Human Interactive Communication (RO-MAN 2015) (pp. 498–504). New York: IEEE. This URL goes to a preprint of the paper. http://kryten.mm.rpi.edu/SBringsjord_etal_self-con_robots_kg4_0601151615NY.pdf
Chisholm, R. (1966). Theory of knowledge. Englewood Cliffs: Prentice-Hall.
Chisholm, R. (1977). Theory of knowledge (2nd ed.). Englewood Cliffs: Prentice-Hall.
Chisholm, R. (1987). Theory of knowledge (3rd ed.). Englewood Cliffs: Prentice-Hall.
Ebbinghaus, H. D., Flum, J., & Thomas, W. (1994). Mathematical logic (2nd ed.). New York: Springer.
Francez, N., & Dyckhoff, R. (2010). Proof-theoretic semantics for a natural language fragment. Linguistics and Philosophy, 33, 447–477.
Franzén, T. (2004). Transfinite progressions: A second look at completeness. Bulletin of Symbolic Logic, 10, 367–389.
Friedman, N., & Halpern, J. (1995). Plausibility relations: A user’s guide. In Proceedings of the Eleventh Conference on Uncertainty in AI (pp. 175–184). https://www.cs.cornell.edu/home/halpern/papers/plausibility_manual.pdf
Galavotti, M. C. (2011). The modern epistemic interpretations of probability: Logicism and subjectivism. In D. Gabbay, S. Hartmann, & J. Woods (Eds.), Handbook of the history of logic (Inductive logic, Vol. 10, pp. 153–203). Amsterdam: Elsevier.
Gettier, E. (1963). Is justified true belief knowledge? Analysis, 23, 121–123. http://www.ditext.com/gettier/gettier.html
Govindarajulu, N. S., & Bringsjord, S. (2014). Proof verification can be hard! In Presented at the 10th Conference of Computability in Europe (CiE). http://www.naveensundarg.com/papers/ProofVerificationCanBeHard.pdf
Govindarajulu, N., Licato, J., & Bringsjord, S. (2013a). Small steps toward hypercomputation via infinitary machine proof verification and proof generation. In M. Giancarlo, A. Dennuzio, L. Manzoni, & A. Porreca (Eds.), Unconventional computation and natural computation (Lecture notes in computer science, Vol. 7956, pp. 102–112). Berlin: Springer.
Govindarajulu, N. S., Bringsjord, S., & Licato, J. (2013b). On deep computational formalization of natural language. In A. M. H. Abdel-Fattah & K.-U. Kühnberger (Eds.), Proceedings of the Workshop: “Formalizing Mechanisms for Artificial General Intelligence and Cognition” (Formal MAGiC) at Artificial General Intelligence 2013. http://cogsci.uni-osnabrueck.de/~formalmagic/FormalMAGiC-Proceedings.pdf
Hájek, A. (2002/2011). Interpretations of probability. In E. Zalta (Ed.), The stanford encyclopedia of philosophy. https://plato.stanford.edu/entries/probability-interpret
Hamilton, E., & Cairns, H. (Eds.). (1961). The collected dialogues of plato (including the letters). Princeton: Princeton University Press.
Hamkins, J. D., & Lewis, A. (2000). Infinite time turing machines. Journal of Symbolic Logic, 65(2), 567–604.
Hawthorne, J. (2004/2012). Inductive logic. In E. Zalta (Ed.), The stanford encyclopedia of philosophy. https://plato.stanford.edu/entries/logic-inductive
Hintikka, J., & Hilpinen, R. (1966). Knowledge, acceptance, and inductive logic. In P. Suppes & J. Hintikka (Eds.), Aspects of inductive logic (pp. 1–20). Amsterdam: North-Holland.
Ichikawa, J., & Steup, M. (2012). The analysis of knowledge. In E. Zalta (Ed.), The Stanford encyclopedia of philosophy. http://plato.stanford.edu/entries/knowledge-analysis
Johnson, G. (2016). Argument & inference: An introduction to inductive logic. Cambridge: MIT Press.
Kyburg, H. (1970). Probability and inductive logic. London: Macmillan.
Licato, J., Govindarajulu, N. S., Bringsjord, S., Pomeranz, M., & Gittelson, L. (2013). Analogico-deductive generation of Gödel’s first incompleteness theorem from the liar paradox. In F. Rossi (Ed.), Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI–13) (pp. 1004–1009). Beijing: Morgan Kaufmann. Proceedings are available online at http://ijcai.org/papers13/contents.php. The direct URL provided below is to a preprint. The published version is available at http://ijcai.org/papers13/Papers/IJCAI13-153.pdf, http://kryten.mm.rpi.edu/ADR_2_GI_from_LP.pdf
Pelletier, J. (1998). Automated natural deduction in thinker. Studia Logica, 60(1), 3–43.
Russell, S., & Norvig, P. (2009). Artificial intelligence: A modern approach (3rd ed.). Upper Saddle River: Prentice Hall.
Scott, D., & Krauss, P. (1966). Assigning probabilities to logical formulas. In P. Suppes & J. Hintikka (Eds.), Aspects of inductive logic (pp. 219–264). Amsterdam: North-Holland.
Smith, P. (2013). An introduction to Gödel’s theorems. Cambridge: Cambridge University Press. This is the second edition of the book.
Stickel, M., Waldinger, R., Lowry, M., Pressburger, T., & Underwood, I. (1994). Deductive composition of astronomical software from subroutine libraries. In Proceedings of the Twelfth International Conference on Automated Deduction (CADE–12), Nancy (pp. 341–355). SNARK can be obtained at the url provided here. http://www.ai.sri.com/~stickel/snark.html
Wiles, A. (1995). Modular elliptic curves and Fermat’s last theorem. Annals of Mathematics, 141(3), 443–551.
Wiles, A., & Taylor, R. (1995). Ring-theoretic properties of certain Hecke algebras. Annals of Mathematics, 141(3), 553–572.
Wos, L. (2013). The legacy of a great researcher. In M. P. Bonacina & M. E. Stickel (Eds.), Automated reasoning and mathematics: Essays in memory of William McCune (pp. 1–14). Berlin: Springer.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this chapter
Cite this chapter
Bringsjord, S., Govindarajulu, N.S. (2018). The Epistemology of Computer-Mediated Proofs. In: Hansson, S. (eds) Technology and Mathematics. Philosophy of Engineering and Technology, vol 30. Springer, Cham. https://doi.org/10.1007/978-3-319-93779-3_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-93779-3_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-93778-6
Online ISBN: 978-3-319-93779-3
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)