502 – Completeness

September 25, 2009

1. Preliminaries

Just as with propositional logic, one can define a proof system for first order logic. We first need two definitions.

Definition 1 If {\phi} is a formula, a generalization of {\phi} is any formula of the form

\displaystyle \forall x_1\forall x_2\dots\forall x_n\,\phi.

(We are not requiring in the definition above that the {x_i} are different or that they are present in {\phi.})

Definition 2 Let {t} be a term, let {x} be a variable, and let {\phi} be a formula. We say that {t} is substitutable for {x} in {\phi} iff no free occurrence of {x} in {\phi} is within the scope of a quantifier {\exists z} or {\forall z} with {z} a variable occurring in {t.}

Read the rest of this entry »

2 Comments | 502: Logic and set theory | Tagged: | Permalink
Posted by andrescaicedo

502 – Propositional logic (4)

September 14, 2009

11. Completeness

We now want to show that whenever {S\models A,} then also {S\vdash A.} Combined with the soundness Theorem 22, this shows that the notions of provable and true coincide for propositional logic, just as they did for the tree system. The examples above should hint at how flexible and useful this result actually is. This will be even more evident for first order (predicate) logic.

Theorem 26 (Completeness) For any theory {S} and any formula {A,} if {S\models A,} then {S\vdash A.}

Read the rest of this entry »

Leave a Comment » | 502: Logic and set theory | Tagged: , | Permalink
Posted by andrescaicedo

502 – Formal systems (3)

September 4, 2009

Theorem 2 (Completeness) Whenever {\Sigma\models\tau,} then also {\Sigma\vdash\tau.}

Read the rest of this entry »

Leave a Comment » | 502: Logic and set theory | Tagged: | Permalink
Posted by andrescaicedo