There might be a difference if we permitted the domain of quantification to be empty; then it might be that every $x$ --- all none of them --- is such that $Fy$ even though $Fy$ itself isn't true. If we discuss "free logics" later in the semester, this will be something we return to. In mainstream orthodox logics, though, we assume that the domain of quantification isn't empty, and that every term constant or variable can be associated with some object in the domain.

Similarly, in my example $\forall x(\exists x Fx)$, the $\forall x$ doesn't bind any occurrences of $x$. Quantifiers that don't bind any free variables are called **vacuous**.
For more discussion of these various notions in this week's readings, see Sider pp. 90--91; Bostock pp. 78--79; and Gamut pp. 74, 76--77.
What do we say about the *first* $x$ in the string $\exists x Fx$, the one immediately after the $\exists$? People are all over the map about this. Some authors say that is another occurrence of the variable $x$, and that it's bound. Others say it's neither bound nor free. Others say it's not even an occurrence of the variable $x$. I prefer this last way of talking, but as I said there is lots of variation here. Perhaps best just not to speak of it.
In expressions like:
> $\forall x(Gx \wedge \exists xFx \wedge Hx)$
and:
> $Gx \wedge \exists xFx \wedge Hx$
we say that the binding or assignment had by $x$ in the outer expression gets **shadowed by** the quantifier $\exists x$, which rebinds $x$ for its own use in the subformula $Fx$. The interpretation $x$ has in the outer scope is no longer visible inside the scope of the $\exists x$. This is perfectly legitimate, but as we'll see below, it does introduce some complexity when we're thinking about what it is to substitute one expression for another within a larger expression.
There are some alternate notations for quantification where this kind of phenomenon just can't arise. I may mention them later in the term.
6. Most everyone thinks $\horseshoe$ is a bit weird when they first encounter it. If you still feel that way, and you have restricted quantification as a primitive in your language, you might think of $\phi\horseshoe \psi$ as defined by $\forall x\colon \phi. \psi$, where $x$ doesn't occur free in $\phi$ or $\psi$. That will be true if all the $x$s such that $\phi$ (which will be all the objects if $\phi$ is true, or no objects if $\phi$ is false) are such that $\psi$. In other words, just in case $\phi$ is false or $\psi$ is true: which is just the meaning of $\phi \horseshoe \psi$.
There are some interesting contexts in logics *weaker* than "classical" logic where you want a truth-functional conditional that's *not* equivalent to the one just explained. But here we're getting to the limits of what I understand well.
7. We'll sometimes have to talk about the result of **substituting** some expression $\tau$ in place of another expression $\sigma$ in a larger expression $E$. For discussion, see Sider p. 100; Bostock pp. 80--81; and Gamut pp. 78, 99--100.
A variety of notation is used to express this. Commonly authors will say something like $E[\tau/\sigma]$, with the idea being that you "divide out" the free occurrences of $\sigma$ from $E$ and replace them with $\tau$. But sometimes the $E$ comes after the $[\tau/\sigma]$, sometimes the $\sigma$ comes on top rather than the bottom(!), and sometimes the notation looks rather different than this. I find this very frustrating. I've adopted a notation that, while not already in widespread use, at least has the advantage of being very difficult to misunderstand. I will say:
> $E[\sigma \leftarrow \tau]$
to mean the result of substituting $\tau$ for all free occurrences of $\sigma$ in $E$.
You have to be careful when doing this. Let $E$ be the expression:
> $Fxy \wedge \exists y Gxy$
Now suppose we want to generate $E[y\leftarrow x+1]$. Only the first occurrence of $y$ should then get replaced, because the last occurrence is bound by the quantifier $\exists y$. Suppose instead we want to generate $E[x\leftarrow y+1]$. Here the last occurrence of $x$ is *free*, so it *should* be replaced. But if we simply replace the $x$s with $y+1$, we'd get:
> $F(y+1)y \wedge \exists y G(y+1)y$
which isn't correct. For there we'd have introduced a new variable binding (the $\exists y$ will bind the $y$ in $y+1$) that we shouldn't have. Instead, we want to perform substitution in a way that doesn't introduce any new "free variable captures". We have two choices about how to handle this. First, we could simply declare the result of a substitution
> $\dots[x\leftarrow \tau]$
into a subexpression
> $\exists y \dots$
where $x$ occurs freely to be undefined when $\tau$ contains free occurrences of $y$. Alternatively, we could say that the substitution *is* defined, but introduces a renaming of the bound variable in $\exists y \dots$ to some new variable not occurring in $\dots$ and not occurring free in $\tau$, like so:
> $F(y+1)y \wedge \exists z G(y+1)z$
Some authors take a different strategy. They say that $(\dots\exists y Gxy)[x\leftarrow y+1]$ *is* defined to be $ $\dots\exists y G(y+1)y$, it's just that $y+1$ doesn't count as being **substitutable for x** in that original expression. These authors then have to qualify various rules and claims they make with the proviso that the term being substituted is substitutable in the relevant ways. It's much more straightforward to just define the substitution operation so that these provisos aren't needed.

