@Zanna Conveniently this does not really affect the terminology for truth-functional logic, which my more recent messages about logic are about. The meaning of "formula" in first-order logic as a whole is different from that of "propositional formula." Also, I don't use the phrase "propositional formula"; I prefer to call a combination of sentence letters and truth-functional sentential connectives a truth-functional schema (or schema for short, though there are other kinds of schemata).

However, in this and future messages, I will speak of open formulas, i.e. those in which one or more variables are free -- like "Fx" where "x" is a variable of quantification -- as formulas but not as sentences. And I will speak of closed formulas, i.e. those that are not open, i.e. those in which no variable is free -- like "Fa" (where a is a constant) and "∃x Fx" (where "x" is a variable of quantification) -- as formulas and also as sentences.

To clarify why I have been talking about truth tables lately, it is for a few reasons but they are closely connected. A while ago, I had prompted you to express schemata that used particular connectives by writing other schemata with other connectives--specifically, expressing p ∧ q with ¬ and ∨ [as ¬(¬p ∨ ¬q)] and p ∨ q with ¬ and ∧ [as ¬(¬p ∧ ¬q)] (or close variants thereof), and p → q with ¬ and ∨ [as ¬p ∨ q] and also with ¬ and ∧ [as ¬(p ∧ ¬q)].

All of which you did. However, your attitude toward your own correct results was tentative. I realized at the time that I had presented no method for actually checking arbitrary equivalences of truth-functional schemata, even though it would have made sense in context to do so, and even though it would have contributed conceptual clarity. When you mentioned rereading that part, I felt that I should make up for this.

As I thought about what to say, I realized that quite a bit would have stood to be bolstered by this material, because I had not actually said what logical equivalence means, and I had also not introduced the related and important concepts of logical implication, logical validity, and logical inconsistency. Those four concepts are closely tied to, but importantly not the same as, the biconditional, the conditional, truth, and falsity (respectively).