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

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?

• The members of $\Delta$ are arbitrary. – Andrés E. Caicedo Sep 21 '18 at 13:03
• Formulas; in the context of formalized theory, like e.g. first order arithmetic, the arithmetical axioms (the first-order version of Peano's axioms) are in $\Delta$. – Mauro ALLEGRANZA Sep 21 '18 at 13:35
• NO, in the context of e.g. first order set theory, axioms in a derivation are logical axioms, while "mathematical" axioms (e.g. the specific axioms of ZFC) are in the set of assumptions of derivations i.e. in $\Delta$. – Mauro ALLEGRANZA Sep 21 '18 at 13:54
• The complete definition of proof sequence in a formalized theory for $\Delta \vdash \varphi$ is : " a sequence $\varphi_1, \ldots, \varphi_n$ where $\varphi_n=\varphi$ and each $\varphi_i$ is either a logical axiom or a formula in $\Delta$ or derived from previous formulas of the sequence by way of inference rules (e.g. modus ponens)." – Mauro ALLEGRANZA Sep 21 '18 at 13:57
• To your comments: Yes, $\Delta$ typically consists of the non-logical axioms relevant to whatever you are doing (such as the ZFC axioms if doing set theory). I hadn't seen your other comment, so: in a proof each step is either a logical axiom or a non-logical axiom (a member of $\Delta$), or comes from previous steps via the rules of your system (which I suppose up to this point it is just via modus ponens). But you see, theorems are not just axioms "pieced together via connectives", but any statements you can derive from the axioms using the rules of your system. – Andrés E. Caicedo Sep 21 '18 at 14:11

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.

• Doesn't this imply that we can prove things with faulty assumptions in $\Delta$? – user525966 Sep 21 '18 at 16:27
• @user525966 You bet! If I assume that pigs fly, I can prove that pigs fly. But this is exactly why I say that logicians don't care as to what is actually true. They only care about logical entailment. – Bram28 Sep 21 '18 at 16:29

$$\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$$

• That's sort of my question though, what are these "predicates" exactly? I understand what the theorem itself is saying, but my question is more about what $\Delta$ is and its role. – user525966 Sep 21 '18 at 13:32
• Are "contingencies" the same as "unproven assumptions that may be true, may be false"? i.e. something of the form $\vdash \varphi$ but not necessarily sound? – user525966 Sep 21 '18 at 13:36
• "Predicates" sounds strange to me in this context. Are you sure you didn't mean that $\Delta$ is a list of propositions? Or perhaps premises? – Henning Makholm Sep 22 '18 at 0:10
• How is Δ a list of predicates if the context is propositional calculus? – Doug Spoonwood Sep 22 '18 at 10:46