I am reading "handbook of knowledge representation" and here the author mentioned two kinds of proofs for propositional logic: Meta-level and object-level proofs. It says:
When we want to establish that a formula $F$ is entailed by a knowledge base $ \Gamma$, the straightforward approach is to use the definition of entailment, that is, to reason about interpretations of the underlying signature. For instance, to check that the formulas $\lnot p$ and $q \rightarrow r$ entail $(p \lor q) \rightarrow r$ we can argue that no interpretation of the signature $\{p, q, r\}$ can satisfy both $\lnot p$ and $q \rightarrow r$ unless it satisfies $(p \lor q) \rightarrow r$ as well.
A sound deductive system provides an “object-level” alternative to this meta-level approach. Once we proved the sequent $\Gamma \implies F$ in the deductive system described above, we have established that Γ entails F.
I am quite confused. From "this meta-level approach", it can be inferred that the author means the way he mentioned of checking interpretations of $\{p,q,r\}$ is meta-level proof.
Then he goes:
For instance, the claim that the formulas $\lnot p$ and $q \rightarrow r$ entail $(p \lor q) \rightarrow r$ is justified by Fig. 1.2. Since the system is not only sound but also complete, the object-level approach to establishing entailment is, in principle, always applicable.
Fig.1.2 is a proof procedure of the entailment above:
Now I don't understand if Fig1.2 shown above is an object-level or a meta-level proof? And what is the essential difference between these two?
My understanding now is that object-level focus more on the specific atoms while meta-level focus more on $left \implies right$, which is more high-level. But I really don't understand the author here.
The proof shown in the linked Figure is a derivation in the propositional calculus.
It is said at "object level" because the propositional calculus is the "object" we are using to perform derivation (i.e. calculations with formulas and rules of inference).
At the "meta level", we are studying the mathematical properties of the mathematical object : propositional calculus, like e.g. consistency, soundness, completeness.
These properties are established trhough proofs that are "usual" pieces of mathematical reasoning regarding the calculus.
When we say e.g. that the propositional formula $p ∨ ¬p$ is a theorem of the calculus we can work two ways :
either (i) provide a derivation of it (i.e. $⊢ p ∨ ¬p$), from the axiom of the calculus, and this is an object-level proof,
or (ii) use semantics (truth table) to show that the formula is a tautology (i.e. $⊨ p ∨ ¬p$) and apply the Completeness theorem for the calculus, stating that every tautology is derivable in the calculus to conclude. In this case we are using a result (the completeness of the calculus) proved at the meta-level.
The distinction object-meta can be easily understood with the following example : a Chinese grammar written in English.
The Chinese Language is the object of study : the object-language, while the English Language is the language used to describe the first one : the meta-language.