Q:

Building an axiomatic theory

I am using an expert system inferring some logical rules on a knowledge base to produce some new statements. I would like to formalize the logical mechanisms used by the inference engine. As a novice in the logic field, I am not sure of how to do it. After some researches, I come to the conclusion that what I am trying to do is building an axiomatic theory (defining a set of axioms and derives some theorems from them).
So my question is : How to build such an axiomatic theory ? As this is quite a vast question, I have tried to answer it myself, can you confirm me that I am doing it right ?
It appears to me that I need a whole formal system composed of :

A syntax : an alphabet and some grammar rules that defines how to build formulas
A deductive system : some axioms and some inference rules
A semantic : a domain of discourse and an interpretation of the alphabet over this domain

Illustration on a factory example :

Syntax : first order logic alphabet and grammar
Deductive system : an Hilbert system without logical axiom & modus ponens rule of inference & some domain specific axioms (see below)
Semantic : all things of the word as a domain of discourse & an interpretation linked to this use-case (see below)

Let's $D$ denote the domain of discourse and let's $E, P, O \subset D$ respectively denotes the set of all employees, the set of all products and the set of all orders of the factory.
Here are some predicates :

isEmployee(-) : the fact of being an employee that is interpreted by the set $E \subset D$ ;
isProduct(-) : the fact of being a product that is interpreted by the set $P \subset D$ ;
isOrder(-) : the fact of being an order that is interpreted by the set $O \subset D$ ; 
CraftableProduct(-) that maps to products that can be manufactured (subset of $P$) ;
AchievableOrder(-) that maps to orders that can be realised in the factory (subset of $O$) ;
EknowsP(-,-) that maps to a subset of $(E \times P)$ interpreted as the fact that an employee knows how to craft a product ;
OcontainsP(-,-) that maps to a subset of $(O \times P)$ interpreted as the fact that an order contains a product ;

We should now be able to state the two following axioms :

(A1) $\forall x,y \in D, isProduct(x) \land isEmployee(y) \land EknowsP(y,x)$ 
$\to CraftableProduct(x)$
(A2) $\forall x,z \in D, CraftableProduct(x) \land isOrder(z) \land OcontainsP(z,x) \to AchievableOrder(z)$

From (A1) and (A2), we can derive the following theorem :

(T) $\forall x,y,z \in D, isProduct(x) \land isEmployee(y) \land isOrder(z) \land EknowsP(y,x) \land OcontainsP(z,x) \to AchievableOrder(z)$

Now, if I have three constants $e,p,o$ respectively in $E,P,O$ such that $isProduct(p)$, $isEmployee(e)$, $isOrder(o)$, $EknowsP(e,p)$ and $OcontainsP(o,p)$ are true and if I feed the inference engine with (A1), (A2), (T), it should derive that $AchievableOrder(o)$ is true according to the axiomatic theory composed of (A1), (A2) and (T).
This is the end of my proposed answer to the initial question. I have also three extra questions :

Do I really need predicates such as $isProduct(x)$ with $x \in D$ or could I choose to pick $x \in P$ and therefore assume that $isProduct(x)$ is true ?
Is this theory alright even if my axioms are completely non sense with another interpretation ? My guess on this is that it is fine to use such theory as long as it is consistent.
What should I modify in the above example if I would like to use some dynamic logic elements in the axioms ? As far as I understand things, I should extend the syntax with dynamic logic syntax, add dynamic logic axioms to the deductive system and extends the semantic with possible world models (even if I am not sure of how to do it...).

Thanks !

A:

You assumed first-order logic. But if you use also $\in$ you are extending your language to first-order set theory.
Is this necessary ? I think not. In your axiom 

(A1) : $\forall x,y \in D (isProduct(x)\land isEmployee(y) ...$

you are using $\in D$ only to restrict the "applicability" of your axioms to the domain $D$: this is already given by your semantical interpretation.
You said : "Deductive system : an Hilbert system without logical axiom & modus ponens rule of inference ..."; you need logical axioms. It does not make sense an "Hilbert system" without them.
About the "three constants $e,p,o$  respectively in $E,P,O$  such that $isProduct(p)$ , etc. are true and if ...", the semantical "conventions" force us to assume that the domain $D$ is not empty. For predicates, in order to add to the language (syntactical part) some constants, you must prove that there are objects in the domain that are their denotation; in principle, the predicate may have as counterpart in the interpretation the $\emptyset$ subset of the domain $D$. 
Having in the language a predicate $isProduct(p)$, does not assure you that exists in the domain at least an object that is a product. You have two choices: you must introduce axioms that give you by fiat the existence of those objects (like the axiom of set theory that introduce the empty set) and then you are allowed, by the rules of first-order logic, to add to your language the constants denoting them.
Otherwise, you introduce in the language constants for those objects (like $0$ in arithmetic) and the rule of standard semantics for first-order logic allows you to select "distinguished" objects in the domain that are the denotation of those constants in your interpretation.
Question 1) "Do I really need predicates such as $isProduct(x)$ with $x \in D$ or could I choose to pick $x \in P$ and therefore assume that $isProduct(x)$ is true ?"
As per comment about the domain $D$, you cannot mix the syntactical part (the language) with the semantical one (the interpretation of the language).
If you want to speak in the language of the objects $x$ of the domain $D$ such that they are "products" you must correctly introduce the predicate $isProduct(x)$ such that it holds of $x$ when $x$ is a product.
In the interpretation, the set $P$ will be exactly the interpretation of the predicate $isProduct(x)$, but $P$ will not be part of the language. So you need $isProduct(x)$.
Question 2) "Is this theory alright even if my axioms are completely non sense with another interpretation ? My guess on this is that it is fine to use such theory as long as it is consistent."
You are right. Formal arithmetic (that is first-order logic with Peano's axioms) is exactly f-o logic plus some non-logical axioms, like :

$\forall x (\lnot 0 = S(x))$.

In "your" theory, this axioms is not true; strictly speaking, it is nonsense, because in your language their are no the $0$ and $S(x)$ symbols.
In the same way, your predicate $isProduct(x)$ is not parte of the language of arithmetic.
So, the conclusion is that natural numbers will not be a viable domain for an interpretation of your theory.

