A question on XOR
in [Logic]
|
Prev: Accounting Information Systems 11E Romney Solutions manual
Next: Godel had no idea what truth is so incompleteness theorem is meaningless
From: Jan Burse on 8 Aug 2010 15:32 Nam Nguyen schrieb: > Thanks for the link. As mentioned with JB, the context here > is "FOL proof". My intention is to claim (A xor ~A) _signify_ > the impossibility to syntactically prove the consistency of > a consistent system. But I'm not so sure the formula would > be a correct characterization of such. The problem here is that you're changing the formula, the formula where the notion "tautology" is applied to. But I guess for your venture you probably need to change the notion. Go more down to the bowels of truth respectively derivation. One way to do it, would be to use a modual logic of provability. There you would have available inside the logic what is usually only available out side. The modal operator can refer to interpretations, like we do in the notion of tautology. Alternatively the modal operator could also refer to derivations, like it is done in the notion of valid consequence. Lets try the later. Let []A denote that there is a derivation for A. Then consistency is simply ~[]f, see below. Then the imposibility to prove this would be ~[]~[]f. Well this is just a shoot from the hip. No clue whether this would really work out to the end. The problem that now remains is a precise definition of your provability logic, and of course a derivation of a all the necessary theorems, if possible. > The scodnary intention is to go from there and find a replacement > for CON(T) that doesn't depend on the notion of the natural numbers. > (A very long shot though, imho). CON(T) should be the same as T |/- f. So falsum is not derivable from the theory T. By the deduction theorem this is the same as: |/- T -> f Which is the same as: |/- ~T So the negation of the theory T is not derivable. This of course only works when T is finitely representable. I.e. when it is not an infinite set of formulae. When it is a finite set of formulae we can take the conjunction and we will stay in FOL.
From: Jan Burse on 8 Aug 2010 15:47 Jan Burse schrieb: > Nam Nguyen schrieb: > >> Thanks for the link. As mentioned with JB, the context here >> is "FOL proof". My intention is to claim (A xor ~A) _signify_ >> the impossibility to syntactically prove the consistency of >> a consistent system. But I'm not so sure the formula would >> be a correct characterization of such. > Lets try the later. Let []A denote that there is a derivation > for A. Then consistency is simply ~[]f, see below. Then the > imposibility to prove this would be ~[]~[]f. Well this is > just a shoot from the hip. No clue whether this would really > work out to the end. The problem that now remains is a precise > definition of your provability logic, and of course a derivation > of a all the necessary theorems, if possible. Looks like ~[]~[]f does not really say what you wanted to say. First of all I was using the wrong modal operator. It seems that <>A is better suited to denote derivation, since <> usually indicates a possibility(*). Then we would need to distinguish between two modal operators. One for the semantical truthness in all interpretations [1] and one for the syntactic derivability <2>. Then I guess what you want to say would be, where T is your theory you are examine: ~[1]~T |/- ~<2>~T The outer |/- is again a modal operator. So maybe the whole thing would boil down to: ~<2>(~[1]~T -> ~<2>~T) Bye (*) But in literature they neverthelss use the box instead the diamond. http://en.wikipedia.org/wiki/Provability_logic
From: Nam Nguyen on 8 Aug 2010 19:44 Jan Burse wrote: > Nam Nguyen schrieb: >> Please note the word "proof" in my "As far as FOL proof is >> concerned". Are we then saying in _all_ formal systems >> there's a _proof_ for (A xor ~A)? > > Your saying "As far as FOL proof is concerned (A \/ ~A) > signifies a tautology" doesn't make much sence. Let's not fight with terminology where we don't have to. We could have coined a new term "syntactical tautology", "logical theorem-hood", etc... The point is from the syntactical point of view it'd signify something, just as (A /\ ~A) would signify the consistent theory of the underlying language. > Since > the notion tautology is not related to derivability > in a proof system, it is related to a notion of truth. One could say tautology definition is based on the notion of truth values, but as far as FOL provability is concerned I'd not say it's not "related" to provability. There's such a thing as the (meta) Tautology Theorem, which concerns about provability of some formulas. > > A tautology(*) is a formula that is true under all > interpretations. A proof system does not primarly > define a notion of interpretation. A proof system > usually defines a notion of derivation. Right. > > But what should your saying "As far as FOL is concerned > (A /\ ~A) signifies a contradiction" mean? The difficulty > here is the same. It's not the same. (A /\ ~A) represents an inconsistent theory _where contradictions can be proven_ ! > The notion of contradiction, as > a property of a formula, is not related to derivability > in a proof system, it is related to a notion of truth. That's simply not true: semantically, (A /\ ~A) means a contradiction! > > A contradiction(*) is a formula that is false under all > interpretations. Be that as it may, a contraction could also be defined as a formula of the form (F /\ ~F) for some formula F. All this still doesn't make it wrong to ask what (A xor ~A) would syntactically signify within the context provability w.r.t. to a particular T. You yourself said "A xor ~A is also a tautology" so apparently it does signify a "logical-theoremhood", as far as FOL proof is concerned, right? -- ----------------------------------------------------------- Normally, we do not so much look at things as overlook them. Zen Quotes by Alan Watt -----------------------------------------------------------
From: Nam Nguyen on 8 Aug 2010 22:35 Nam Nguyen wrote: > > The [secondary] intention is to go from there and find a replacement > for CON(T) that doesn't depend on the notion of the natural numbers. > (A very long shot though, imho). It still seems a long short but let me attempt. The meta statement I think we'd like to make would be something like (*) Let T be a formal system satisfying certain "conditions", then if T is consistent there is a formula of L(T), named say KONT(T), that is true but not provable in T. Where "conditions" would be anything except "as strong as arithmetic". Tentatively I have a suggestion: "expressing non-finiteness". So the statement would now be: (**) Let T be a consistent formal system that doesn't express finiteness, there's a formula of L(T), named say KONT(T), that's true but not provable in T. For example, the extension G' of the basic group theory G with the additional axiom A[x=y] would be a system that would express finiteness. Otoh, Q and PA would express non-finiteness. *** Now then we do have a trivial meta theorem about a general consistent T: (*') If T is a consistent formal system, then there's a formula of L(T) that if true in T is unprovable. I think it's debatable how close (*') is to (**) but seems to be in the right direction. Any suggestion so far though? -- ----------------------------------------------------------- Normally, we do not so much look at things as overlook them. Zen Quotes by Alan Watt -----------------------------------------------------------
From: Nam Nguyen on 9 Aug 2010 01:51
Nam Nguyen wrote: > Nam Nguyen wrote: >> >> The [secondary] intention is to go from there and find a replacement >> for CON(T) that doesn't depend on the notion of the natural numbers. >> (A very long shot though, imho). > > It still seems a long short but let me attempt. The meta statement > I think we'd like to make would be something like > > (*) Let T be a formal system satisfying certain "conditions", then > if T is consistent there is a formula of L(T), named say KONT(T), > that is true but not provable in T. > > Where "conditions" would be anything except "as strong as arithmetic". > Tentatively I have a suggestion: "expressing non-finiteness". So the > statement would now be: > > (**) Let T be a consistent formal system that doesn't express finiteness, > there's a formula of L(T), named say KONT(T), that's true but not > provable in T. > > For example, the extension G' of the basic group theory G with the > additional axiom A[x=y] would be a system that would express finiteness. > Otoh, Q and PA would express non-finiteness. After some reflections I'd like to alter the intended meta statement. The revised statement would now be: (*) If T is a formal system that expresses non-finiteness and that has a model M, then there's a formula of L(T), say KONT(T), that if true in M is not provable in T. Also, the following isn't a full (meta) proof and is only a take-it-at- own-risk sketch. But here it is: (a) We'd make use of Cantor theorem that there's no 1-1 mapping between U (of M) and P(U) [which is the Power set of U]. (b) We'd make use the fact that we could "re-define" L(T) so that there be more non-logical symbols available to us that L(T) might have. Would you think the revised (*), steps (a) and (b) are in the right direction? -- ----------------------------------------------------------- Normally, we do not so much look at things as overlook them. Zen Quotes by Alan Watt ----------------------------------------------------------- |