As I said at the end of point 5, there are some alternate notations for quantification where these kinds of difficulties can't arise.
8. Bostock and Sider both work with a minimal set of logical operators, rather than the full range you may be familiar with. There are multiple ways to choose a minimal set (but not every choice is equally expressive). It's even possible to have only a single operator.
If I had to choose, I'd choose $\horseshoe$ and $\neg$ (or $\horseshoe$ and $\bot$) as primitives, because these make it easiest to compare "classical" logic with some weaker systems. Sider already tells you (p. 27) how to define some other operators in terms of these:
> $\phi \wedge \psi$ is short for $\neg(\phi\horseshoe\neg\psi)$
> $\phi \vee \psi$ is short for $\neg\phi\horseshoe\psi$
Some other definitions one can use:
> $\phi \vee \psi$ is short for $(\phi\horseshoe\psi)\horseshoe\psi$
> $\neg\phi$ is short for $\phi\horseshoe\bot$
If you're ever working in a "non-classical" logic, you'll have to take special care about which of these "definitions" still give intuitively correct results.
For the most part, I won't be choosing a minimal set of operators. We'll take the whole familiar range of operators as primitives, even the term literals $\bot$ and $\top$, which always get interpreted as being false, and true, respectively. (I won't talk about $\mathrm{xor}$, though, as there's too much variation in what notation to use for it.)
Also, when we talk about *predicate* logic, I'll assume we nonetheless still have *sentence* constants like $P$ and $Q$ in the language (as well as the literals $\bot$ and $\top$), not just predicate constants like $F$ and $G$. As I've said in our meetings, you can think of the sentence constants as though they were 0-adic predicate constants (see Bostock p.75). And you can think of term constants like $a$ and $b$ as though they were 0-adic functors. (A **functor** is a symbol like $+$ that designates a function, in the way that a predicate designates a property or relation.)
When we shift to talking about *logical* properties of our languages, we will consider what is invariant across changes of meaning to all the non-logical constants in the language, and also changes to the domain of quantification when the language has quantifiers. But we don't change the meaning of logical operators like $\vee$ and $\horseshoe$. Neither do we change the meaning of $=$ or $\bot$ or $\top$. That is why I tend to call the latter predicate and term **literals**, rather than just **constants**.
You may ask: on what grounds is it decided whether to count something as a *logical* symbol (or literal) rather than a non-logical one.
That's an *excellent* question. We will make no effort to answer it. Instead, for this class, we'll just be uncritically following the existing conventions.
Those existing conventions include treating symbols like $0$, $+$, $\lt$, $\in$, and so on as *non*-logical constants, not logical symbols or literals like $\vee$, $\horseshoe$, $\bot$, and $=$ are. If you want to constrain the meanings of $0$, $+$, $\lt$, or $\in$, you need to do so by adding *extra-logical axioms* to your system, and talking about your **theory** of so-and-so, rather than thinking these constraints will be imposed by your *logic*. As we'll discuss later, a theory in the sense of this class is just a set of sentences, closed under provability in some background logic. (These will generally be *terrible* "theories" by the lights of philosophers of science.)
9. When one is specifying what logic one wants to talk about, it should be clear whether it has a "classical" semantics or something weaker or stronger (or just different). It should also be clear what logical symbols are present, in particular whether quantifiers are present and whether $=$ is present. (If other binding-devices like $\lambda$ or $\desc$ are present, that should also be clear.)
The term **signature** is used to describe what range of *non*-logical predicates (of whatever adicity), functors (of whatever adicity), and term constants (or functors of adicity 0) are available in a logic's language. Signatures that have no non-logical predicates of adicity greater than 1 are sometimes called **algebraic**; these signatures may include $=$ and functors of whatever adicity. If you review our discussions of algebra, you'll see we talked in terms of belonging to this-or-that set (which can be treated as a monadic predicate), operations (functors), and equalities, rather than any other relation.