# Does there exist a first-order theory $T$ and a proof system $\vdash$ such that $T\vDash\phi$ iff $T\vdash\phi$, but $\vdash$ is not complete?

Let $L$ be a first-order language and $T$ a theory in $L$. (Here I take "theory" simply to mean a set of sentences in $L$.)

Under the standard semantics $\vDash_{std}$ and any standard proof system $\vdash_{std}$, we have strong soundness and strong completeness: for all first-order languages $L$ and for all sentences $\phi$ in $L$ and for all theories $T$ in $L$, $T\vDash_{std}\phi$ iff $T\vdash_{std}\phi$.

I'm wondering whether, given $L$, there is always an alternative proof system $\vdash_{*}$ such that there exist theories $T$ in $L$ for which $T\vDash_{std}\phi$ iff $T\vdash_{*}\phi$, even though $\vdash_{*}$ isn't strongly complete -- i.e. even though semantic and syntactic consequence don't coincide hold for all theories $T$.

Perhaps the question is trivial if we pick a silly enough proof system, but I've been away from logic for a while and am getting lost in quantifiers (does the language matter?). Perhaps one strategy is to imagine ditching some of the axioms or inference rules of a standard axiomatic proof system: we'll lose completeness of $\vdash_{std}$, so we'll lose the semantics-syntax correspondence on some theories, but will we necessarily lose it on all theories?

If the question is trivial, can it be perturbed to something interesting nearby?

EDIT: Per my own example (take $T$ to be $\left\{\forall x(x\neq x)\right\}$ and $\vdash_{*}$ to be the standard system without quantifier axioms, except for universal instantiation) and that of user Apostolos (take $T$ to be complete in the sense of containing, for each sentence $\phi$, either $\phi$ or its negation, and let $\vdash_{*}$ be the empty system, with no rules and no axioms), the answer to the question in the title is yes.

But what if we require $T$ to be consistent and $\vdash_{*}$ to be nonempty (i.e. to have some axioms and inference rules)?

• Or maybe the more interesting or appropriate setting for the question is second-order logic, where there are no $\vdash$'s that are strongly complete (given other nice properties we want: effectiveness and soundness). So: are there second-order theories where $\vDash$ and $\vdash$ coincide (even though they obviously cannot coincide for all theories)? Is there any interesting difference between this second-order question and the first-order situation? – symplectomorphic May 2 '17 at 22:25
• If $T$ is a complete theory then you can pick a proof system with no rules or axioms (hence it can only prove statements in $T$) and what you ask for will hold, because $T$ is complete. – Apostolos May 2 '17 at 22:57
• @Apostolos: ah, right. I had a strong hunch the question was trivial: I just couldn't put my finger on an example at first. I realized just before you posted that taking $T$ to be inconsistent works as well (see my comment on the answer below). – symplectomorphic May 2 '17 at 23:06

One obvious counterexample is to take $T$ to be inconsistent but preserve enough of the proof system to get the principle of explosion -- e.g. take $T$ to be the set consisting of the single sentence $\forall x(x\neq x)$, and $\vdash_{*}$ to be the standard proof system minus any quantifier axioms/rules except universal instantiation.
User Apostolos also points out in the comments that taking $\vdash$ to be the empty proof system (no axioms, no inference rules) and $T$ to be any theory such that for all sentences $\phi$ either $\phi\in T$ or $\lnot\phi\in T$ works as well. (E.g. take $T$ to be the theory of the natural numbers.)