Understanding the syntactical completeness

A formal system is syntactically complete if for each sentence (closed formula) $\varphi$ either $\varphi$ or $\lnot \varphi$ is provable.

A formal system is semantically complete if every sentence (closed formula) $\varphi$ which is tautology is provable.

What I wonder is

  1. The Godel's first incompleteness theorem states that there is a sentence $\varphi$ in Peano's arithmetic which is true, but which is not provable and which negation is not provable, so it is at the same time syntactic and semantic incompleteness theorem, right? Is it right to say that the semantic incompleteness is more essential result since it implies the syntactic incompleteness under the assumption of soundness?

  2. Consider the formula $P$ in propositional calculus where $P$ is a propositional variable from the signature. It is syntactically incomplete since neither $P$ nor $\lnot P$ is not a tautology, and by the semantical completeness of propositional calculus, we can conclude that neither $P$ nor $\lnot P$ are deducible. However is there a way to prove that neither of them are deducible syntactically, without the semantic argument?

  3. Are there any examples of useful syntactical complete formal systems?


On (1). In more standard terminology:

A formal theory is [negation] complete if for each sentence (closed formula) φ either φ or ¬φ is provable.

A logical deductive system is semantically complete if every sentence (closed formula) φ of the system which is a logical truth is provable.

Gödel's incompleteness theorem shows that first-order Peano Arithmetic isn't negation complete. (And trivially, since one of either φ or ¬φ is true on the standard interpretation, there is a truth PA can't prove).

But the first-order deductive system built into PA is still semantically complete (by Gödel's completeness theorem!).

It was/is important that Gödel's official incompleteness result is a purely syntactic one, proved on purely syntactic assumptions. For recall the context back around 1930. Semantic notions (pre-Tarski) were widely thought murky and "unscientific"; and the major research programme in foundations in Gödel's environment was the Hilbertian program which presupposes that we can completely axiomatize swathes of mathematics. Showing on syntactic assumptions that the Hilbertians would have to buy that we can't even get a complete theory of elementary arithmetic was therefore devastating.