How can FOL logic be at the same time complete and only semi-decidable?
in [Logic]
|
Prev: Problem: how can first-order logic be at the same time complete and only semi-decidable?
Next: How can FOL logic be at the same time complete and only semi-decidable?
From: cesare cassiobruto on 7 Aug 2010 09:21 Hi, I'm new to this forum. I have a doubt about completeness and decidability in First-order logic that I cannot solve: how is it possible for first-order logic to be at the same time complete and only semi-decidable? Let me explain. In 1930 Kurt Goedel demonstrated the completeness of first-order logic (I mean FOL: logic with predicates and quantifiers): 1) if a sentence A of FOL is valid, i.e. it is a logical consequence of the axioms, (that is it cannot be false while the axioms are true, and this is a semantical concept), then A is a theorem, i.e. it is (syntactically, mechanically) derivable in the language of FOL from the axioms. The converse, that 2) every theorem is valid comes from the already demonstrated soundness of FOL. so, 1) and 2) together allow us to say that, at least in FOL, the concept of validity (so that of truth) and that of being derivable have the same extensionality: in other words, every true statement of FOL is a theorem of it and vice-versa (this does not hold for arithmetic, where for Goedel incopleteness theorem, 1931, if arithmetic is sound, there ARE true statements that are NOT theorems). BUT, it is also demonstrated that FOL is not decidable, that it is only semi-decidable: 3) DEF.: A theory T is semi-decidable if, given a statement P in the language of the theory, it does exist a general mechanical procedure (let's call it Theorem Checker, with argument A TC(P)) for determining if P is a theorem, that outputs a positive answer in a finite time if P is actually a theorem, but does not halt at all if P is not a theorem. Let's give the definition of decidability for a theory also: 4) DEF.: A theory T is decidable iff given a statement P in the language of the theory, it does exist a general mechanical procedure that always ends in a finite time for checking if P is or is not a theorem of T. From the known semi-decidability (3) of FOL, given a statement A expressed in the language of FOL, it follows that if A is a theorem of FOL, then a mechanical theorem checker TC(A) will certainly halt after a finite amount of time. But that if A is not a theorem, TC(A) will NEVER halt. Now, if A is NOT a theorem, then from the completeness of FOL (1), it follows that A is not valid, i.e. it is false. So, not-A is true, i.e. it is valid. But then again, from the completeness of FOL it follows that not-A is a theorem. So, we know that a procedure TC(not-a ) for checking if not-A is a theorem WILL halt, eventually, saying it is a theorem. SO, given a generic A, of which we don't know it is a theorem or not, we could build a mechanical procedure TC2(A) ALTERNATING at each step TC(A) and TC(not-A), knowing that, being either A or (not-A) a theorem, TC2(A) WILL stop in a finite time (TC2 a is built with the condition that, as soon as one of its subroutines TC(a) or TC(not-a) halts, so does the entire TC2 procedure). So, given the definition of decidability (4) and the always-ending procedure TC2 described above, (which relies on the completeness of FOL (1)) we can now say FOL IS decidable! SO, it seems that if FOL is complete, then it IS DECIDABLE. How come than that there is a well known demonstration (involving the halting problem for a Turing machine) that it is NOT?!?! (i.e. that it is only semi-decidable)? Sorry for the long and complex post, but I had to explain the question carefully. I hope some of you can shed some light on this (for me) paradox. Thanks a lot
From: cesare cassiobruto on 7 Aug 2010 10:29 > first-order logic is not complete in the relevant sense. That is, it is > not the case that for any formula A, either A or the negation of A is > logically provable. Please, have the patience to elaborate more on that. Do you mean that from the fact that a sentence A is not valid, i.e. it is not true in EVERY interpretation, it does NOT follow that not-A is true in every interpretation? Of course I missed this subtlety. So the wrong passage, if applied to FOL is >Now, if A is NOT a theorem, then from the completeness of FOL (1), it >>follows that A is not valid, i.e. it is false. So, not-A is true, i.e. >>it is valid. so, the error lies in the passage from not-valid to FALSE. Did understood you answer correctly? thanks a lot:)
From: Colin on 7 Aug 2010 13:07 On Aug 7, 8:21 am, cesare cassiobruto <vjq...(a)gmail.com> wrote: > Hi, I'm new to this forum. I have a doubt about completeness and > decidability in First-order logic that I cannot solve: how is it > possible for first-order logic to be at the same time complete and > only semi-decidable? Let me explain. > [snip] > > Now, if A is NOT a theorem, then from the completeness of FOL (1), it > follows that A is not valid, i.e. it is false. So, not-A is true, i.e. > it is valid. But then again, from the completeness of FOL it follows > that not-A is a theorem. So, we know that a procedure TC(not-a ) for > checking if not-A is a theorem WILL halt, eventually, saying it is a > theorem. This is where you go wrong. Yes, if A is not a theorem then A is not vaild. But, no, that does mean that not-A is therefore valid. A being invalid simply means not-A is satisfiable in SOME model. For not-A to be valid it would have to be valid in EVERY model. (You yourself seem to have finally gotten this point in your response to Aatu's post.)
From: cesare cassiobruto on 7 Aug 2010 13:24 On 7 Ago, 19:07, Colin <colinpoa...(a)hotmail.com> wrote: > On Aug 7, 8:21 am, cesare cassiobruto <vjq...(a)gmail.com> wrote: > > > Hi, I'm new to this forum. I have a doubt about completeness and > > decidability in First-order logic that I cannot solve: how is it > > possible for first-order logic to be at the same time complete and > > only semi-decidable? Let me explain. > > [snip] > > > Now, if A is NOT a theorem, then from the completeness of FOL (1), it > > follows that A is not valid, i.e. it is false. So, not-A is true, i.e. > > it is valid. But then again, from the completeness of FOL it follows > > that not-A is a theorem. So, we know that a procedure TC(not-a ) for > > checking if not-A is a theorem WILL halt, eventually, saying it is a > > theorem. > > This is where you go wrong. Yes, if A is not a theorem then A is not > vaild. But, no, that does mean that not-A is therefore valid. A being > invalid simply means not-A is satisfiable in SOME model. For not-A to > be valid it would have to be valid in EVERY model. (You yourself seem > to have finally gotten this point in your response to Aatu's post.) Yes, now I finally grasped it. Intuitively, I think the problem is, when you talk about logic you don't talk about a formal system which is intepreted in a fixed model, so you forget that in FOL not every sentence is simply true or false, but that can be true in a possible world and false in another. While when talking about let's say, arithmetic, you talk about an intepreted system for which every statement is either true or false, and being not true means being false. In logic, when you say it's a validity you don't simply say it's true, but that it's true in every possible interpretation. Anyway, such questions always confuse me a bit. For example: decidability Is the definition I cited correct? It was this one: DEF.: A theory T is decidable iff given a statement P in the language of the theory, it does exist a general mechanical procedure that always ends in a finite time for checking if P is or is not a theorem of T. BUT in many textbooks I found a definition that states " for checking if P is or is not a VALID formula of T". So, it seems the first one is SYNTACTICAL, the second a SEMANTIC requirement. Accfording to yuo, which is the standard meaning of "decidable theory"? Which it seems to this is the same as asking "what do we mean with 'theory', the set of all derivations from the aìxioms (syntax) or the set of all logical consequences (semantics)?" What is your opinion? Moreover, can anybody of you please clarify the distinction between syntactic an semantic completeness? I found many definitions of them, not always clear. Is this distinction related in a way to the distinction between the two definition of decidability I mentioned above? Thanks a lot Edit / Delete Edit Post Quick reply to this message Reply Reply With Quote Reply With Quote Multi-Quote This Message Thanks
From: George Greene on 8 Aug 2010 19:08
On Aug 7, 9:21 am, cesare cassiobruto <vjq...(a)gmail.com> wrote: > Hi, I'm new to this forum. I have a doubt about completeness and > decidability in First-order logic that I cannot solve: how is it > possible for first-order logic to be at the same time complete and > only semi-decidable? Aatu K.'s replies are often abusive. There is a very simple answer to your question. > Let me explain. No; let ME explain. The word "complete" is being used in two DIFFERENT senses. > In 1930 Kurt Goedel demonstrated the completeness of first-order logic Exactly. And the sense in which he proved this logic complete IS NOT the SAME sense in which he subsequently proved it INcomplete (that would, after all, be a contradiction). The answer to your question is that there are two different kinds of completeness at work here. Aatu knows this but his personal pedagogical strategy seems to involve withholding what is being clearly requested. The sense in which Godel proved FOL "complete" is DEDUCTIVE completeness. That is, he proved that some standard definitive system-of-rules-of- inference for FOL does, in fact, allow you to infer (from some axioms) ALL of the sentences that actually ARE LOGICAL CONSEQUENCES of those axioms. This is NOT circular because there are two A PRIORI DIFFERENT notions of logical consequence in play here. The content of the completeness theorem is that (for standard classical FOL, anyway) these two notions can be identified, because the deductive one "completely" covers the semantic one. The "semantic" definition of logical consequence is that a sentence Q is a logical consequence of some prior set P of sentences (premises) IFF EVERY MODEL of the premises (conjunctively) is also a model of the sentence, i.e., if every model of P is also a model of Q, i.e., if every model that makes every sentence in P true, also makes Q true. It was not a priori obvious that ANY set of deductive inference rules would produce all the relevant Q's from any P. > 1) if a sentence A of FOL is valid, i.e. it is a logical consequence > of the axioms, (that is it cannot be false while the axioms are true, > and this is a semantical concept), then A is a theorem, i.e. it is > (syntactically, mechanically) derivable in the language of FOL from > the axioms. Exactly. The first concept was "semantical" and the second one was syntactic. So they are not (a priori) obviously the same. It takes the proof to SHOW that they coincide, in the case of standard classical FOL. > > The converse, that > > 2) every theorem is valid > > comes from the already demonstrated soundness of FOL. > > so, 1) and 2) together allow us to say that, at least in FOL, the > concept of validity (so that of truth) Wrong. Validity is NOT the same as "truth" here. > and that of being derivable > have the same extensionality: in other words, every true statement of FOL THERE IS NO SUCH THING as a "true statement of FOL". Truth is from MODELS, NOT from LOGICS. It is a "semantical" concept, NOT a logical one. What the completeness theorem winds up meaning is that if a sentence is Valid-in-FOL then it is TRUE IN ALL MODELS into which the relevant language can be interpreted. In particular, the sentence expressing that the consequence follows from the premises (P -> Q, or P |- Q depending on your level of discourse) is true in all models, because Q is true in all models*OF*P, i.e. all models that make P true (and that are linguistically connected in the proper way to both P and Q). You DON'T GET ANY *TRUTH* from the logic or even the axioms: Having assumed an axiom true for the purposes of one investigation, you can always have a second investigation of what would happen instead, in the alternative, if it were false; NO axioms are inherently "true" UNTIL AFTER you have CHOSEN them as axioms. You get your TRUTHS from MODELS. |