I have formalized meta-theories for first-order logic with the Coq Proof Assistant. I defined rule (${\forall}$I) by: $$ \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)$; where $x$ is an individual variables and so is $y$, $A$ is a well-formed formula, $\Gamma$ is a set of well-formed formulae, $\mathrm{FV} \left( X \right)$ denotes the set of all free variables occur in object $X$, and $[t/x]\varphi$ is substitution of $t$ for $x$ in $\varphi$.
And then, I have tried to find a formal proof of the monotonicity property, i.e., $$ \Gamma \vdash C \, \mathrm{and} \, \Gamma \subseteq \Gamma^{\prime} \implies \Gamma^{\prime} \vdash C . $$ However, if $\Gamma^{\prime}$ is of a set but not a list, it is failed for me to find an individual variable $y^{\prime}$ such that $y^{\prime} \notin \mathrm{FV} \left( \Gamma^{\prime} \right)$ and $y^{\prime} \notin \mathrm{FV} \left( \left( \forall x \right) A \right)$, because $\mathrm{FV} \left( \Gamma \right) \subseteq \mathrm{FV} \left( \Gamma^{\prime} \right)$ .
Actually, letting $v_i$ denote the $i$-th individual variable, there is a counter example: $$ \emptyset \vdash \left( \forall v_1 \right) \left( v_1 = v_1 \right) \;\not\!\!\!\implies \Gamma \vdash \left( \forall v_1 \right) \left( v_1 = v_1 \right) $$ where $\Gamma := \left\{ v_i = v_i \, | \, i \in \mathbb{N} \right\}$.
So, I am considering a plan: when proving a meta-theory of first-order logic, I add the constraint on $\Gamma$ in the statement of the meta-theory, for which has countably infinite free-variables and is denoted by $\mathbf{P} \left( \cdot \right)$. If it is accetable, for an example, the statement of the monotonicity property will be $$ \Gamma \vdash C \, \mathrm{and} \, \Gamma \subseteq \Gamma^{\prime} \, \mathrm{and} \, \mathbf{P} \left( \Gamma^{\prime} \right) \implies \Gamma^{\prime} \vdash C . $$
However, I have not found any textbook in which such a constraint is defined or used. I have two questions:
- I wonder if the above statement is considered okay in terms of many mathematicians.
- Furthermore, my question is whether the plan is acceptable or not.
On Oct 9, 2023, the original question was:
Title: How can I prove the Monotonicity property of Natural Deduction?
I'm working on making another framework for 1st-order Logic in The Coq Proof Assistant.
I stated $\dot{\forall}$-intro rule: for any set of formula $\Gamma$ and any formula $C$ and any individual variable $x$ and $y$, if $\Gamma \vdash C \left[ y / x \right]$ then $\Gamma \vdash \dot{\forall} x , C$ provided by $y \notin \mathrm{FV}\left(\Gamma\right)$ and $y \notin \mathrm{FV} \left(\dot{\forall} x , C \right)$, where $\varphi \left[ t / x \right]$ denotes the result substituting $x$ for $t$ in $\varphi$.
To prove the Monotonicity property, I struggled with the condition $y \notin \mathrm{FV} \left( \Gamma \right)$. Assume $\Gamma \subseteq \Delta$ and $\Gamma \vdash C$. Then, to prove $\Delta \vdash C$, it is required to assume $\mathrm{FV} \left( \Gamma \right) = \mathrm{FV} \left( \Delta \right)$.
So I wonder that the $\dot{\forall}$-intro rule is correct. If so, how can I prove the property?
Or, how can I state again correctly if it is wrong? Since I've already proved the soundness theorem of Natural Deduction for the Tarski's semantics, I hope it correct.
Proving the following Extraction Lemma requires the Monotonicity property:
where p⟦ x ↦ t ⟧ denotes $p \left[ t / x \right]$.