FOM: Models of ZFC, truth predicates, reflection

[Joe Shipman]

Suppose you add a truth predicate Tr to ZFC, along the lines discussed
on FOM earlier this month, and also add a constant k and axioms saying
"k is inaccessible" and "Phi iff Tr(Phi) iff V_k |= Phi" for any
sentence Phi which doesn't mention Tr or k.  This is one way of
formalizing "k is an infallible cardinal".  What is the consistency
strength of this augmented system?  If there are inaccessibles then k
can't be the nth inaccessible because then V_k would model the false
sentence "there are exactly n-1 inaccessibles" -- how far up can this
kind of argument take you?

Related question: assume that inaccessible cardinals form a proper
class.  Define a sentence Phi of set theory to be "eventually true" if
for all sufficiently large inaccessible k, V_k |= Phi.  Clearly some
sentences are neither eventually true nor eventually false (for example,
"there is a largest inaccessible cardinal").  There is also a smallest k
such that V_k satisfies all eventually true sentences.  What can be said
about the size of this cardinal, and how does it compare with the
smallest infallible cardinal?

-- Joe Shipman