8
$\begingroup$

Given a first-order logic theory $T$ and and a formula $F$, suppose I have semantically proved that $T\vdash F$. That is, I have proved that any model $M$ of $T$ satisfies $F$ and I conclude by Gödel's completeness theorem.

Do I have a general algorithm to extract from the above a syntactic proof of $T\vdash F$, i.e. a finite sequence of formulas that respects inference rules, uses $T$ and finishes at $F$ ?

If no such algorithm exists, then did I really prove $T\vdash F$ ? The completeness theorem was just an example of how to indirectly prove that there exists a proof of $T\vdash F$, without explicitly giving this latter proof. What if my indirect proof uses an inaccessible cardinal, do I have to mention the awkward $$ (\text{ZFC + Inaccessible cardinal})\; \vdash\; (T \vdash F) $$ And then this proof can also be indirect, so I might continue stacking theories to the left and it becomes a nightmare. Don't semantic or other indirect formal proofs somewhat defeat the purpose of formal logic, that we should be absolutely certain that the formal proofs exist and are correct?

|cite|improve this question
$\endgroup$
  • 2
    $\begingroup$ Re your last question, usually mathematicians are not actually interested in formal logic for some particular first-order theory. The interest in formal logic is only for foundational theories such as the ZFC in which the semantic argument is formulated. Then, this foundation is used to reason about other mathematical structures. $\endgroup$ – Eric Wofsey Oct 3 '18 at 20:29
  • 2
    $\begingroup$ To put it another way, a semantic proof is a perfectly good formal proof in first-order logic--it's just that the underlying theory is ZFC, not T. And the statement you are proving is $T\vdash F$, not $F$ itself. $\endgroup$ – Eric Wofsey Oct 3 '18 at 20:30
  • 1
    $\begingroup$ You don't mention that any more than you mention that any other proof was in ZFC. If you prove a theorem $P$ in algebraic geometry (using $ZFC$ as your foundation), say, you don't say that $ZFC\vdash P$. You just say that you've proved $P$ (and if someone asks what foundation you're working with, you tell them $ZFC$). Most of the time, no one really cares what exact foundation you are working with and the default is $ZFC$. $\endgroup$ – Eric Wofsey Oct 3 '18 at 21:00
6
$\begingroup$

Keep in mind that proofs are "easily-recognizable finite strings of symbols" - precisely, we can effectively enumerate all proofs from a given theory. So we can always find a formal proof of $F$ from $T$ - if one exists - effectively by simply checking each $T$-proof in order until we find one which is a proof of $F$. This is unsatisfying, but is perfectly precise and effective.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ @V.Semeria If there isn't actually a proof of $F$ from $T$, what do you want your algorithm to do? $\endgroup$ – Noah Schweber Oct 3 '18 at 20:45
  • 1
    $\begingroup$ @V.Semeria I still don't understand what you want the algorithm to do in this case. Suppose I come to you and present a proof $\pi$, from ZFC + "There is an inaccessible," of ZFC $\vdash p$. But secretly ZFC + "There is an inaccessible" is inconsistent, and in fact ZFC $\not\vdash p$. What do you want your algorithm to do when given $\pi$ (keeping in mind that you don't know at the moment that ZFC + "There is an inaccessible" is inconsistent)? $\endgroup$ – Noah Schweber Oct 3 '18 at 22:21
  • $\begingroup$ On second thought, yes, the risk that this brute force search never terminates perfectly reflects the risk that the stronger theory I used to prove the existence of the formal proof is inconsistent. $\endgroup$ – V. Semeria Oct 7 '18 at 15:46
  • $\begingroup$ @V.Semeria Or worse, is consistent but wrong (= consistent but not $\Sigma_1$-sound) - that way you don't even find out down the road that you were wrong to trust it in the first place! $\endgroup$ – Noah Schweber Oct 7 '18 at 15:47

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.