In a paper published in 1975, Robert Jeroslow introduced the concept of an experimental logic as a generalization of ordinary formal systems such that theoremhood is a (or in practice ) rather than . These systems can be viewed as (rather crude) representations of axiomatic theories evolving stepwise over time. Similar ideas can be found in papers by Putnam (1965) and McCarthy and Shapiro (1987). The topic of the present article is a discussion of a suggestion by Allen Hazen, that (...) these experimental logics might provide an illuminating way of representing “the human mathematical mind”. This is done in the context of the well-known Lucas-Penrose thesis. Though we agree that Jeroslow's model has some merit in this context, and that the Lucas-Penrose arguments certainly are less than persuasive, some semi-technical doubts are raised concerning the alleged impact of experimental logics on the question of knowable self-consistency. (shrink)

PA is Peano Arithmetic. Pr(x) is the usual Σ1-formula representing provability in PA. A strong provability predicate is a formula which has the same properties as Pr(·) but is not Σ1. An example: Q is ω-provable if PA + ¬ Q is ω-inconsistent (Boolos [4]). In [5] Dzhaparidze introduced a joint provability logic for iterated ω-provability and obtained its arithmetical completeness. In this paper we prove some further modal properties of Dzhaparidze's logic, e.g., the fixed point property and the Craig (...) interpolation lemma. We also consider other examples of the strong provability predicates and their applications. (shrink)