I took these to mean the existential operator and the implication operator, but I agree they were insufficiently defined for me, esp. as we're building from first principles. The post could have made the early proofs more obvious in how they were constructed (e.g. how the language is really used to prove statements).