Non-string symbolic languages (e.g. diagrams) as "formal languages"

84 Views Asked by At

A formal language is a concept that is fundamental to computer science, logic, and metamathematics. It is defined as a subset $\mathcal L$ of the set $S^*$ of sequences of symbols from a set $S$, that can be generated by certain formal production rules.

The notion of formal language can be used to formalize certain notions mathematicians often think about somewhat informally/intuitively, the prime example being proofs.

However, there are symbolic languages that are not "strings of symbols", perhaps a prime example being categorical diagrams, e.g.:

enter image description here

While we can represent this diagram as a string (i.e. write a string that describes an algorithm to construct the diagram), the diagram doesn't naturally have the structure of a string.

My question is basically, Can we think of non-string languages like this as "formal languages", in the sense that we can treat them with the same degree of rigor as e.g. a proof calculus on first-order propositions (i.e. strings)? I have always thought of non-string languages like this as "relatively" more informal objects than the fully rigorous first-order logics to which we can apply automated theorem provers.

1

There are 1 best solutions below

0
On

Sure, this can be done. At its core, a deductive system (ignoring semantics for the moment) is a set of things called sentences together with a deduction relation on that set; there's no requirement that the sentences be strings or that the deduction relation be "generated by" operations on strings, and a deductive system based around (say) diagrams is perfectly possible.

For one example of such a thing, Hughes has presented an entirely graph-theoretic approach to classical propositional logic and first-order logic - neither sentences nor proofs are strings. They also aren't simply graphs, though, so this may not quite be what you're looking for, but I think it's still valuable to consider. In particular it illustrates the broader point that as long as we define things precisely, the components of our deductive system can be whatever we want.

(Implementing non-string-based deductive systems on a computer is of course a whole other issue, but that's a side point.)