In the deduction theorem, what exactly is contained in $\Delta$?

Question

In the deduction theorem you'll sometimes see a specific set referred to as $\Delta$ or $\Gamma$ or $U$, as used below:

$$\Delta, A \vdash B \implies \Delta \vdash A \to B$$

I've seen this set $\Delta$ referred to as a set of "assumptions", a set of "hypotheses", a set of "axioms", a set of "non-logical axioms", a set of "postulates", a set of "schemata", etc.

I'm not entirely sure what this means formally, if these are all actually saying the same thing -- but if that's the case and an "assumption" is the same as a "non-logical axiom" I'm not sure how this differs from a regular "axiom" that we normally build right into the system to begin with.

Especially when we define a proof as a sequence of lines $\varphi_1, \varphi_2, \varphi_3, ..., \varphi_n$, where "each line is either an axiom or theorem", I can't tell if this includes non-logical axioms / assumptions, or if we have some special name for the results acquired through modus ponens (are these theorems?). I know a "theorem" for example is composed of axioms and other theorems via logical connectives but I don't know if this includes non-logical axioms or modus ponens results.

Furthermore I don't really know where these assumptions/hypotheses/non-logical axioms "come from" -- if they're invoked out of thin air $\vdash \phi$, or if they may not necessarily be sound/true or what have you.

Can anyone shed some light on this? What's contained in $\Delta$ exactly? Where do they come from exactly? What is each line of a proof allowed to be exactly?

Answer 1

It's just some set of statements, that's it.

Where they come from, you need not be concerned about, unless you apply all of this logic theory to something real, but in logic itself, we don't care where the statements come from, whether they are true, or what they even mean.

Answer 2

$$\dfrac{\Delta, A\vdash B}{\Delta \vdash A\to B}$$

The $\Delta$ is a list of predicates.   The deduction theorem states that if the list $\Delta$ and $A$ does syntactically entail $B$, then you can infer that the $\Delta$ will be a list which syntactically entails $A\to B$.

---

I'm not sure how this differs from a regular "axiom" that we normally build right into the system to begin with.

They are not tautologies built into the proof system but are contingencies made for a particular proof.

---

So if you can show that $A\to (C\to B), C, A\vdash B$ then you may infer that $A\to (C\to B), C \vdash A\to B$