# What is a local inference system?

A inference system is a set of rules that can be used to prove something in some formal model. I understand that.

But what does it mean to a inference system to be local?

For instance, in the page 36 of these MPRI notes there is the following definition:

Definition 4.2 (locality) Let $I$ be an inference system. The system $I$ is local if whenever $T ⊢ u$ in $I$, there exists a proof $\Pi$ of $T ⊢ u$ such that $Steps(\Pi) \subset st(T \cup \{u\})$.

But I am not able to understand this definition because even if I know that $st(T\cup\{u\})$ is the set of subterms of $T \cup \{u\}$, I don't know what is $Steps(\Pi)$.

$\mathsf{Steps}(\Pi)$ is defined just above, in the paragraph below Definition 4.1. It's the set of node labels in the proof, i.e. the set of propositions that are proved as lemmas in that proof.
Thus a local inference system is a set of propositions such that every deduction $T \vdash u$ can be proved from lemmas that only involve terms that are subterms of the proposition $u$ or of the premises $T$.
• So, in the tree presented in example 4.2, do we have $Steps(\Pi) = \{a, b, (a, b) \}$ ? – Hilder Vitor Lima Pereira Mar 9 '16 at 12:45
• @Vitor The label is the conclusion, e.g. $u$. In Example 4.2, there's also $\textsf{senc}(s, \langle a, b \rangle)$ and so on. – Gilles 'SO- stop being evil' Mar 9 '16 at 13:30
• Ok, the conclusions of each node. Got it. And the subterms of $T \cup \{u\}$ would be just $\{(senc(s,(a,b)), a), senc(b,a), s\}$ in this example? – Hilder Vitor Lima Pereira Mar 9 '16 at 13:36
• @Vitor Also $a$, $b$ and $\langle a,b\rangle$. – Gilles 'SO- stop being evil' Mar 9 '16 at 13:38