Logic done with syntax trees instead of sequences of characters?

Last year, I took a course in logic. In it, sentences were defined inductively as sequences of characters in a certain way. I am now reading Shoenfield as an attempt to look deeper into the subject, and he too defines sentences as sequences of characters.

The first theorem he proves is effectively equivalent to: any sentence can be uniquely parsed into a syntax tree.

That said, why not forego the definition of sentences as sequences, and use syntax trees from the get-go? Is there any benefit to using sequences, other than that being how we are used to writing propositions? Does anyone out there forego sequences entirely?

• At a guess, because it's more natural and there's no particular reason to look at them as trees, except maybe in the particular cases where you want to use structural induction. And even then you don't need to talk about trees if you don't want to. – Malice Vidrine Jul 28 '19 at 19:08
• @MaliceVidrine In my experience (which is much more Programming Language Theory/Type Theory), you want to do structural induction over the syntax trees far more often than you want to do structural induction over the sequences of characters. PLT folks virtually never care about the sequence of characters unless they are implementing a parser. If you code logics up or formalize them in something like Agda/Coq, you usually won't specify the parsing details but will work entirely in terms of the abstract syntax trees. – Derek Elkins left SE Jul 28 '19 at 23:42
• If I remember correctly, Barwise's book "Admissible Sets and Structures" uses what amounts to trees (in a set-theoretic representation) as the official syntax. I suspect the same is true in other work on infinitary logic, because linear syntax is a mess there. (As a grad student, I sat in on a course in infinitary logic where the instructor used linear syntax, and I can personally testify that it was a mess.) – Andreas Blass Jul 29 '19 at 0:41
• @AndreasBlass Oof - that definitely doesn't sound ideal. How did they even do it? Was it (morally equivalent to) just the Kleene-Brouwer order of the syntax tree? – Noah Schweber Jul 29 '19 at 0:42
• I've repressed a lot of memory of the mess, but I remember that formulas were well-ordered sequences of symbols, including parentheses, and that a good deal of work went into showing unique readability. (I don't think he even used a symbol for infinitary conjunction; the conjuncts would be written in a long sequence with $\land$'s between them, but I don't remember this with any certainty.) – Andreas Blass Jul 29 '19 at 0:49

In my experience, which is more programming language theory (PLT) and type theory (and generally CS-y) than traditional logic, we virtually never work in terms of sequences of characters. I, personally, view logic texts that put a lot of focus on this as using their time/space poorly. This made a bit more sense before computers were widely used. It's certainly important to know that you can go between sequences of characters and trees in a computational way, but it's not a hard to believe fact, and the details of it are almost always irrelevant. As long as you know what tree is represented by the text in the book, that's generally all you need to know.

I'm not aware of any introductions that actually draw the trees as a matter of course as that would be quite verbose and typographically awkward.

What PLT/etc. people usually do is write pseudo-CFGs (context free grammars) such as $$\varphi,\psi ::= A \mid \varphi\supset\psi \mid \bot$$ and then go on to write things like $$((P\supset\bot)\supset\bot)\supset P$$ with only, maybe, some informal comments about precedence, grouping with parentheses, and the syntax of atomic formulas.

In formal (i.e. machine-checked) expositions or other code operating on logic, you'll see data types like:

data IPC⟨→⟩ : Set where
⋆_  : V → IPC⟨→⟩
_⊃_ : IPC⟨→⟩ → IPC⟨→⟩ → IPC⟨→⟩
⊥c  : IPC⟨→⟩


which describes the syntax tree of IPL but not really the concrete syntax. (Of course, the definition of Agda, in this case, specifies the syntax of code that uses these constructors.) You can't do an induction on the sequence of characters making up the formulas as there isn't one. If you wanted to do such a thing, you'd have to define a function from this type into the type of sequences of characters (and prove theorems that such an encoding is faithful). If you read the full article from which I got the above data type, it never does this nor needs to.

This isn't to say that the field of formal languages, i.e. parsing theory and context free grammars etc., isn't interesting. It's just not logic, though they often share techniques.

There are indeed situations where syntax trees are more easy to handle than sentences-as-strings - every induction-on-complexity argument provides such an example. However, the converse also holds sometimes - e.g. it's a bit easier to linearly order the set of sequences, and we often want an enumeration of the expressions in our language.

Ultimately, though, the translation between the two is elementarily enough that their respective technical advantages/disadvantages quickly stop mattering. In light of this, we primarily use sequences since they better match what we actually think of as "sentences." One aspect of this is that I think sentences are generally easier to parse than syntax trees. They're also easier to write on a page - trees take up a lot more space.

In summary, the mathematical differences between the two aren't obviously substantial enough to provide strong motivation in either direction, and sentences seem to have a nontrivial "human advantage" over trees.

• If the question is whether we should draw trees or write formulas in our books, then clearly we should do the latter. If the question is should we include parentheses in our description of syntax and proof unique reading lemmas or talk about trees and just informally describe how the textual formulas we write correspond to them, then it's clear to me that we should do the latter. That is, we define formulas to be these tree like things and then we give a notation for these trees in the same way we would for vectors. – Derek Elkins left SE Jul 29 '19 at 0:24
• It seems to me that Gödel numbering trees isn't bad: $\langle\text{code of root, code of left subtree, code of right subtree}\rangle$. If you code sequences directly, then the coding is easy, but all the definitions of things like "$x$ is free in $\alpha$" seem to need to include descriptions of the parsing algorithm, which is trivial for trees. – Andreas Blass Jul 29 '19 at 0:36
• Now that I"m in my office, I checked how Gödel numbering is done in a few textbooks. Shoenfield's "Mathematical Logic" and Hinman's "Fundamentals of Mathematical Logic" code the syntax trees, as I suggested in my previous comment. Enderton's "A Mathematical Introduction to Logic" codes llinear sequences of symbols. – Andreas Blass Jul 29 '19 at 22:09
• @AndreasBlass Yes, you're right - I take back my comment. – Noah Schweber Jul 30 '19 at 15:58