# Can semantic entailment be used in a formal proof?

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.

• @spaceisdarkgreen sorry that was a particularly bad typo. I have fixed it. – masiewpao Dec 4 '19 at 11:00

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$$.

• Thank you, this was exactly what I was looking for in the rule of inference! Can I ask whether it is ever valid to use a metalogic fact in a formal proof? Or would I need to 'convert' it into some rule of inference in sequent notation? (For e.g. in this case using disjunction elimination) – masiewpao Dec 4 '19 at 13:56
• my apologies I ended up editing my comment! I thought I had a slight follow up question, but I think your answer addresses it and now I see it. – masiewpao Dec 4 '19 at 14:03