0
$\begingroup$

I came across the following in a textbook:

enter image description here enter image description here

$\mathcal{L}$ is a language. $\alpha \in \mathcal{L}$ is a formula. $\alpha \frac{c}{x}$ means: replace every instance of $c$ in $\alpha$ by $x$.

I am not sure I understand the sketch of this proof. Part of the issue I am finding, as I go through logic texts, is that the notation isn't the most illuminating.

Thus, I am wondering, may I have a sketch of proofs that show that boolean algebra is complete, using as much English as possible? (A sketch of a proof is something that is not a proof, but merely outlines how one would start the proof, or what strategy one would employ.)

$\endgroup$
  • 1
    $\begingroup$ It seems to be about predicate logic. The sentence 'Boolean algebra is complete' adds a little confusion.. $\endgroup$ – Berci May 4 at 7:49
  • $\begingroup$ The notation isn't going to go away or reduce as you proceed, so avoiding it doesn't seem like a good strategy. Also, with a few minor exceptions, most of the "notation" is just the things themselves. Formulas like $\neg\alpha$ are pieces of syntax, just symbols, they don't have meaning. $\equiv$ is a relation between formulas, so it's saying something that could arguably be written out in English, but I doubt that would be too helpful (except by making it more clear that it doesn't mean equality and that it's acting on these formulas). At any rate, there appears to be a typo in (1). $\endgroup$ – Derek Elkins May 4 at 7:54
  • $\begingroup$ $\alpha\frac{x}{c}$ means "replace every instance of $x$ in $\alpha$ by $c$", not the other way round. $\endgroup$ – lemontree May 4 at 10:47
  • 1
    $\begingroup$ @user89 I'm afraid the notation could hardly be made any easier, and the terminology used is just the standard terminology of FOL. Abstract concepts and involved proofs requie a minimum of notation and terminology; that's not a fault of the textbook, that's just how math works. $\endgroup$ – lemontree May 4 at 19:57
  • 1
    $\begingroup$ @user89 While this is not my favorite notation by any means, it's not too dissimilar to many other popular notations. Either way, learning to deal with potentially bad and certainly a variety of notations is also something you'll need to learn. Yes, it is annoying that there is a variety of notations, but given how bad old notations used to be, I'm glad people didn't feel too tied to them. $\endgroup$ – Derek Elkins May 5 at 0:43
2
$\begingroup$

In order to prove completeness of a calculus, we need to show that any consistent theory $T$ has a model, that is, we need to find an $\mathcal{L}$ structure $\mathfrak{A}$ such that $\mathfrak{A} \vDash T$. This is achieved by constructing so-called Henkin theories. It is possible to show that any complete Henkin theory has a model. So the goal is to "henkinize" a given theory, i.e. extending the theory $T$ to a Henkin theory $T_H$, which is then extended to a complete Henkin theory in a next step.

The first step towards the construction of such a Henkin theory is what is done here: Your textbook snippet defines the "Henkin formulas" which will be added to the theory $T$ to arrive at a Henkin theory $T_H$.

In a Henkin theory $T_H$, any existential statement $\exists x \alpha \in \mathcal{L}$ (note: any existential statement of the language $\mathcal{L}$, not just those in $T_H$!) is "witnessed" by an individual constant $c$. This means that if we claim that $\alpha$ is true for some $x$, then we need to be able to provide a concrete term $t$ that provides evidence for this claim, hence the name "witness". For example, in the language of Peano arithmetic with a symbol for $>$, if we claim that $\exists x(x > 0)$, then we want to find a concrete instance of $x$ that satisfies this property (in this acse, this could be $s(0)$). This concrete instance is denoted by an individual constant $c$. (We later need to extend the alphabet of our language to include all of these witnesses $c$; this will result in the Henkin language $\mathcal{L}_H$, in which the Henkin theory $T_H$ of a theory $T$ can be axiomatized.)
In our example, $\alpha = x > 0$ (note that $\alpha$ contains a free variable $x$), and $\alpha\frac{c}{x}$ just means that $x$ is substituted by $c$, so here $\alpha\frac{c}{x} = c > 0$.
Note that this is an implicative statement, so the individual denoted by $c$ does not necessarily need to have the property $\alpha$: We only have $T_H \vDash \alpha\frac{c}{x}$ in case $T_H \vDash \exists x \alpha$.

So in a Henkin theory $T_H$, we want that the formula $\exists x \alpha \to \alpha\frac{c}{x}$ is $\in T_H$ for any $\alpha$. To define this "Henkin formula" for any $\alpha$, we can introduce the notation $\alpha^x$, and write it as

