Can semantic entailment be used in a formal proof?

Question

I am wondering about whether it is possible/makes sense that you could use the fact of semantic entailment (or logical consequence) in a formal proof?

Consider the example: Suppose $A \cap C \subset B$ and $a \in C$. Then $a \notin A\backslash B$. It is straightforward to prove by turning the negation into an implication and just directly proving it. In this example, I can imagine how these steps, starting from the premises, could be written out formally starting with the premises and using rules of inference to arrive at the next sentence, step-by-step until I arrive at the final sentence.

However I was wondering about what happens if instead you follow this sequence of logical inference until you arrived at the following (very contrived) sentence: $$\forall x [x \in A \land x \in C \implies x \in B] \land a \in C$$

Up until this sentence it seems to me that there would be a way of using logical inferences to get here from the premises. Here is where my question came from: It seems to me that by assuming cases for $a \in A$ and it's negation, we can show the conclusion. I.e.

If we assume $a \in A$ then we have $a\in A \land a \in C \rightarrow a \in B$, and

if we assume $a \notin A$ then we have $a \notin A$

To finally arrive at $a\notin A \lor a \in B$, which is exactly the conclusion.

However I don't know if this reasoning works in a logical proof. The cases I considered have the form $A$ and $\neg A$.So consider the truth table for $A \lor \neg A$, $P$, $Q$, and $P \lor Q$, and where we know that $A \vdash P $ and $\neg A \vdash Q$, where here $P$ and $Q$ could represent the statements $a \notin A$ and $a \in B$ respectively.

From the truth table (or quite obviously anyway), I can see that $P \lor Q$ is a logical consequence of $A \lor \neg A$. In other words, $(A \lor \neg A) \vDash (P \lor Q)$.

My understanding is that a formal proof is a sequence of sentences, which are derived from the rules of inference of our formal system. I have recently learnt the distinction about the difference between metalanguage and language of the formal system, and the semantic entailment does not seem to be a logical inference rule (at least of propositional calculus).

So ultimately my question is whether I can use the fact that $(A \lor \neg A) \vDash (P \lor Q)$ in a formal proof? For example, could I in the proof assume $A \lor \neg A$ (which I assume is valid since it is a tautology), and then state "since $(A \lor \neg A) \vDash (P \lor Q)$ , $P \lor Q$"

My apologies if I am misunderstanding the notions here, I only have a shallow understanding of logic so I am not sure if this answer is obvious either way.

Answer 1

The two premises of the argument are : $A \cap C \subset B$ and $a \in C$.

Then we have two cases :

(i) $a \in A$. Then $a \in A \cap C \subset B$, and thus $a \in B$. By $\lor$-intro : $a \notin A \lor a \in B$.

(ii) $a \notin A$. Thus by $\lor$-intro again : $a \notin A \lor a \in B$.

In conclusion, due to the fact that the two cases are exhaustive, we can conclude that under assumptions above : $a \notin A \lor a \in B$.

The logical rule of inference to be used is Disjunction Elimination (aka : Proof by cases) :

$\alpha \to \varphi, \lnot \alpha \to \varphi \vDash \varphi$,

using the tautology : $\alpha \lor \lnot \alpha$.

Here $\alpha$ is $a \in A$ and $\varphi$ is $a \notin A \lor a \in B$ and the argument has shown that :

$a \in C, A \cap C \subset B \vDash a \notin A \lor a \in B$.