symbol pushing

Stream: new members

[Huỳnh Trần Khanh]

what does that phrase mean? it has something to do with interactive theorem provers right

[Jason Rute]

Can you provide some context where you heard it? It sounds like a (possibly pejorative) way to say symbol manipulation. In some sense, theorem provers (and all formal systems) are based around purely syntactic rules, which I guess someone could call symbol manipulation, or "symbol pushing".

[Jason Rute]

Are you familiar with the distinction between syntax (formal rules, grammars, and symbols) vs semantics (meaning)? Proving systems like first order logic or Lean's foundations are syntactic rules that say when it is and is not okay to write something in a proof (and Lean, for example, rigorously checks that you are following these rules). This is the syntactic sides of logic (often called proof theory, and maybe "symbol pushing" :smile:). In this view, there is not specific meaning to the symbols, it is just a collection of rules.

On the other side of the coin, there is semantics. Formal systems like first order logic or Lean's foundations can be interpreted as saying something about mathematical objects. When you see \forall x, x = x you interpret that mentally as saying something about the usual equality relation you are familiar with in mathematics. This is semantics. The semantic side of logic is called "model theory". There are important and deep theorems in logic relating proof theory and model theory, and almost any concept in logic can be thought about in both a syntactic and a semantic manner.

[Huỳnh Trần Khanh]

https://coq.gitlab.io/zulip-archive/stream/237977-Coq-users/topic/Automation.20and.20.60mathcomp.60.2E.html#244015632

But even for symbol pushing, auto might diverge quite rapidly.

[Jason Rute]

Actually, based on how it’s been used here on this Zulip and the internet (from a quick Google search), I now think it likely just means routine calculations or symbolic manipulations that aren’t particularly insightful or interesting.