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 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).
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).