What is the difference between proving something for an arbitrary object and proving something using a universal quantifier?

Question

I think I am a little out of my depth in asking this question, but I'll give it a go.

I am having trouble distinguishing between proving something for an arbitrary object of some type (something that I believe can be 'encoded' in sentential logic), which then generalizes to all objects of the same type, and proving something using a universal quantifier (which I believe can only be encoded in predicate logic).

I came across this issue, in particular, when I tried proving the Deduction Theorem. Firstly, some necessary background:

In the book "Model Theory", the "...notion of a formal deduction in [the] logic $\mathscr S$" is introduced in the following paragraph:

The Rule of Detachment states: From $\psi$ and $\psi \rightarrow \varphi$ infer $\varphi$. Now consider a finite or infinite set of $\Sigma$ of $\mathscr S$. A sentence $\varphi$ is deducible from $\Sigma$, in symbols $\Sigma \vdash \varphi$, iff there is a finite sequence $\psi_0,\psi_1,...,\psi_n$ of sentences such that $\varphi = \psi_n$ and each sentence $\psi_m$ is either a tautology, belongs to $\Sigma$, or is inferred from two earlier sentences of the sequence by detachment.

In my book, the Deduction Theorem for sentential logic is posed as follows:

If $\Sigma \cup \{\psi\} \vdash \varphi$, then $\Sigma \vdash \psi \rightarrow \varphi$

Firstly, by completing this proof, aren't I really saying the following?

$\forall \Sigma, \forall \varphi, \forall \psi$ $ \ \ $ If $\Sigma \cup \{\psi\} \vdash \varphi$, then $\Sigma \vdash \psi \rightarrow \varphi]$

This, in and of itself, is already confusing because it seems like I am utilizing a higher order logic system's terminology in order to describe a result from a lower order logic system.

---

Secondly, consider the proof for the Deduction Theorem ( provided here https://proofwiki.org/wiki/Deduction_Theorem) that is depicted below. Note that the language is slightly different...the change in notation is:

If $U, A \vdash B$, then $U \vdash A \rightarrow B$

I have marked in $\color{red}{\text {red}}$ the line that is causing me some grief.

After completing the base case for $n=1$, the proof states (implicitly) that our hypothesis case is:

Assume for a proof of size $n$ (i.e. $\theta_1 \theta_2...\theta_n$ where $\theta_n = B$) $\ \ \ $ If $U, A \vdash B$, then $U \vdash A \rightarrow B$.

In the $n+1$ step, the proof invokes the hypothesis in order to stipulate that:

1. $U \vdash A \rightarrow C$
2. $U \vdash A \rightarrow (C \rightarrow B)$

Once again, this suggests to me that our hypothesis is actually of the form:

For a proof length of size $n$, $\forall U, \forall A, \forall B \ \ \ \ $ If $U, A \vdash B$, then $U \vdash A \rightarrow B$

In this case, we are using concepts from a higher order logic system to facilitate the acquisition of a result in a lower order logic system (which seems a little fishy to me).

Am I misunderstanding something here?

Cheers~

Answer 1

For quantifiers, see Universal generalization:

(aka: Universal Introduction) is a valid inference rule. It states that if $\vdash P(x)$ has been derived, then $\vdash \forall x\,P(x)$ can be derived.

It amounts to the formal counterpart of the intuitive inference: "what holds for any, holds for all".

Thus, regarding the title question:

What is the difference between proving something for an arbitrary object and proving something using a universal quantifier?

the answer is: we prove that the "universal generalization" of a property holds proving it for something arbitrary.

The Deduction Theorem is a meta-theorem, i.e. a result about the proof system. Thus, it is a "piece" of standard mathematics and not an expression of the formal system.

As often in modern mathematics, it uses a jargon that is a mixture of natural language ("if..., then...") and symbols ($\vdash$).

As often in mathematics, universal quantifier are implicit.

The theorem holds, for every set of formulas $\Sigma$ and every pair of formulas: $\varphi, \psi$ of the language.

Thus, regarding again the title question, we may say that:

there is no difference between asserting something for an arbitrary object and asserting it using a universal quantifier.