Monday, 19 September 2011

Book draft: Formal Languages in Logic

(Apologies for shameless self-promotion!)

In several of my posts, I mentioned the book on formal languages that I've been working on for the last few years. I now have a draft of the book ready for (moderate!) public consumption, which is now available here. The two final chapters are still missing, but the draft is already something of a coherent whole, or so I hope.

Many people have kindly expressed their interest in checking out the material, hence my decision to make it available online at this point, despite the fact that it is still a somewhat rough draft (references are still a mess). Needless to say, comments are always welcome :)

10 comments:

  1. Hi Catarina, thanks for uploading the draft (thanks for emailing a copy of one of the chapters too a few days ago).

    On the containment point again,
    "As observed by van Benthem, “mathematicians want results about ‘arithmetic’, not about the first-order Peano system for arithmetic”; in other words, they want results about the target phenomenon, the ‘real thing’, not about the formalism used to
    describe it." (p. 86)

    Sounds exactly right - but what *is* the phenomenon, the 'real thing'? If, with my physics knowledge, I model a ball rolling down an inclined surface or plane, I know what the model is and what the phenomenon is.

    But, in the case that interests you, what is the phenomenon?

    "And yet, logicians working with formal systems are first and foremost proving theorems about the formalism, which say something about the target phenomenon only insofar as the fitting between formalism and phenomenon is good enough."

    This is expressed using the notion of truth, surely?
    For example, let $\phi$ be the formula $\forall x(S(x) \neq \underline{0})$ of the interpreted language $\mathbf{L}_A = (\mathcal{L}_A, \mathbb{N})$ of arithmetic. The definition of truth for $\mathbf{L}_A$ gives, e.g.:

    $\phi$ is true in $\mathbf{L}_A$ iff 0 is not the successor of any natural number.

    Surely this is how we obtain results about the completeness or soundness properties of, e.g., $I \Sigma_1$?

    Jeff

    ReplyDelete
  2. Hi Jeff,

    I'll discuss the matter of the elusive 'target phenomena' in more detail in chapter 7. In the case of mathematics, I'd say that the target phenomenon of, for example, PA, is the series of the natural numbers. There are two basic problems with this though: the metaphysical problem of the ontological status of mathematical objects and mathematical structures, and the epistemic problem of how we have access to them so as to formalize/axiomatize. These are important issues, but they need not be solved before we embark on an axiomatization.

    Moreover, two people can disagree on the ontological status of e.g. the series of the natural numbers and yet perfectly agree on a given axiomatization thereof. So these are important issue, but I submit that they do not preclude talk of 'target phenomena' in such cases. We don't have the same clarity as to what the phenomena in question are as we do with physical phenomena (and even there, all kinds of tricky issues too!), but there is no doubt that there is *something* external we are trying to characterize, and being clear on that is an important aspect in the enterprise.

    However, it may well happen that we get more clarity on the phenomena precisely by means of a formalization, in a Carnapian vein. So I guess formalization is more of an open-ended, Neurath-boat kind of thing.

    ReplyDelete
  3. Hi Catarina,

    Many thanks!

    "I'd say that the target phenomenon of, for example, PA, is the series of the natural numbers. "

    Yes, that sounds about right, it's a bit more in two ways:

    1. The target domain is the *structure* consisting of the series and the distinguished operations $S$, $+$ and $\times$ on them. In other words, the structure $\mathbb{N} = (N, 0, S, +, \times)$.
    One can also expand this, or take reducts, and see what happens. For example, the theory of $(N, 0, S, +, \times)$ is not recursively axiomatizable, but the theory of $(N, 0, +)$ is decidable (Presburger arithmetic). If one just considers the series, i.e., $(N, <)$, this theory is decidable. So which operations/relations on $N$ are taken as primitive can make a huge difference.

    2. What we formalize into axioms is our *knowledge* of the domain. I.e., propositions about $\mathbb{N}$ which we accept, for whatever reason, as true. This knowledge is partial and incomplete.

    "There are two basic problems with this though: the metaphysical problem of the ontological status of mathematical objects and mathematical structures, and the epistemic problem of how we have access to them so as to formalize/axiomatize."

    Ok, but I have a tu quoque!
    For presumably you assume a theory of syntax in your own work - and this theory itself adopts an infinity of expression types and is as strong as $PA$ is. Even the most elementary discussion of syntax (e.g., what you call formation and transformation rules) contradicts nominalism. Even with a finite alphabet $A$, one assumes all finite sequences $(a_0, ..., a_n)$ with $a_i \in A$, with closure under concatenation and substitution.

    I think, in the end, your view is that formalization is not translation. In my view, formalization is translation.

    Jeff

    ReplyDelete
  4. Hi Catarina, here's another comment, this time on p. 88

    "(SYNCOM) For every formula $\phi$ in the relevant domain of discourse, FS either proves $\phi$ or it proves its contradictory.
    (SEMCOM) For every formula $\phi$, if what $\phi$ says is the case in MO, then FS proves $\phi$."

    I think, for the first of these, you must mean negation-completeness? (which it needn't be understand syntactically; it can be understood as semantic consequence too. E.g., second-order arithmetic $PA_2$ is negation-complete in the semantic sense (assuming standard models), but not the deductive sense.) This notion is usually applied to theories.

    Negation-Completeness
    Let $\mathcal{L}$ be a formalized language and let $T$ be a theory in $\mathcal{L}$. Then $T$ is negation-complete iff for all $\phi$, either $T \vdash \phi$ or $T \vdash \neg \phi$.

    So, I suspect the first should be called "(NEG-COM)" or something like that.

    For the second, this is quite different from negation-completeness - it's the completeness of the deductive system with respect to the class of (semantic) validities - as in Gödel's completeness theorem.

    Completeness
    Let $\mathcal{L}$ be a formalized language such that the notion of being valid (i.e., "true in all $\mathcal{L}$ interpretations) is understood and let $D$ be a deductive system for $\mathcal{L}$. Then, $D$ is complete iff, for all $\phi$, if $\phi$ is valid, then $\vdash_D \phi$.

    Gödel's completeness theorem involves completeness of any of the many deductive systems for FOL with respect to the notion of validity; Gödel's incompleteness theorem involves the notion of negation-completeness ("any consistent recursively axiomatizable extension of $Q$ is negation-incomplete")

    To make matters a bit more complicated, it's sometimes generalized, as your formulation of (SEm-COM) suggest, to apply to "completeness with respect to some given set of truths". E.g., any system $T$ of arithmetic extending $Q$ is $ \Sigma_1$-complete. I.e., if $\phi$ is a $\Sigma_1$ truth, then $T \vdash \phi$.

    Jeff

    ReplyDelete
  5. Thanks, Jeff! I was mostly following Awodey & Reck 2002 in this section, but I will give it some thought tomorrow first thing (calling it a day now).

    ReplyDelete
  6. Hi Catarina,

    By the way, I've really enjoyed reading this, and I've learnt lots of interesting stuff.

    So, here's the result of negation-completeness for second-order Peano arithmetic, $PA_2$, so long as we have full/standard models (not general, or "Henkin", models).

    Lemma 1: If $M$ is a (full) model of $PA_2$, then $M$ is isomorphic to $\mathbb{N}$.
    (To prove this, take the denotations of the terms $\underline{n}$ (i.e., terms of the form $S(S(....(0)...))$) in $M$. Then one can show that every element of $M$ is one of these terms. Defining the obvious mapping $f: N \rightarrow M$ by $f(n) = (\underline{n})^M$, we can show that $f$ is an isomorphism.)

    It follows from this that,

    Lemma 2: $\phi$ is a semantic consequence of $PA_2$ iff $\phi$ is true in $\mathbb{N}$.

    Then we get:

    Lemma 3. $PA_2$ is negation-complete (with respect to full second-order consequence). I.e., for all $\phi$, either $\phi$ is a semantic consequence of $PA_2$ or $\neg \phi$ is a semantic consequence of $PA_2$.

    (The proof is simply based on, first, the fact that: either $\phi$ is true in $\mathbb{N}$ or $\neg \phi$ is true in $\mathbb{N}$ (this uses the law of excluded middle in the semantic metatheory). Then use Lemma 2.)

    In fact, these are the three main theorems about $PA_2$ with standard, full, models. The first is what attracts some philosophers (e.g., Stewart Shapiro) to second-order theories - since they may function (modulo some strong assumptions) as "implicit definitions".

    Jeff

    ReplyDelete
  7. Hi Jeff,
    So I went through that section of chapter 3 again: it was a mess! Clearly what I wanted to talk about was only *deductive* incompleteness, so now I've re-written it so as to make that explicitly. That section is not supposed to be highly technical or anything, it's simply meant to flag these interesting, intrinsic limitations in formal methodology for the reader with a general background. But obviously, I should still be precise and not make claims that don't check! I hope it's fixed now -- thanks to you :)

    ReplyDelete
  8. Hi Catarina, thanks.
    The technicalities get heavy, quickly, particularly with second-order logic! And there's non-uniformity in the literature with the usage of "complete"; in practice, "complete" is overloaded, much as the symbol "$\models$" is overloaded, to mean either "satisfies" or "implies".

    Jeff

    ReplyDelete
  9. Jesus Christ, did you write this book in WORD?

    Even I use Latex these days and I'm just a life scientist. You should definitely know better.

    ReplyDelete
  10. So much for constructive criticism... And anonymous also, how brave! :)

    ReplyDelete