4
$\begingroup$

During one of the lectures in logic, My prof proved completeness and soundness of Hilbert system of axioms or simple axiom system as in http://en.wikipedia.org/wiki/Propositional_calculus#Soundness_and_completeness_of_the_rules

But looks like neither my prof's proof nor the proof in wikipedia has any references to the axioms on which completeness is proved. I am really confused, Completeness supposed to mean any tautology can be proved just through that axiom schema and modes ponens right? Or am i missing something?

Entire proof seems to make valid statements but i dont see any connection to what it proves and how it uses of any of the assumptions.

$\endgroup$
  • $\begingroup$ "Completeness supposed to mean any tautology can be proved just through that axiom schema and modes ponens right? " No, completeness means that any tautology can get proved just through the formal axiom schema (or formal axioms) and the rules of inference of the system. If you have no formal axioms or formal axiom schema, then completeness can get proved just through the rules of inference of the system. $\endgroup$ – Doug Spoonwood Sep 17 '14 at 4:47
  • $\begingroup$ But if u look at the completeness proof in that article. I doesn't take the inference rules or axioms into account. It just considers the semantics of the tautology or i am missing to see the reference $\endgroup$ – vinothkr Sep 17 '14 at 6:11
  • 1
    $\begingroup$ @vinothkr - The "sketch of proof" of Wiki's article shows us a "method" that we have to apply to e.g. the two proof system previously defined in the article : the three axioms + modus ponens and Natural Deduction. For soundness, the method is general and works by induction : (i) prove that the axioms (if any) are tautologies; (ii) prove that the rules preserve "tautologuesness". For completeness we have two possible approaches... $\endgroup$ – Mauro ALLEGRANZA Sep 17 '14 at 6:26
  • 2
    $\begingroup$ The approach sketched in Wiki (but you need a full exposition of it : see some textbook) needs some preliminary Lemmas like : $\varphi$ is unprovable from a set of formulae $\Gamma$ iff there is a valuation which satisfy all formulae in $\Gamma$ and falsify $\varphi$. From this follows, with the emptyset as $\Gamma$, that if $\nvdash \varphi$, then $\nvDash \varphi$. This, by contraposition, is the Completeness Theorem. 2/2 $\endgroup$ – Mauro ALLEGRANZA Sep 17 '14 at 6:46
  • $\begingroup$ The part of the lemma you talk about is the finite satisfiability right? But my question is how is this connection between semantic validity (there is a valuation which satisfy all formulae in Γ and falsify φ) and the syntactic provability (φ is unprovable from a set of formulae Γ) is made. $\endgroup$ – vinothkr Sep 17 '14 at 6:52
5
$\begingroup$

You can see a full exposition of the Completeness Theorem for propositional logic in every good math log textbook, like :

The proof system used is Natural Deduction; here is a sketch of the proof.

Lemma 2.5.1 (Soundness) If $Γ \vdash \varphi$, then $Γ \vDash \varphi$.

The proof of it needs the rules of the proof system.

