Is syntactic consequence required to define semantic consequence?

I have read quite a number of the questions on stack exchange to try to understand the relationships/differences between syntactic consequence, semantic consequence, and material implication.

For example in this post: https://philosophy.stackexchange.com/questions/10785/semantic-vs-syntactic-consequence, the definition of semantic consequence is given as Γ ⊨ φ says: sentence φ is true in all models of Γ. A similar definition is given here: https://math.stackexchange.com/questions/365569/whats-the-difference-between-syntactic-consequence-⊢-and-semantic-consequence-⊨. In particular that we have to have the entailed sentence be 'true'.

From this I am wondering does 'truth' in the definition of semantic consequence require the use of syntactic consequence? That is, do we first need the notion of syntactic entailment in order to define this semantic consequence?

• any particular reason why you think it would? Commented Jul 18, 2020 at 20:44
• @spaceisdarkgreen my thought process was that if it wasn't true, then we have no way of defining what 'truth' means in this context. I did think about whether this could be addressed by defining the truth literally by assigning it a value under the interpretation Commented Jul 18, 2020 at 21:00
• @spaceisdarkgreen (cont) but my understanding of what an interpretation is, is that's it's an assignment of meaning to the symbols of some formal language. So that would mean in order to deduce the truth of a statement, we would need to follow the rules of inference starting from the set of symbols we have assigned truth to. This seems to me like syntactic entailment, but I also feel like I have a misunderstanding of some of the concepts.. Commented Jul 18, 2020 at 21:04
• Semantics (and syntax for that matter) is defined in a mathematical background, and if we formalize this background, we will have some notion of formally proving that a sentence is valid... but this is a proof in a different system. If we use a natural deduction proof system for the original system, a formal proof of a statement and the semantic argument that it is valid will typically look very much alike (hence the 'natural'). Commented Jul 18, 2020 at 21:10
• As @spaceisdarkgreen is saying you are need to be clear about the distinction between the object language you are studying , e.g., Peano Arithmetic (PA), and the metalanguage you are using to study it, e.g., Zermelo-Frankel Set Theory (ZF). See this discussion of the work of Tarski on the definition of truth. Commented Jul 18, 2020 at 21:20

Any sensible system of logic (e.g. propositional calculus or predicate calculus) is sound ($$p$$ the syntactic consequence of $$\Omega$$ implies $$p$$ is the semantic consequence of $$\Omega$$. That means that if something is provable (from a set of premises) then it must be true (assuming the premises are true). This seems necessary if proof is going to mean anything. The non-trival theorem is whether $$p$$ being the semantic consequence of $$\Omega$$ implies that $$p$$ is the syntactic consequence of $$\Omega$$. i.e. if something is true then it is provable. This is true for the propositional calculus with a finite set of premises. It requires the axiom of choice to prove it for propositional calculus with an infinite set of premises and, of course, it is not true for any formal system that includes arithmetic (as shown by Godel).