Smullyan's truth and provability

We revisit Smullyan's paper ``Truth and Provability'' (2013) for three purposes. First, we introduce the notion of Smullyan models to give a precise definition for Smullyan's framework discussed in that paper. Second, we clarify the relationship between three theorems proved by Smullyan and other newly introduced properties for Smullyan models in terms of both implications and non-implications. Third, we construct two Smullyan models based on arithmetical ideas and show the correspondence between the properties of these Smullyan models and those concerning truth and provability in arithmetic.