Prove that if $Σ$ is consistent and $Σ \vdash A$ , then $Σ ∪ \{A\}$ is consistent.

Question

Maybe I am wrong, but isn't $Σ$ being consistent equivalent or very similar to $Σ$ being satisfiable?

Since $Σ$ is consistent it is not a contradiction. Since $Σ \vdash A$, we know that $Σ$ is tautologically equivalent to $A$. Therefore $Σ ∩ \{A\}$ is consistent because it is satisfiable and not a contradiction.

Is this the right line of thinking here?

How would one go about answering this question properly?

Answer 1

For a logic that is (sound and) complete, a theory is indeed consistent if and only if it is satisfiable.

This is the case for standard first-order logic.

On the other hand, second or higher-order logic do not have complete proof systems according to the standard semantics. In those logics it is possible for a theory to be consistent (that is: the theory cannot prove a contradiction) and at the same time not being satisfiable (that is: it has no model).

You're explaining your proof idea a bit off. Just because $\Sigma\vdash A$ does not make $\Sigma$ and $A$ equivalent. For example, consider a language with three constant symbols $a,b,c$, and let $\Sigma$ be $\{a=b, b=c\}$ and $A$ be $a=c$. Then $\Sigma\vdash A$, but $A$ is true in more structures than $\Sigma$ is, so they are not equivalent.

Instead, what you'll probably want to do is describe how if $\Sigma\vdash A$ and $\Sigma,A\vdash\bot$, then you can construct a proof of $\Sigma\vdash\bot$ -- as a matter of syntactic manipulation of proofs.

Answer 2

It is true that consistency and satisfiability coincide for first-order logic, but that is a non-trivial theorem: the Gödel completeness theorem. Consistency is a syntactic notion: it is about what one can prove. Satisfiability is a semantic notion: it is about what models exist. You don't need to appeal to semantic notions to prove the purely syntactic claim you are trying to prove.

The definition of consistency says that $\Sigma$ is consistent if there is a formula $B$, such that $\Sigma \not\vdash B$, meaning that $B$ cannot be proved in first-order logic taking $\Sigma$ as a set of axioms. But then if $\Sigma$ is consistent, so also is $\Sigma \cup \{A\}$ for any $A$ such that $\Sigma \vdash A$, because if $\Sigma \not\vdash B$, then also $\Sigma \cup \{A\} \not\vdash B$ (because given a proof of $B$ taking $\Sigma$ and $A$ as axioms, you could get a proof of $B$ from $\Sigma$ alone, by replacing each use of the axiom $A$ by proof of $A$ from $\Sigma$).

Answer 3

How about this as an answer:

Σ |- A

We are given that Σ is consistent, using a proof by contradiction, let's assume that Σ∪{A} is inconsistent.

Then we have:

Σ∪{A} |- B

Σ∪{A} |- ¬B

By deduction theorem:

Σ |- A → B

Σ |- A → ¬B

Using what we just found above, and the fact that Σ |- A, by modus ponens we must have:

Σ |- B

Σ |- ¬B

Therefore Σ is inconsistent. This contradicts our initial assumptions of Σ being consistent.

Therefore Σ∪{A} is consistent.

Answer 4

Prove that $$ \frac{\Gamma \vdash A ~~~~~~ \Gamma\nvdash \bot}{A, \Gamma \nvdash \bot} $$ Proof.

Let us assume the same premises, but with the opposite conclusion i.e. $$A, \Gamma \vdash \bot\tag{1}$$ instead of $$A, \Gamma \nvdash \bot \tag{2}$$ Then (1) being provably equivalent to $$\Gamma \to A, \Gamma \vdash \bot \tag{3}$$ because $$\Gamma \nvdash \bot\tag{4}$$ is assumed, (3) would be valid only if $$A = \bot \tag{5}$$ would be true, to get from (3), via rule $\to E$ on the left, the valid sequent $$\bot, \Gamma \vdash \bot \tag{6}$$ But (5) would be in contradiction with the premises: $\Gamma \vdash A$ and $\Gamma \nvdash \bot$. Therefore

$$ \frac{\Gamma \vdash A ~~~~~~ \Gamma\nvdash \bot}{A, \Gamma \nvdash \bot} $$ Q.E.D

Answer 5

These two inference rules are logically equivalent in a classical meta-level with (D |/- B) = ~(D |- B). They are just contraposition of each other:

   G |- A     G, A |- C
----------------------- (Cut)
         G |- C

   G |- A     G |/- C
----------------------- (Contra-Cut)
       G, A |/- C

So the OPs theorem emerges for C = f and when the system has (Cut). Would work for incomplete calculus as well, since OP asked for consistency and not satisfiability.