It is my understanding that Gödel Encoding and "Arithmetization of Syntax" can be used to represent any logical system. This is exemplified by the encoding of a Universal Turing Machine.
"According to model-theoretic interpretation, the semantics of a logical system describe whether a well-formed formula is satisfied by a given structure." - Wikipedia - Formal Systems
Since satisfiable
is defined with syntactic rules, this seems to easily lead to the following controversial claims:
(1) The semantics of any logical system are able to be represented as syntax via the (orthodox) model-theoretic interpretation.
(2) A logical system (semantics included) is able to be represented entirely with syntactic rules alone.
(3) Semantics of a logical system which cannot be represented in the syntax of a logical system are merely stuff we haven't formalized yet (they aren't well-defined in the system).
My understanding is that these claims are outrageous/iconoclastic and would not be generally accepted, but I don't understand how that's the case. How is it that these claims are incorrect?
To venture an analogy, how could a logical system be a logical system if it depends on rules specified outside of the system? How could a computer perform a procedure whose instructions aren't specified in terms of operations it can perform?
@AndrejBauer gets quite close to the topic in this post:
In classical treatments of first-order logic and model theory, the dichotomy between syntax and semantics is quite pronounced, and one easily gets the impression that it is necessary. Students are taught that finitary syntax must be the norm. However, this really is just a design choice.
Perhaps I'm merely rebelling against this "design choice" for subjective reasons, which would mean that my above claims are "correct, but insignificant"?
Later in the same post @PeterLeFanuLumsdaine offers:
In summary, if syntax is not set up as independent from semantics, but just for a specific fixed structure, then one loses the distinction between existential quantifiers and infinitary disjunctions indexed by the domain. Similarly, one loses the distinction between having infinitely many constants in the language and infinitely many elements in the domain, and so on.
In this case my second claim would become: We can augment the current syntax so as to set up these independent notions in syntax itself. It seems to me that that is precisely what is done in practice (unavoidably) as the field of mathematics progresses.