cyclic definitions of material/logical implications

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$ ?

• perhaps this iff for the case of (1) means that depending on the values of p and q, $p\implies q$ should have preciesly the same value as $\lnot p \lor q$? And the iff in (2) means that you simply define $(p⊢q)$ that way, e.g. when you say, a function is continuous if ( ... some stuff...). You might say, a function is continuous iff ( ... some stuff...), but that's just the same, you simply define this previously unknown notion of continuity. So it's a kind like, you might establish logical equivalence between things which meanings you know, and this thing has its own definition
– W_D
Jul 26, 2013 at 7:04
• but here you're a kind of saying, this notation will mean preciously the thing after the "iff" word. That's how i understand that
– W_D
Jul 26, 2013 at 7:05

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.