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

  • $\begingroup$ 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? $\endgroup$ – symplectomorphic May 2 '17 at 22:25
  • 1
    $\begingroup$ 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. $\endgroup$ – Apostolos May 2 '17 at 22:57
  • $\begingroup$ @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). $\endgroup$ – symplectomorphic May 2 '17 at 23:06

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

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.