Use of contexts in formal proofs

I have the idea that a formal system is defined by a set of inference rules that can be used to extend a finite set of theorems starting from the axioms. If I look at the wikipedia page or if I ask on stackexchange I see that people use a more relaxed definition of inference which requires the use of some kind of context or nested proof. For example to prove $$P\implies Q$$ one creates a context where $$P$$ is assumed to be true, then operates in this context until is able to prove $$Q$$. Then one can deduce $$P\implies Q$$ outside the context.

In the wikipedia page this is explained saying that $$P\implies Q$$ can be derived from $$P \vdash Q$$. I cannot fully understand how this can be turned into a formal definition. If I take it literally it requires to formally define $$P \vdash Q$$. I think that it is of fundamental importance to know if the inference rules are computable (so that a computer can make a formal proof verification). So it is very important to explain which is the algorithm to check if $$P\vdash Q$$. I think that in general there is not such an algorithm (in view of Turing's Theorem) hence I think that $$P\vdash Q$$ should not be used in defining the inference rules of a formal system. Am I wrong?

I can instead understand how the use of context could be formalized. However the introduction of contexts makes inference rules much more complicated since every theorem must be associated to the context where it was proven. So I can imagine that $$P\implies Q$$ can be added to the set of theorems in a context if there is a sub-context where $$P$$ is taken as an axiom and $$Q$$ is a theorem. This explains the algorithmic bit that was missing in the previous approach.

Now, finally, the point of my question. Why don't we simply prepend each theorem in the context with the assumptions of the context? In the case where the context has the proposition $$P$$ added as an axiom we could simply replace each theorem $$T$$ with $$P\implies T$$ and avoid the use of contexts. The only problem being that the formal inference rules should address this: for example we cannot simply say that $$Q\land Q$$ can be derived from $$Q$$. We should say that also $$P\implies (Q\land Q)$$ can be derived by $$P\implies Q$$ since $$P\implies Q$$ can be viewed as the theorem $$Q$$ in the context where $$P$$ holds.

Clearly the use of contexts seems easier to understand and is what usually mathematicians do in everyday life. But I would say that using contexts in the formal definitions is hiding some of the formal difficulties (among which the restrictions on the usage of free and bounded variables). So I wonder if there is some discussion of these issues and in case if there is some exposition of propositional logic, predicate logic, or set theory which is context free.

• The tag context-free-grammar does not seem appropriate. Commented Jul 23 at 13:06
• Re your linked question, in that case the "context" is the derivation: outside it, free variables have no meaning. Specifically, the proof start from axiom $\forall x (x=x)$ and the following step instantiates it to $(a=a)$. This is correct whatever $a$ is: either or variable or a constant, because the axiom states that reflexivity holds ALWAYS. This means that e.g. in the case of arithmetic we are licensed to derive $(0=0)$ and so on. Nitpicking issue: what you call "predicates" are "open formulas" i.e. formulas with free occurrences of variables. Commented Jul 23 at 14:13
• This answer might be of help to you. Commented Jul 23 at 18:06
• I recommend you get familiar with one precise formulation of a formal proof system, such as Fitch-style natural deduction as presented in forallx.openlogicproject.org/html/Ch17.html. Then it will be easier to see how subderivation etc can be defined in any particular system and how it translates to other notational systems. Or at least it will be easier to ask more targeted questions, because there is not the precise answer you're seeking in the broad set-up you're asking. Commented Jul 24 at 1:24
• Re. your last suggestion, sounds like you're looking for sequent calculus. What Gentzen called "sequent" and Wikipedia calls "conditional tautology" just means "proof with context" in your words, and noting in each derivation step the context in which a formula was proved is exactly what sequent calculus does. Commented Jul 24 at 4:35