Inference rule and soundness I am kind of newbie in the logic field and I have some difficulties linked to soundness and completness concepts.
Let's consider a domain composed of :


*

*A set of libraries $L = \{l_1, l_2, l_3\}$,

*A set of books $B = \{b_1, b_2, b_3\}$,

*A set of users $U = \{u_1, u_2, u_3\}$;


and the following relations:


*

*$P(x, y)$ with $x \in L$, $y \in B$ that stands for "The library $x$ has the book $y$" ;

*$Q(x, y)$ with $x \in U$, $y \in B$ that stands for "The user $x$ rents the book $y$" ;

*$R(x, y)$ with $x \in U$, $y \in L$ that stands for "The user $x$ is a member of the library $y$".
We introduce the following rule that stands for "If a library has a book and a user rent it, then this user is a member of this library"
$\forall l \in L, \forall b \in B, \forall u \in U, P(l, b) \land Q(u, b) \implies R(u, l)$
We assume that $P(l_1, b_2)$ and $Q(u_1, b_2)$ are both true. Can we prove syntaxically that $R(u_1, l_1)$ is true? 
$R(u_1, l_1)$ is definitively valid because the deduction mechanisms involved are logically correct (modus ponens). Consequently, to prove that this statement is true, we have to prove that its premises are true. By definition, $P(l_1, b_2)$ and $Q(u_1, b_2)$ are true but what about our own rule: $\forall l \in L, \forall b \in B, \forall u \in U, P(l, b) \land Q(u, b) \implies R(u, l)$? Can we demonstrate that this rule is true or are we forced to accept it as an axiom ?
If we are in a logic system that is sound and complete and if we add this kind of rule, is the system still sound and complete?
Thanks
 A: The answer to your first question is simply no, we cannot prove any of these premises are true; all of them must be taken as givens, or "axioms" in order to derive the conclusion $R(p_1, l_1)$. These premises are akin to "empirical facts", facts we happen to know to be true about librarians, books, people, and their relations to one another. (Side note: The fact that you use the letter "$P$" as both standing for the set of people and standing for a relation between librarians and books is potentially confusing; you'd be better off choosing a different letter, or adding a ' somewhere.)
A proof system is said to be sound if it cannot derive sentences that aren't valid (pardon the double negative), i.e. it can only derive sentences that are valid. If you added your premise, $\forall l \in L, \forall b \in B, \forall p \in P, P(l, b) \land Q(p, b) \implies R(p, l)$, as a rule, i.e. a rule of the proof system, then your proof system would cease to be sound, as this isn't always true (part of the confusion lies in your use of $L$, $B$, and $P$; these can't occur in the sentence unless they are predicate letters. But if they are, then your association of these letters to their respective sets is arbitrary, and can easily have been chosen differently to invalidate the sentence above.)
A: It sounds like you have some confusion over the difference between inference rules and statements.  An inference rule is a way of deducing statements from other statements.  A statement is something which can be true (or false, or something else, depending on what language you use).  So, for instance, Modus Ponens (From "$A$" and "$A \longrightarrow B$" deduce "$B$") is an inference rule, while "For all $x$, $x = 0$ or $x \neq 0$" is a statement.
Of course, confusion can result because, in some logical systems (such as everyday speech or higher-order logic), inference rules can be "equivalent to" statements.  For instance, in higher-order logic, an equivalent formulation of Modus Ponens would be the statement "For all predicates $P$ and $Q$, [$P$ and $(P \longrightarrow Q)$] $\longrightarrow Q$".
The reason that I cite confusion is that you refer to your "rule" as both an inference rule and a possible axiom; an axiom is a statement, not a rule.  The answer to your questions depend on whether you really want your "rule" to be a rule or a statement.
In the case that you want it to be an inference rule, then see Alex Kocurek's post for your answers.
In the case that you want it to be a statement, then the answer is "it depends".  Now, instead of talking about sound and complete logic systems, I think that you actually want to talk about sound and complete formal theories.  Basically, a theory is a set of statements (not rules) that you accept as axioms, in order to see what statements can be deduced from those axioms.  Note that the axioms do not have to valid in general for a theory to be useful: for instance, group theory is a useful theory even though the group theory axioms aren't true of every mathematical object.  Thus, the group theory axioms are "sound" when considered as a theory but unsound when considered as a set of inference rules.

Although there is no definition of soundness for theories, there are related concepts.  Generally, a theory is said to be consistent if its axioms do not contradict each other.  So, if you add your "rule" to a consistent theory as an axiom, then the resulting theory will be consistent if and only if your "rule" does not contradict the existing theory.
Generally, a theory is said to be complete if, for every statement $\alpha$ in the language, either $\alpha$ is true in the theory or $\neg \alpha$ is true in the theory.
So, if you have a consistent and complete theory, then your "rule" will already be either true or false in the theory.  If your "rule" is true in the theory, then adding it will do nothing and the theory will remain consistent and complete; if your rule is false in the theory, then adding it will make the theory inconsistent.
