As far as I know, most of mathematical logic textbooks state the Weakening Lemma:
Let $L$ be a first-order language.
Then, for any sets $\Gamma_1$ and $\Gamma_2$ of $L$-formulas and any $L$-formula $\varphi$,
if $\Gamma_1 \subseteq \Gamma_2$ and $\Gamma_1 \vdash \varphi$ then $\Gamma_2 \vdash \varphi$.
I tried to prove it by induction on $\Gamma_1 \vdash \varphi$.
But there was a serious issue with $\forall\mathrm{I}$.
To explain it, let me introduce some notations:
- $\mathrm{FV} \left( X \right)$ denotes the set of all free variables in $X$;
- $\left[ t / x \right] A$ is a substitution instance of $t$ for $x$ in $A$.
I stated $\forall\mathrm{I}$ rule as follows:
$$ \frac{\Gamma \vdash \left[ y / x \right] A}{\Gamma \vdash \left( \forall x \right) A} $$
provided by $y \notin \mathrm{FV} \left( \Gamma \right)$ and $y \notin \mathrm{FV} \left( \left( \forall x \right) A \right)$.
Since $\Gamma_1 \subseteq \Gamma_2$,
$\mathrm{FV} \left( \Gamma_1 \right) \subseteq \mathrm{FV} \left( \Gamma_2 \right)$.
But I had only condition $y \notin \mathrm{FV} \left( \Gamma_1 \right)$.
So I couldn't show $y \notin \mathrm{FV} \left( \Gamma_2 \right)$,
which must be shown.
And then I conjectured that this is a counterexample:
$$ \Gamma_1 \vdash \left( \forall v_1 \right) v_1 = v_1 \;\not\!\!\!\!\implies \Gamma_2 \vdash \left( \forall v_1 \right) v_1 = v_1 $$
where $\Gamma_1 = \emptyset$ and $\Gamma_2 = \left\{ \, v_i = v_i \, | \, i \in \mathbb{N} \, \right\}$,
$v_i$ is the $i$-th individual variable.
Therefore, I concluded if my $\forall\mathrm{I}$ rule was right then the Weakening Lemma for first-order logic wouldn't hold.
I surveyed former researches on formalizing meta-theorems for first-order logic.
But there were only researches dealing with natural deduction $\Gamma \vdash \varphi$ in which $ \Gamma $ is a list not a set,
i.e., $\Gamma$ is always finite.
They did not consider when $\Gamma$ is infinite,
and their methods were not applicable in case $\Gamma$ is possibly infinite.
So my question is what type $\Gamma$ is of:
-
List (which is necessarily finite); or
-
Set (which is possibly infinite)?
If vdash is of the type list formula -> formula -> Set (as a Coq type),
then how can we play PA or ZFC, etc.?
I've already asked a related question.
Best Answer
I can't give you one single answer to this question, because you have many possibilities, depending on how you wish to formalize things.
Some of these choices work better than others depending on your choice of metatheory, and even on your choice of proof assistant. For example, infinite sets will work much more smoothly in Isabelle/HOL than in Coq. A lot of proof assistants also come with name binding systems that you can reuse (see Kristensen in Twelf), or HOAS facilities (see Xu in Agda albeit for a sequent-style system). Certain choices can make your job much harder later on, depending on what exactly you wish to prove.
In any case, what you've been doing is too naive and, as you noticed, doesn't work for infinite sets. I enumerate a few alternative options below.
Option 1
You can define $\Gamma$ as an infinite set of formulae in a finite set of free variables.
One could argue that this solution is closest to the "intentions" of first-order logic. First-order theories constitute sets of sentences (not sets of proper formulae) anyway, and this solution allows you to have just enough proper formulae to handle anything that occurs in usual syntax and semantics, and to choose a fresh variable whenever you need to.
In Coq, thanks to dependent types, you may even keep track of the finite set of free variables in use directly inside the type of $\Gamma$, which comes in handy when you need to pick a fresh variable, or when you need to keep track of the sorts of the variables in many-sorted first-order logic. This is known as maintaining a variable context.
Option 2
Keep $\Gamma$ as a finite list. For first-order logic, this is a perfectly viable solution, and the preferred one when dealing with sequent systems in textbooks. Since you have finitely many formulae in your list, you have a finite set of free variables in use, and so you can always choose a fresh one.
How do you deal with infinite theories? Simply by defining $T \vdash \varphi$ for a theory $T$ as "we can find a finite set of formulae $\Gamma\subseteq T$ such that $\Gamma \vdash \varphi$", and defining a theory in turn as a (potentially infinite) set of sentences.
This is perfectly adequate: results about infinite $\Gamma$ are usually not very interesting proof-theoretically, except for the case of theories. And depending on what you want to do (e.g. Gentzen-style study of Peano arithmetic), you might want to define your theory using further rules, rather than infinite sets of sentences, anyway.
Option 3
Implement proper renaming. The reason you have a counterexample to weakening is that you can choose $\Gamma$ large enough that no fresh variable remains, leaving you with no way to invoke the $\forall I$ rule.
Arguably, you should let the quantifier rules do variable maintenance, i.e. give the invocation of these rules the ability to rename all free variables. This allows you to use the Hilbert hotel tricks to free up a variable on demand. You will have to implement and reason about substitution if you take this path, though.
Which one to choose?
Quite possibly none of the above. As I explained, the choice depends strongly on what you want to prove, and some trial and error tends to precede the final decision, with false starts (like the one you had) being common. Books and treatises are regularly written on naming and alpha-equivalence, for good reason.
It's best to find existing implementations, see what they did, and start from there. I linked some of these in the text, but there's a Proof Assistants stack exchange: I'm sure they'll produce an extensive list of existing natural deduction implementations if you ask a question.