In this post, Andrej Bauer writes:

[…] the principle known as Proof by Contradiction: For every proposition $ϕ$, if $ϕ$ is not false then $ϕ$ is true. With a formula we write this as $∀ϕ∈\mathsf {Prop},¬¬ϕ⇒ϕ$.

I asked him in a comment how he justifies the use of the notation $∀ϕ∈\mathsf {Prop},¬¬ϕ⇒ϕ$, because I was confused, since I thought $\mathsf{Prop}$ should be the set of all propositions; but propositions are not first-class mathematical objects – one can only speak about them in some external meta-theory. Andrej told me that $\mathsf{Prop}$ is in fact not intended to be the set of all propositions/formulas, but rather the set of truth values. He said that the $\mathsf{Prop}$ he has in mind is isomorphic to the power set $\mathfrak P(\{\star\})$ of a singleton $\{\star\}$.

Questions:

1. Why is the set of truth values denoted $\mathsf{Prop}$? I think this notation suggests that the set is intended to include all propositions, rather than truth values.

2. If one can imagine $\mathsf{Prop}$ to be the power set $\mathfrak P(\{\star\})$ of a singleton $\{\star\}$, then the proof method by contradiction becomes

$$∀ϕ∈\mathfrak P(\{\star\}),¬¬ϕ⇒ϕ.$$

But this expression seems to me to not make sense. Because $\phi$ is a mathematical object (a subset of $\{\star\}$), and it does not make sense to apply logical connectives like $\Rightarrow$ or $\neg$ to mathematical objects. For example to say that the "$3$ and $5$ are true" does not make sense: $3$ and $5$ are not statements. Similarly, to say that "if $\phi$ isn't not true, then $\phi$ is true", where $\phi$ is a subset of $\{\star\}$ does not make sense.

When you write something like $\forall \phi \in Prop, \neg \neg \phi \Rightarrow \phi$, you are really making a metalogical claim, and it is a claim about propositions, not truth-values. The claim is that any proposition of the form $\neg \neg \phi$ logically implies the proposition $\phi$. Indeed, the $\Rightarrow$ symbol is a metalogical symbol of logical implication, it is not the material conditional logica symbol $\rightarrow$.