Definition 2.5.2 A set $\Gamma$ of propositions is consistent if $\Gamma \nvdash \bot$ [$\bot$ is the logical constant for "the falsum, used in ND].

Let us call $Γ$ inconsistent if $Γ \vdash \bot$.

Lemma 2.5.4 If there is a valuation $v$ such that $v(\psi) = 1$ for all $\psi \in \Gamma$, then $\Gamma$ is consistent.

Lemma 2.5.5

(a) $Γ \cup \{ ¬\varphi \}$ is inconsistent iff $Γ \vdash \varphi$,

(b) $Γ \cup \{ \varphi \}$ is inconsistent iff $Γ \vdash ¬\varphi$.

For (a) : by assumption we have (see def of consistency) $\Gamma, \lnot \varphi \vdash \bot$. Now apply the (RAA) rule [i.e. if we have a derivation of $\bot$ from $\lnot \varphi$, we can infer $\varphi$, "discharging" the assumption $\lnot \varphi$] to conclude with : $\Gamma \vdash \varphi$.

Lemma 2.5.7 Each consistent set $Γ$ is contained in a maximally consistent set $Γ^*$.

Lemma 2.5.8 If $Γ$ is maximally consistent, then $Γ$ is closed under derivability (i.e. if $Γ \vdash \varphi$, then $\varphi \in Γ$).

[...]

Lemma 2.5.11 If $Γ$ is consistent, then there exists a valuation $v$ such that $v(\psi) = 1$, for all $\psi \in Γ$.

Corollary 2.5.12 $Γ \nvdash \varphi$ iff there is a valuation $v$ such that $v(\psi) = 1$ for all $\psi \in Γ$ and $v(\varphi) = 0$.

Proof $Γ \nvdash \varphi$ iff $Γ \cup \{ ¬ \varphi \}$ is consistent iff there is a valuation $v$ such that $v(\psi) = 1$ for all $\psi \in Γ \cup \{ ¬ \varphi \}$, or $v(\psi) = 1$ for all $\psi \in Γ$ and $v(\varphi) = 0$.

Theorem 2.5.13 (Completeness Theorem) $Γ \nvdash \varphi$ iff $Γ \nvDash \varphi$.

Proof if $Γ \nvdash \varphi$, then $Γ \nvDash \varphi$ by Corollary 2.5.12. The converse holds by Lemma 2.5.1.

$\endgroup$
  • 1
    $\begingroup$ Now i get it. The axiom system has to prove given a maximal set Let X be a maximal consistent set. en: (i) For all formulas α, α ∈ X iff ¬α /∈ X . (ii) For all formulas α,β, α ∨ β ∈ X iff α ∈ X or β ∈ X . $\endgroup$ – vinothkr Sep 17 '14 at 14:01
  • $\begingroup$ @Mauro ALLEGRANZA, do you happen to know any free books or notes where all those lemmas are proved? I could really use a reference (I studied all of them in a short course I took some time, and I'd like to review the proofs, but I can't find free online sources). $\endgroup$ – YoTengoUnLCD Jan 3 '16 at 20:44
  • $\begingroup$ @YoTengoUnLCD - you can see : Stephen Simpson, Mathematical Logic (2013), Stephen Simpson, Model Theory (1998) and Stephen Simpson, Foundations of Mathematics (2009). $\endgroup$ – Mauro ALLEGRANZA Jan 5 '16 at 12:58
  • $\begingroup$ I don't understand the proof of corollary 2.5.12. Why $\Gamma\nvdash \varphi\implies \Gamma\cup\{\neg\varphi\}$ is consistent? $\endgroup$ – user 170039 Dec 17 '16 at 6:30
  • $\begingroup$ @user170039 - Lemma 2.5.5(a) : $Γ ∪ \{ ¬φ \}$ is not-consistent iff $Γ⊢φ$. Thus, it is enough the negate both sides to get : $Γ ∪ \{ ¬φ \}$ is consistent iff not $Γ⊢φ$. $\endgroup$ – Mauro ALLEGRANZA Dec 17 '16 at 13:49
0
$\begingroup$

I'm not sure I follow what you're asking, but the confusing may be in the fact that the propositional calculus is sound and complete with respect to any truth assignment. You could think of a truth assignment $A$ as a list of axioms: some number of statements which are claimed to be true (or false.) Then we can semantically deduce an infinite set of truths $A_e$, using the rules like "$\phi \wedge \psi$ is true if and only if $\phi$ is true and $\psi$ is true." And we can syntactically deduce an infinite set of truths $A_y$ using the proof rules, e.g. "$\phi,\psi\vdash \phi \wedge \psi$".

The point of the soundness and completeness theorems is exactly that $A_e=A_y$-completely regardless of the initial choice of axioms $A$! So these are theorems about a method of deduction, rather than about any particular axiom system.

Another possible point of confusion about these theorems is that it seems like we give the exact same set of semantic rules as syntactic rules, so that it seems almost obvious that deductions via the two sets of rules can only lead the same place. The point is that deductions via the semantic rules need not proceed via finitely many sequential applications of the rules, so the main content of the completeness theorem is that one doesn't need any infinite proofs to get all the consequences of $A$. This is no longer necessarily the case in other logical systems! So the existence of these theorems enshrines propositional logic as a beautiful elementary case in which everything works out as well as one could possibly hope.

$\endgroup$
  • $\begingroup$ "The point of the soundness and completeness theorems is exactly that Ae=Ay-completely regardless of the initial choice of axioms A!" No. You can consider systems with any set of well-formed formulas as axioms under some set of rules and see what follows. For instance, you can consider the system with just the axiom (p$\rightarrow$(q$\rightarrow$p)) under detachment and uniform substitution. You can't prove all tautologies of 2-valued logic in that system. You could also consider the system ((p$\rightarrow$q)$\rightarrow$(q$\rightarrow$p)) with the above rules. You won't deduce a variable. $\endgroup$ – Doug Spoonwood Sep 17 '14 at 4:42

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.