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?

174 Views Asked by At

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

1

There are 1 best solutions below

0
On BEST ANSWER

Belatedly realizing that in its current formulation, my question is indeed trivial.

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