$$(1') \quad \alpha^x := \exists x \alpha \to \alpha\frac{c}{x}$$

Now suppose that a formula has the form of a negated statement, for example $\alpha' := \neg \alpha = \neg (x > 0)$. Then the Henkin formula becomes

$$(2) \quad (\neg \alpha)^x = \exists x \neg \alpha \to \neg \alpha \frac{c}{x}$$

This means that under the assumption $\exists \neg \alpha$, there is a witness $c$ that provides evidence for $\neg \alpha$, and therefore a counterexample to the validity of $\alpha$.

This is precisely what your textbook snippet says. It is easy to see that this is equivalent to the negation of (1):

$(\neg \alpha)^x\\ \equiv \exists x \neg \alpha \to \neg \alpha \frac{c}{x}\\ \equiv \neg(\exists x \neg \alpha \land \neg \neg \alpha \frac{c}{x})\\ \equiv \neg(\neg \forall x \alpha \land \neg \neg \alpha \frac{c}{x})\\ \equiv \neg(\neg \forall x \alpha \land \alpha \frac{c}{x})\\ \equiv \neg(\alpha^x)$

So we can deduce the unintuitive formula (1) by starting with the more intuitive implicative formulation (1') and inserting a negative formula $\neg \alpha$ as in (2).

However, for positive formulas $\alpha$, (1) = $\alpha^x$ is not equivalent to the implicational formulation (1') of the Henkin formula:

We have

$$(1) = \neg \forall x \alpha \land \alpha \frac{c}{x} \vDash \exists x \alpha \to \alpha \frac{c}{x} = (1')$$

(since $\neg \forall x \alpha \land \alpha \frac{c}{x} \vDash \alpha \frac{c}{x} \vDash \exists x \alpha \to \alpha \frac{c}{x}$)

but $$(1') = \exists x \alpha \to \alpha \frac{c}{x} \not \vDash \neg \forall x \alpha \land \alpha \frac{c}{x} = (1)$$

(since if $\mathfrak{A}, v \not \vDash \exists x \alpha$ and $\mathfrak{A}, v \not \vDash \alpha \frac{c}{x}$, then $\mathfrak{A}, v \not \vDash \exists x \alpha \to \alpha \frac{c}{x}$ but $\mathfrak{A}, v \not \vDash \neg \forall x \alpha \land \alpha \frac{c}{x}$).

So (1) $\vDash$ (1') but (1') $\not \vDash$ (1), hence (1) is a stronger statement than (1'): All situations (here: combinations of structures $\mathfrak{A}$ and assignments $v$) where (1) is true are also situations where (1') is true, but not the other way round, so there are fewer cases where (1) holds than where (1') holds, i.o.w. fewer structures which will manage to satisfy (1) than (1'), so (1) manages to exclude more possibilities (if you imagine a structure as a "possibility of what the universe could look like", you managed to exclude more such possibilities), hence it is a stronger, more informative claim than the more intuitive (and I think more common) Henkin formula (1').

Your textbook will show how the construction of a Henkin theory - and its extension to a complete Henkin theory for which we can prove the existence of models - will work for this more unintuitive, stronger formulation of Henkin formulas, but the idea is the same: For any existential statement, we want to have a witness in the form of an individual constant denoting a concrete object that provides evidence for this existential claim, and likewise, in the case of an existential negated statement, we want a witness that proves the invalidity of the unnegated statement. This is exactly what is done here.

$\endgroup$
  • $\begingroup$ Thank you for this answer. However, can I ask some fairly "stupid" questions, and ask you to update your answer with their answers? (I'll also be very happy to give a large bounty.) $\endgroup$ – user89 May 4 at 19:01
  • $\begingroup$ 1) A model is simply a choice of instantiation for each free variable in each formula. Yes? If so, can you replace the word model with something more appropriate? $\endgroup$ – user89 May 4 at 19:02
  • $\begingroup$ 2) What does $\mathfrak{A} \vDash T$? Let $\alpha$ be a formula, then $\vDash \alpha$ means that every choice of instantiation for all the free variables in $\alpha$ causes $\alpha$ to be evaluated to $\top$. Is this correct? In this context, what does $\mathfrak{A} \vDash T$ mean? That every formula in $T$, when instantiated with constants in $...$ evaluates to $\top$? What should fill $...$? $\endgroup$ – user89 May 4 at 19:04
  • $\begingroup$ 3) Can we avoid the use of honorifics in this answer? For instance, instead of saying "Henkin theory", can we say "$...$ theory", where $...$ is something descriptive? $\endgroup$ – user89 May 4 at 19:06
  • $\begingroup$ 4) What does "positive formula" mean? Does if $\alpha$ is positive, does it mean that $\alpha = \top$? $\endgroup$ – user89 May 4 at 19:12

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.