In Fitch, is a symbol not in a specified language automatically free?

In Fitch proofs where no language has been specified, we (at least seem to) treat lines that have the form

$$p(x)$$

to mean that $x$ "can be anything". That is they are equivalent to

$$\forall x.p(x)$$ where $x$ has no specified constraints.

However, it isn't clear to be how to handle the corresponding line in a proof with a specified language. For example, given a language $\Delta$ with terms $a$ and $b$, and relation constants $p$ and $q$, it is clear that I might (depending on the premises) be able to conclude things like

$$p(a)$$ $$q(b)$$

but (again assuming premises that produce them) can lines like

$$p(c)$$

or

$$q(x)$$

ever be valid inferences? If so, do they mean "where $c$ or $x$ is either $a$ or $b$"?

For example, if I have $\Delta$ as above, is it valid to say

1. $\forall z.q(z)\text{ — Given}$
2. $q(x)\text{ — Universal Elimination,1}$

and equally valid (and equivalent) to say

1. $\forall z.q(z)$
2. $q(c)$

even though there is no $c$ or $x$ in $\Delta$?

-

Though we might not always specify the particular language from which expressions and sentences are constructed, there are some general conventions that are often adopted. For instance, $p$, $q$, and $r$, perhaps with subscripts, are often taken as propositional constants, or relation symbols. $f$, $g$, and $h$ are often function symbols. Constants often come from the beginning of the alphabet, e.g., $a$, $b$, and $c$. Variables are often taken from the end, as in $x$, $y$, $z$. Those are some general conventions, but context is necessary for interpretation. If we encounter $\forall b.\phi(b)$, it is clear that $b$ is being used as a variable.

With regard to your last two examples, I'd point out that the guidelines above are for casual use of a Fitch-style systems (e.g., as you'll see in MSE posts!). For a precise formalization of what inferences are valid and what each one means, you'd need to consult the precise formalization of the proof system. The example

1. $\forall x.q(z)$ Given.
2. $q(x)$ by universal elimination 1

could be syntactically correct in some Fitch-style proof systems, but not in others. If the proof system specifies that subproofs for universal introduction and existential elimination also introduce new constant symbols, then (I think) the proof system could get away with specifying that universal elimination can only instantiate universals with ground terms (i.e., with terms that have no free variables), in which case (presuming that $x$ is a variable) $q(x)$ the above would not be a syntactically correct proof. With the second example in which $q(c)$ is inferred from $\forall z.q(z)$, it depends on what $c$ is. Informally speaking, since it is near the beginning of the alphabet, I'd expect that it's a constant symbol in the language, thus a ground term, and thus $q(c)$ is syntactically correct deduction. Formally, it all depends on the formal definition of the proof system.

In Fitch-style systems, subproofs may play a role in determining the use of a name. For instance, while a universal introduction proof could be performed using variables as the "arbitrary individuals", some systems will mark the beginning of a subproof with a new constant symbol that plays the role of the arbitrary individual (or, in the case of existential elimination, the witness).

In general, you won't end up with free variables (or new constant names, or however the proof system handles it) in sentences outside of a subproof. Inside of a subproof, the meaning of the formula depends on where the name came from. For instance, consider the following proof

1. $\forall x.(p(x) \to q(x))$ Given.
• $p(a)$ Assume, with a new individual $a$.
• $p(a) \to q(a)$ universal elimination from 1.
• $q(a)$ conditional elimination from 2 and 3.
• $q(a) \lor r(q)$ disjunction introduction with 4.

What should we say the meaning of line 5 is? $q(a) \lor r(a)$ hasn't been derived as a theorem, since we're still inside the subproof. All we can say about $a$ is that it is an arbitrary individual such that $p(a)$ holds. Then $q(a) \lor r(a)$ may be seen as saying "$q(a) \lor r(a)$ holds for any individual $a$ for which $p(a)$ holds." That explains why we could end the subproof and by a combination of universal and conditional introduction conclude $\forall x.(p(x) \to (q(a) \lor r(a))$.

As to the meaning of, e.g., $q(x)$ and $\forall x. q(x)$ in a system with only constant symbols $a$ and $b$, quantification is typically understood to range over the entire universe of discourse, not just the subset of it identified by constant symbols. For instance, in a first-order language with equality and just one individual constant symbol, $a$, I can write the sentence

$$\exists x.(x \ne a)$$

and find models that satisfy it. If $x$ were only permitted to range over $a$, there would be no way to satisfy that sentence.

So for any symbol $ξ∉\{a,b\}$, $q(ξ)$ and $∀ξ.q(ξ)$, for example, are equivalent and mean "for any symbol $ξ$, regardless of whether it is in $Δ$"? And thus, is the example I added to the original question correct?

The meaning of quantification in first-order logic isn't based on saying something about all the constant symbols of the language, or even all the terms of the language, but rather about the individuals in the domain of a model for the language. A model for a first-order language can be given as a triple $\langle D, \cal V, \cal I\rangle$ where $D$ is a set of individuals (the domain of discourse), $\cal V$ is a mapping from variables to $D$, and $\cal I$ is an interpretation function that maps each variable $x$ to $\cal V(x)$, each constant symbol of the language to an element of $D$, each unary predicate symbol in the language to a subset of $D$, each binary predicate symbol in the language to a binary relation on $D$, and so on. Given a model $\cal M$ and a formula $\phi$, we can determine whether $\cal M$ satisfies a formula $\phi$, i.e., whether $\phi$ is true in $\cal M$, typically denoted $\cal M \models \phi$. The $\models$ relationship is defined recursively. For connectives like $\land$, we have

$${\cal M} \models \phi\land\psi \mbox{ if and only if } {\cal M} \models \phi \mbox{ and } {\cal M} \models \psi$$

For predicates we have, e.g., (recall that the interpretation function $\cal I$ maps each constant symbol to an element of $D$ and each unary predicate to a subset of $D$)

$${\cal M} \models p(t) \mbox{ if and only if } {\cal I}(t) \in {\cal I}(p)$$

Finally, we can turn to quantifications. A universal (existential) quantification is true if and only if the quantified formula is true for every (some) element in $D$. Formally,

$${\cal M} \models \forall x.\phi(x) \mbox{ if and only if } \langle D, {\cal V}', {\cal I}\rangle \models \phi(x)$$

for every ${\cal V}'$ that that differs from $\cal V$ at most on $x$.

The use of $\cal V$ and $\cal V'$ there is a little confusing, but it achieves the desired meaning that $\phi(x)$ is true if the property that $\phi$ expresses holds for every element of $D$.

-
So for any symbol $\xi\not\in\{a,b\}$, $q(\xi)$ and $\forall\xi.q(\xi)$, for example, are equivalent and mean "for any symbol $\xi$, regardless of whether it is in $\Delta$"? And thus, is the example I added to the original question correct? – raxacoricofallapatorius May 1 '13 at 4:10
@raxacoricofallapatorius If some string $\sigma$ isn't a term in the language, then $q(\sigma)$ isn't a formula. When we're using these systems informally, we very much depend on people understanding what it is we're trying to express, and understanding how we're using certain symbols. I updated the answer with some discussion of your examples, and of what quantification in first-order logic means (it doesn't range over terms of the language, but over individuals in the domain of an interpretation). – Joshua Taylor May 1 '13 at 12:01