How to show that something is not logically entailed?

Question

I was just thinking about entailment and would like to know if you can show that something is NOT entailed by the premises.

I know that to show $A, A → B \vdash B$, I could just provide a proof using, say, Fitch. So:

1. $A$

2. $A → B$

3. $B$ (modus ponens: 1,2)

My questions:

(1) Is there such thing as a negated turnstile? $\nvdash$ ? If so, are these taken to be two ways of saying the same thing? {premises} $\vdash \neg Q$ is the same thing as: {premises} $\nvdash Q$ ?

(2) How might one show that $A, A → B \nvdash C$ ? (That C is not a syntactic consequence of A, A → B?)

(3) If something is entailed by the premises, is it called a "theorem"? So, in my above example, is "B" a theorem?

My guesses so far:

My guess is that if what I said in (1) is right, then I would have to show that my premises entailed $\neg C$, in order to get that it $A, A → B \nvdash C$.

But even if that is the case, I don't know how to go about showing that ~C. Indeed, I don't even see the letter C anywhere to begin working with!

Answer 1

As you said you can show that $P \vdash \lnot C$ and assuming that your deductive system is not contradictory then $C$ man not hold. You can also prove using meta-theory that proof of $C$ from $P$ (ie $P \vdash C$) can not exist. As far as I remember Dirk van Dalen in his Logic and Structure uses |-\- symbol in the later sense.

Answer 2

In this answer $A,B,C,P$ and $Q$ are all taken as pairwise distinct propositional atoms, because otherwise the question asserts some irreparable falsehoods.

(2) How might one show that $\{A, A \to B\} \not \vdash C$ ? (That $C$ is not a syntactic consequence of $\{A, A \to B\}$?)

The completeness theorem tells you that you can equate provability and truth (or syntactic truth and semantic truth, if you prefer), that is, given a set of formulas $\Sigma$ and a formula $\varphi$, one has $\Sigma \models \varphi$ if, and only if, $\Sigma \vdash \varphi$. Thus, to prove that something is not a syntactic consequence of a set of premises, it suffices to prove that it is not a semantic consequence of those premises, that is, it suffices to check that there are lines on the truth table that make all the premises $\Sigma$ true and $\varphi$ false.

If you don't have the completeness theorem yet, then you need to prove it by definition of proof, but the completeness theorem (well, half of it), exists exactly so we don't have to do that.

You probably know how to use this information to prove that $C$ is not a syntactic consequence of $\{A, A\to B\}$.

(1) Is there such thing as a negated turnstile, $\not\vdash$ ? If so, are these taken to be two ways of saying the same thing? $\{\text{premises}\} \vdash \neg Q$ is the same thing as: $\{\text{premises}\} \not \vdash Q$?

Yes, there is such a thing as $\not \vdash$ (non-entailment) and it can be used when whatever is on the right of $\vdash$ is not provable from what's on the left.

No, $\{\text{premises}\} \vdash \neg Q$ and $\{\text{premises}\} \not \vdash Q$ do not assert the same thing. The first one tells you that $\neg Q$ is a syntactic consequence of the set of premises, the second one tells you that $Q$ is not a syntactic consequence of the premisses. Certainly $\{\text{premises}\} \not \vdash Q$ is a logical consequence of $\{\text{premises}\} \vdash \neg Q$, but not the other way around, hence they mean different things.

Let me try to clarify with an example. Consider $\{P\}$ as the LHS , then clearly it doesn't hold that $\{P\}\vdash Q$, that is, it holds that $\{P\}\not \vdash Q$ (your question (2) asks how does one prove non-entailment, read my answer to it first to know why it is so clear), but $\{P\}\vdash \neg Q$ doesn't necessarily hold, so $\{P\}\vdash \neg Q$ is not a logical consequence of $\{P\}\not \vdash Q$, even though $\{P\}\vdash \neg Q$ implies $\{P\}\not \vdash Q$.

I'm using the term 'logical consequence' as meta-term, it's not related to logical consequence within the system.

(3) If something is entailed by the premises, is it called a "theorem"? So, in my above example, is "$B$" a theorem?

A theorem is, by definition, a statement provable from the empty set of premises. In your example above $B$ is not a theorem because one doesn't have $\varnothing \vdash B$. However, there's a natural way to extract a theorem from the proof you've provided, given by the deduction theorem. What is indeed a theorem is $A\to ((A\to B)\to B)$.

Given this definition of theorem, the completeness theorem asserts that a formula is a theorem if, and only if, it is a tautology.

Answer 3

A usual method, as Git Gud hints at, lies in constructing a model where the formulas on the left side of the $\vdash$ hold, but those on the right do not. Tools like Mace4 can help you to find such models.

Also, in axiomatic systems with modus ponens and substitution as rules of inference it sometimes comes as possible to show that only certain formulas or certain substitution instances of formulas can get proved. For example, suppose our only axiom is

C Np Cpq.

We can't prove C p Cqp. Why? Well, in order to prove something with C Np Cpq as our axiom, we need to find some substitution instance of C Np Cpq which would come as possible to end up as the left side of C Np Cpq. But, then it would have to start with an "N", and no substitution instance of C Np Cpq does this. Using J. A. Kalman's terminology (and maybe others terminology also), we would have a "symbol clash". So, nothing can get derived from C Np Cpq. Therefore, C p Cqp can't get proved either.

As another example, suppose our only axiom is 1-C CCpqp p. Now, let's suppose that a theorem which is not a substitution instance of C CCpqp p exists in this system. We'll try to find the most general theorem derivable D1.1

C C C a   b a a
  | | |   | |
  | | --- | |
  C C Cpq p p

So, if we have such a theorem, this diagram suggests that we have a/Cpq, b/p, and p/a. Fixing those false substitutions we have a/Caq, b/a, and p/a. But, we can't substitute "a" with "Caq", since "a" occurs in the formula that is to get substituted for "a". Using J. A. Kalman's terminology, we have an "occurs check" here. And thus, ApNp, for example, is not derivable from CCCpqpp.

For some further references on this topic one might see Jan Lukasiewicz's paper The Equivalential Calculus or J. A. Kalman's book on OTTER on p. 224-226, or contact John Halleck.

Answer 4

You asked 3 questions. Question 1:

Is there such thing as a negated turnstile? ⊬ ? If so, are these taken to be two ways of saying the same thing? {premises} ⊢¬Q is the same thing as: {premises} ⊬Q ?

Some people use the negated turnstile. The two things you list in the question are not the same thing. (As others have said.) But let me give an example (if that helps).

Consider the (degenerate, rather useless) system made up of Uniform substitution, and the single axiom p→p. (This system has no use I'm aware of other than as a bad example.)
Clearly any substitution instance of this preserves the property that the antecedent and consequent [The left and right side] are identical. No statement with a top level negation can be formed at all, so it can never the case that {premises} ⊢¬Q. But, if we use p→q for Q, Q is not provable. (since the two sides are not identical). So it IS the case that {premises}⊬Q holds.

This is, by the way, the previous example is an example of a syntactic disproof. (Answering question 2 also.) There are a number of ways syntactic disproofs are done. Most operate by showing that all theorems in a system have some property. (The axioms have it, the rules preserve it). If an alleged theorem does not have that property, it is therefore not a theorem. [An example of this is that the logic "BCI" has the "2-property", the side effect of this is that if an alleged theorem has an odd number of some variable, you know it is not actually a theorem. Other logics have other properties that can be used.] [A google search of "BCI logic 2-property" will get you some discussion of BCI having the 2-property.]

Question 3 has already been answered quite clearly above by others.