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.

  • $\begingroup$ @spaceisdarkgreen sorry that was a particularly bad typo. I have fixed it. $\endgroup$ – 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$.

| cite | improve this answer | |
  • $\begingroup$ 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) $\endgroup$ – masiewpao Dec 4 '19 at 13:56
  • $\begingroup$ 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. $\endgroup$ – masiewpao Dec 4 '19 at 14:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.