2

Professor Peter Koellner, In a talk entitled 'On the Question of Whether the Mind Can be Mechanized' (slides), about Penrose's argument against strong AI, formalizes the concept of absolute provability (i.e. what can be produced by the idealized human mind) as K, and that of truth as T (slide 19). Later (slide 39) Koellner says "...one avoids the paradoxes of K by treating it as an operator and one avoids the paradoxes of T treating it as typed" without elaborating. In response to a question from the audience at 53:15, he says "It's an operator for K and a predicate for T. In this context, where truth is typed, you get an inconsistency if you try to treat K as a predicate. There are theorems due to Montague and Gödel himself, Thompson... that show you have to treat K as an operator."

I am hoping to gain some understanding of the differences between treating something as an operator as opposed to as a predicate, and if anyone can point me to something more on what inconsistencies might arise in this case, I would be most grateful.

sdenham
  • 131
  • The author treats $K$ as a modal operator, like "it is necessary that..." ($\square$). – Mauro ALLEGRANZA Sep 23 '21 at 06:04
  • $T$ is the intuitive notion of TRUE, as elucidated by Tarski's semantic theory. – Mauro ALLEGRANZA Sep 23 '21 at 06:04
  • See slides 19-20: $F$ is a formal system (typical of G's Th) and denotes also the collection of theorems of the system: $F \subseteq T$ means that the system is sound and the gist of 2nd Incompl.Th is: $\text {Con}(F) \notin F$ (a system $F$ satisfying G's Th assumptions) cannot prove its own consistency). But if $F$ is sound $\text {Con}(F)$ is true, and thus we have a true formula not provable in $F$ that amounts to saying that the provable formulas cannot exhaust the true ones. – Mauro ALLEGRANZA Sep 23 '21 at 14:02
  • Re $K$, see slide 21: can we read as the collection of formulas (maybe: mathematical facts ?) known by an idealized mind? If so, Claim 2 sounds like: if the idealized mind knows that a formal system $F$ is sound, then there is a known mathematical fact that is not provable in $F$. This seem reasonable: G's proof of the theorem manufacture an arithmetical formula $G$ that is undecidable in $F$ but it is true if we "read" it as meta-mathematical statement. – Mauro ALLEGRANZA Sep 23 '21 at 14:10
  • See page 27 for the "rules" regarding the "operator" $K$. They can be interpreted as the axioms governing the "ideal Knowability" predicate. Compare with the "Truth predicate" $T$ od Axiomatic truth theory. – Mauro ALLEGRANZA Sep 23 '21 at 14:12
  • @MauroALLEGRANZA WRT the idealized mind: In slide 25, Koellner is skeptical of the " idealized human mind" (and says more about it in the talk, starting at 42:25), but puts this aside to proceed with idealizing assumptions that are as favorable as he feels is possible to his opponents. – sdenham Sep 23 '21 at 14:14
  • And compare with the Provability predicate $\text {Prov}$ (or: $\text {Bew}$) of formalized G's Theorem. – Mauro ALLEGRANZA Sep 23 '21 at 14:17
  • The paradox of knowing is the famous logical omniscience problem in epistemology so we can resolve this by using non-normal modal logic operator K to treat knowledge as justified true belief (but even with this there're still disputes in philosophy like the soundness of epistemic closure property). Truth predicate T originated from Tarski's semantic theory of truth expressed in a metalanguage which belongs to the major correspondence theory of truth in philosophical. – cinch Sep 25 '21 at 01:47
  • A key feature of truth predicate T is it predicates sentence symbols (not objects) thus is a second order theory deciding primitive truth in possibly stratified metalanguages and it's extensional, while modal operator K is intensional thus its truth result may not only depend on the truth of its proposition content... – cinch Sep 26 '21 at 04:30

0 Answers0