Differences

This shows you the differences between two versions of the page.

--- sav08:quantifier_elimination_definition [2009/04/21 23:42]
vkuncak
+++ sav08:quantifier_elimination_definition [2011/04/05 16:02]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Definition of Quantifier Elimination ======
-In this section, we will consider some language ${\cal L}$ and some set $T$ of formulas such that $Conseq(T)=T$ (see [[sav08:First-Order Logic Semantics]]).  We will write $\models F$ to denote $T \models F$ (which is equivalent to $F \in T$).
+In this section, we will consider some language ${\cal L}$ and some set $T$ of formulas such that $Conseq(T)=T$ (see [[sav08:First-Order Logic Semantics]]).
+//Informal summary: the meaning of relations and functions such as <,+, can be defined by starting from first-order logic, and then introducing a set of axioms in first-order logic that they satisfy, and taking also their consequences. The set of axioms and consequences that define the operations and relations of interest is the theory. Formally, the theory is simply any set of fully quantified formulas (often the theory is understood to also include all of its consequences).//
 As a special case, we can have
@@ Line 10: / Line 12: @@
 Then $\models F$ reduces to $\forall I \in {\cal I}. e_F(F)(I)$.
 If we look at one interpretation, then ${\cal I}$ contains only that interpretation and the condition $\models F$ means $e_F(F)(I)$.
+**Shorthand:** We will generally fix $T$ and write $\models F$ as a shorthand for $T \models F$.
 **Example:** Let $M = ({\cal Z},+)$ be the structure of integers with addition. If we let ${\cal I} = \{ M \}$ then $T$ in the definition above is the set of all formulas involving only $+$ that are true about integers. In this example,