cyclic definitions of material/logical implications

Question

Most sources define the material implication (conditional) using a pre-defined connective, usually "or", $$\left(p \implies q\right) \text{ iff } \left(\lnot p \lor q\right) \qquad \text{(1)}$$

Different definitions are possible, including one using "and" instead of "or", and even defining implication as an atom and then defining "and" and "or" in terms of the atom. Regardless, given a material implication, then...

The definition of the logical implication is $$\left(p \vdash q\right) \text{ iff } \left(\left(p\implies q\right) \text{ is a tautology } \top\right) \qquad \text{(2)}$$

(I think some sources use the notation $p \therefore q$ to mean $p \vdash q$ and $p \because q$ to mean $p \dashv q$. Personally I like $\therefore$ and $\because$ more because of their $\LaTeX$ commands \therefore and \because.)

I have some problems with the definitions above.

1. In definition (1), what is meant by "iff"? I always thought that "if and only if" was the material equivalence (biconditional) $a \iff b$, which is defined by $\left(a\implies b\right)\land\left(b\implies a\right)$, which is a binary operation of propositions, that is, it takes two propositions and makes a new one (analogous to the mathematical expression "$x+y$"). So, doing some scratchwork I found that $$\left(p \implies q\right) \iff \left(\lnot p \lor q\right)$$ reduces to $\top$. What does that mean? Stating just "$\top$" doesn't make sense; it's a constant. That would be like stating "$x+y$" as a definition. Definition (1) should be a logical statement about propositions, not a proposition itself. Right?

   I assume that the "iff" in definition (1) is meant to mean that the propositions are "the same", since it's a definition (or if not a definition, a theorem). Since they are "the same", couldn't one say they are logically equivalent and write $$\left(p\implies q\right) \dashv\vdash \left(\lnot p \lor q\right) \qquad \text{(1b)}$$ (where $\dashv\vdash$ denotes logical equivalence, I believe)? This seems to be right, since it's not a binary operation of propositions but rather more like a binary relation of propositions: it takes two propositions and compares them (analogous to the mathematical statement "$x\lt y$"). So is the "iff" in (1) an abuse of notation, or could the phrase "if and only if" denote both material equivalence and logical equivalence?

2. In definition (2), the word "iff" appears again, except this time I'm more confused. For certain, it can't denote the material equivalence $\iff$, because the definition isn't an operation connecting two propositions. It can't even denote the logical equivalence $\dashv\vdash$, because the definition isn't a relation comparing propositions. It appears to be a statement about logical statements! Apparently, the phrase "if and only if" has a third meaning, a so-called metalogical equivalence: a statement comparing two logical statements. Is there such thing as a meta-metalogical equivalence? Where does it end??

   Also, what is meant by the "is" in "$\left(p\implies q\right) \text{ is a tautology } \top$"? Does it mean "is logically equivalent to"? If so, can definition (2) be rewritten... ? $$\left(p\vdash q\right)\text{ "is the same as" }\left(\left(p\iff q\right)\dashv\vdash\top\right) \qquad \text{(2b)}$$ If so, $\dashv\vdash$ would have to be defined beforehand.

3. Lastly, setting all syntactic issues aside, the biggest problem I have of all is the fact that these definitions seem to be semantically dependent on each other. They're cyclic. If the "iff" in (1) and the "is" in (2) do indeed indicate logical equivalence, logical equivalence needs to be defined formally. One definition I found is $$\left(p \dashv\vdash q\right) \text{ iff } \left(\left(p\iff q\right) \text{ is a tautology } \top\right) \qquad \text{(3)}$$ The first thing I noticed off the bat is that logical equivalence uses itself in its own definition. I interpret $\left(\left(p\iff q\right) \text{ is a tautology } \top\right)$ to mean $\left(\left(p\iff q\right)\dashv\vdash\top\right)$, but that would mean the definition refers to itself. Maybe I'm interpreting the "is" wrongly?

   Another possible definition I've seen is $$\left(p \dashv\vdash q\right) \text{ iff } \left(\left(p\vdash q\right) \land \left(p \dashv q\right)\right) \qquad \text{(4)}$$ which again, syntactically, I have another problem with because it uses the $\land$ operation for propositions, call it material conjunction, to connect two statements (unless there is a second interpretation to "and" that allows it to operate on two statements... call it logical conjunction, which hasn't been defined).

   Semantically, $\dashv\vdash$ cannot use $\vdash$ and $\dashv$ in its definition because the definitions of $\vdash$ and $\dashv$ use $\dashv\vdash$ (see (2b)).

One more thing, how does this all relate to the logical consequence $P \models Q$ ?

Answer 1

Your comment in 2. resolves your worries in both 1. and 2.. The "iff" is in neither case a relation between propositional variables in the formal language. Rather, it's a relation between English sentences, that is sentences in the metalanguage—our language—which happen to talk about sentences of another object-level language. But the "iff"s are used slightly differently in the two cases.

In case 1., there's two options. On the one hand, the "iff" can be read definitionally, meaning we're just treating one side as an abbreviation for the other side. That is, we're saying "We'll write "$p \rightarrow q$" as a notational variant of "$\neg p \vee q$"." Alternatively, we could take "$\rightarrow$" as a primitive symbol along with "$\vee$", in which case the "iff" can be read as the logical equivalence relation between propositions in the formal language, i.e. as saying "$p \rightarrow q \dashv \vdash \neg p \vee q$."

In case 2., the "iff" is being used to state the logical equivalence of two statements in the metalanguage, i.e. the metalogical equivalence between the statement "$p \vdash q$" and "The formal sentence "$p \leftarrow q$" is a tautology."

As for case 3., you're right that our notion of logical consequence ($\vdash$) and our notion of tautology are closely interconnected. But you could simply rephrase the claim in 3. as "$p \dashv \vdash q$ iff $\vdash p \leftrightarrow q$." Then the question just boils down to defining what we mean by "$\vdash$", which is often done either via truth tables (in the case of propositional logic), or via some proof system. In either case, you can find an explication in any reasonable introductory book.

Two things should be noted. The first concerns our use of "$p \vdash q$". This sentence is an English-level sentence, not a sentence in the formal language itself. Thus, "$p \vdash q$" means "The formal proposition "$p$" entails the formal proposition "$q$" in the given formal logic." So if we ever happen to say, "$p \vdash q$ iff...", that's an immediate indication we're talking about an equivalence between sentences of English, not sentences of the formal language.

Second, to answer your worry in 2., yes we do have to appeal to a prior notion of a meta-logic in order to set out a formal theory of logic. And, in fact, if you change the metalogic, certain theorems/proofs also change regarding the formal theory of logic. So the metalogic you assume is crucial to setting out a formal theory of logic. Nevertheless, the fact that we have to appeal to one doesn't invalidate the study of logic. After all, the whole point of devising a formal theory is to better understand how the actual thing behaves, and to understand anything, we need to use some logic.