tag:blogger.com,1999:blog-4987609114415205593.post6880465829895630969..comments2021-06-14T17:02:48.428+01:00Comments on M-Phi: On Adding a Validity Predicate to PAJeffrey Ketlandhttp://www.blogger.com/profile/01753975411670884721noreply@blogger.comBlogger18125tag:blogger.com,1999:blog-4987609114415205593.post-56353934055233790362020-11-22T09:49:10.572+00:002020-11-22T09:49:10.572+00:00hi I read your blog which is really great.Please v...hi I read your blog which is really great.Please visit on this site.<a href="https://support-nummerdeutschland.com/mcafee-support-deutschland.html" rel="nofollow">Bellen mcafee</a><br />mcafee-support +32-28081298https://www.blogger.com/profile/03051427917497908913noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-70192415201695893442020-11-10T12:01:04.943+00:002020-11-10T12:01:04.943+00:00Hi, Thank you for sharing such a good and valuable...Hi, Thank you for sharing such a good and valuable information,It is very important for me. Gmail is the worldwide used email service but sometimes user faces some problems in it. If you want to get some information about the Gmail then you can visit <a href="https://tekninenasiakaspalvelu.com/gmail-tukinumero-suomi.html" rel="nofollow">Gmail suomi yhteystiedot</a>.Gmail tuki suomihttps://www.blogger.com/profile/03332253924113399989noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-37222962535162174412020-11-09T11:05:44.156+00:002020-11-09T11:05:44.156+00:00Your blog is very informative and interesting to r...<br />Your blog is very informative and interesting to read, finally, I found exactly what I searching for. There are lots of users of Macfee antivirus in the world because of its features and easy interface. If you want to explore more interesting facts about Mcafee antivirus or want to resolve your technical issues then must visit <a href="https://contactklantenservicenederlands.com/bellen-mcafee-telefoonnummer.html" rel="nofollow">Mcafee ondersteuningsnummer</a>. Mcafee ondersteuninghttps://www.blogger.com/profile/02735746914133699950noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-50742343629272350732020-11-06T05:08:11.052+00:002020-11-06T05:08:11.052+00:00Hallo, mijn naam is Jaclyn Tibben. Ik woon in Amst...<br />Hallo, mijn naam is Jaclyn Tibben. Ik woon in Amsterdam, Nederland en heb mijn studie gevolgd aan de University of Technology Amsterdam. Ik ben technisch ingenieur bij de <a href="https://contactklantenservicenederlands.com/bellen-paypal-telefoonnummer.html" rel="nofollow">helpdesk Paypal</a>Paypal Nederlandhttps://www.blogger.com/profile/10441019087095996665noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-76082535125753941452011-04-07T20:41:20.604+01:002011-04-07T20:41:20.604+01:00Hi Julien,
"The upshot seems to be that the ...Hi Julien,<br /><br />"The upshot seems to be that the validity rules for 'valid' are not valid; yet, if we accept them, we may still want to say that they're valid in some sense."<br /><br />I think I'm with Sam. The weak validity rule (V-Intro) (which can be interpreted inside PA) is sound. But the stronger validity rule (V-Intro)* is not sound (it generates derivations of untruths from true assumptions). So, I don't think validity behaves analogously to truth. It's natural to desire of a truth theory something like: If A is true, then "A is true" is true, etc., etc. But it's not natural to require: if A is valid, then "A is valid" is valid.<br /><br />More generally, I think we have a consistent theory of validity with three ingredients<br />(a) the scheme (V-Out).<br />(b) the rule (V-Intro).<br />(c) the rule (V-Elim).<br /><br />The step I identify as problematic in the post concerning the Curry sentence is the one that uses the much stronger rule (V-Intro)*. Here's another example. Suppose B is one of the non-logical axioms of the validity theory V. Presumably, the inference from any *tautology* to B is not valid. Now, for any formula A,<br /><br />(i) V, A->A |- B<br /><br />So, using (V-Intro)*,<br /><br />(ii) V |- Val(A->A, B).<br /><br />But the inference from the tautology A->A to B isn't valid. So, it seems that the rule (V-Intro)* is not sound.<br /><br />Is there some notion of validity on which (V-Intro)*) might be sound? We have three basic explications of validity,<br /><br />(Modal) "A : B" is valid iff it's impossible for A to be true and B to be false.<br />(Semantic) "A : B" is valid iff any model of A is a model of B.<br />(Syntactic) "A : B" is valid iff B is derivable from A.<br /><br />In (Modal), the notion of possibility has to be logical, so that "1+1=2 : 2+2=4" counts as invalid. We could introduce modification (e.g., allow only standard 2nd-order models for (Semantic) or allow infinitely long derivations for (Syntactic).]<br /><br />But none of these notions seems to support the strong rule (V-Intro)*. The theorems we get in the theory of validity may be true, but they're not (usually) themselves valid.Jeffrey Ketlandhttps://www.blogger.com/profile/01753975411670884721noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-2096199693339081262011-04-07T12:04:18.847+01:002011-04-07T12:04:18.847+01:00Hey Julien,
I haven't thought too much about ...Hey Julien,<br /><br />I haven't thought too much about the need to treat both the truth and validity predicates in a non-hierarchical fashion (though my inclination is to treat them both as non-hierarchical). <br /><br />However, prima facie it's not clear to me that the theory with V-Out and Val-Intro is hierarchical. Indeed it includes all instances of V-Out, not just for those A, B which do not include the validity predicate, say. The same goes for Val-Intro.<br /><br />But you suggest a different route from V-Out/Val-Intro to some kind of hierarchy. I take it the idea is some kind of reflection principle for validity. Something like:<br /><br />(1) If we accept A, then we should accept Val(A).<br /><br />And, I think, unless 'valid' is to mean 'true', (1) cannot in general hold. For instance, I think there is /no/ sense of valid under which 'there is a chair in my room' is valid.<br /><br />What we need, it seems to me, is some notion of validity which, on the one hand, doesn't satisfy (1), and on the other, gives us that V-Out is not simply true but valid. I just can't see what would play this role.<br /><br />What do you think?<br /><br />Best,<br />SamSam Robertshttps://www.blogger.com/profile/07195370003468343442noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-10459158204081339592011-04-07T10:06:29.760+01:002011-04-07T10:06:29.760+01:00Thanks for the comments to you both!
Don't w...Thanks for the comments to you both! <br /><br />Don't we get a hierarchical theory of validity at this point? The upshot seems to be that the validity rules for 'valid' are not valid; yet, if we accept them, we may still want to say that they're valid in some sense. And so on.<br /><br />I wonder whether this way out of the problem sits well with the revisionary thought that truth isn't stratified - if validity and truth are both key semantic concepts, then arguably they should be treated in the same way etc.Julienhttps://www.blogger.com/profile/10145885350564771431noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-81461319857421227162011-04-06T19:42:02.728+01:002011-04-06T19:42:02.728+01:00Yes, all that sounds right - the theory you descri...Yes, all that sounds right - the theory you describe is a bit like closing PA under the (T-Intro) rule (and the (T-Elim) rule, if you like). So, if we weaken (V-Intro)* to your version (Val-Intro), we get a consistent theory, with an extension for Val(.,.) defined by the induction you give.<br />Right, I agree - the instances of the scheme (V-Out) shouldn't be regarded as valid themselves.<br />Thanks for the comments, Sam.Jeffrey Ketlandhttps://www.blogger.com/profile/01753975411670884721noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-48027960490115192842011-04-06T19:08:57.653+01:002011-04-06T19:08:57.653+01:00Sorry, (1) is not strictly true, of course. We don...Sorry, (1) is not strictly true, of course. We don't need the full T-schema to get in to trouble and neither do we need the full V-Out. <br /><br />SamSam Robertshttps://www.blogger.com/profile/07195370003468343442noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-89747881499898711392011-04-06T19:05:50.531+01:002011-04-06T19:05:50.531+01:00Hi Jeff,
I agree completely. I certainly don'...Hi Jeff,<br /><br />I agree completely. I certainly don't think that Val(A, A) is itself a logical truth. Whether it's valid in this context will depend on the notion of validity, of course, and it's not completely clear to me what notion Julien and JC have in mind. In any case, I'm also inclined to think that Val(A, A) isn't valid either.<br /><br />To be clear, the point of T was not to offer a genuine theory of validity, but to offer a slight weakening of Julien and JC's theory which was consistent. For me this raises one thought and one question:<br /><br />(1) The v-curry requires more than c-curry, in that in order to derive c-curry (in classical logic, say) we only need accept T(A) <--> A for all A, whereas for v-curry we need to accept not only V-Out but that V-Out is valid.<br /><br />(2) Given that some truths A are not valid, what reason have we to think that V-Out is? Any more than, say, set-theoretic replacement. <br /><br />Best,<br />SamSam Robertshttps://www.blogger.com/profile/07195370003468343442noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-267340515110371732011-04-06T18:45:15.430+01:002011-04-06T18:45:15.430+01:00Hi Sam, thanks - yes, I get it better now.
[Actu...Hi Sam, thanks - yes, I get it better now. <br /><br />[Actually, I should have said (V-Intro)* above - which is the fully self-applicative rule. This, with (V-Out), gives inconsistency. The weaker rule (V-Intro), on the other hand, is consistent.]<br /><br />Call your (Val-In) "(Val-Intro)" instead - as it's a rule not a scheme. So, your theory has (V-Out) and (Val-Intro).<br />There are three systems now:<br /><br />(i) (V-Out) plus (V-Intro) - this is consistent.<br />(ii) (V-Out) plus (V-Intro)* - this is inconsistent.<br />(iii) (V-Out) plus (Val-Intro) - this is consistent. <br /><br />(Val-Intro) is clearly a bit stronger than (V-Intro) as it allows the inference of Val(A,B) based on reasoning using the (Val-Intro) rule itself. It's basically a necessitation rule, analogous to having, from a derivation of A (in the modal logic), infer []A.<br /><br />"I do not allow V in the antecedent - there are principles of validity which are not themselves valid."<br /><br />Right - yes, that was my original point too. So, to infer Val(A,B), I required a derivation of B from A using only logic (and not the theory of validity itself). But your rule (Val-Intro) is a bit stronger than (V-Intro): it says that if there is a derivation of B from A using logic and applications of (Val-Intro), then infer Val(A,B). I think your consistency proof is correct for T. It allows iteration of the Val(.,.) predicate so long as the derivations only use the (Val-Intro) rule.<br /><br />However, your theory T counts certain things as valid that one might argue are not valid. For example, A is derivable from A in logic; so, T proves Val(A,A) using (Val-Intro). But because Val(A,A) is derivable from the empty set using logic and (Val-Intro), T proves Val(\emptyset, Val(A,A)).<br />So,<br /><br />T |- Val(\empyset, Val(A, A)).<br /><br />But is the inference from emptyset to Val(A,A) itself really valid? My inclination is to say that it is an inference licensed by a rule of the theory of validity, rather than a merely logical rule. So, the inference isn't valid.<br /><br />I would want to have things like Val(ValA,A), Val(A,A)). But should we want Val(\empyset, Val(A, A)) as a theorem?Jeffrey Ketlandhttps://www.blogger.com/profile/01753975411670884721noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-38020543036870659572011-04-06T16:00:38.364+01:002011-04-06T16:00:38.364+01:00Hi Jeff,
Sorry about the notation! I agree the Fr...Hi Jeff,<br /><br />Sorry about the notation! I agree the Friedman & Sheard convention is a useful one.<br /><br />I'm pretty sure that my Val-In is not the same as V-Intro. So, V is a theory of validity. Let's say that V is my theory T. In particular, it has as an axiom my Val-Out. So V-intro would give us the following instance:<br /><br />V |- Val-Out (for some A, B), then V |- Val(0, Val-Out)<br /><br />And, of course, I accept the antecedent. But I explicitly claim that Val-Out is not valid. So V-intro had better not be my Val-In!<br /><br />The difference is that I do not allow V in the antecedent - there are principles of validity which are not themselves valid.<br /><br />What do you think?<br /><br />Best,<br />SamSam Robertshttp://bbk.academia.edu/SamRobertsnoreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-37003890091707459382011-04-06T15:18:19.796+01:002011-04-06T15:18:19.796+01:00Thanks, Sam.
The principles you give are:
(Val-O...Thanks, Sam.<br /><br />The principles you give are:<br /><br />(Val-Out) A & Val(A, B) --> B<br /><br />(Val-In) A |- B<br />---------<br />|- Val(A, B) <br /><br />But aren't these just what I called the scheme (V-Out) and the rule (V-Intro)? If so, one gets the inconsistency as outlined above (and in Julien and JC's article).<br /><br />For (V-Out) is the scheme:<br /><br />Val(A, B) -> (A -> B)<br /><br />which is equivalent to your formulation:<br /><br />A & Val(A, B) -> B<br /><br />And your (Val-In) seems to be what I call (V-Intro) above. That is, an introduction rule saying that if B is derivable from A (possibly using other V-principles), then we can infer Val(A, B).<br /><br />[On the notation, I follow Friedman & Sheard and others in saying "in" and "out" for schemes, and "intro" and "elim" for rules. So, e.g., (T-In) is the scheme : A -> True("A"), while (T-Intro) is the rule that when you've derived A, you can infer True("A").]<br /><br />So, my question is: is your rule (Val-In) not the same as the rule (V-Intro) I mentioned above?Jeffrey Ketlandhttps://www.blogger.com/profile/01753975411670884721noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-60302421008030692462011-04-05T17:01:45.283+01:002011-04-05T17:01:45.283+01:00Hi,
For some reason, the post deleted lots of or...Hi, <br /><br />For some reason, the post deleted lots of ordered pairs in the proof I gave. So here it is again, this time using [A, B] for the ordered pair of A and B.<br /><br /><br />Proof: First we define an extension for Val(x, y) recursively in the following way:<br /><br />Val_0 = {[A, B] : A |-_c B} where |-_c is classical consequence.<br /><br />Val_n+1 = {[A, B] : A |-_Val_n B} where A |-_Val_n B just in case we can derive B from A classically using any Val(C, D) for [C, D] in Val_n as an extra premise. <br /><br />Then we take our deduction relation |-* to be the union of all the Val_n's. We also make the union of the Val_n's our extension of Val(x, y), which we add to N. Call the resulting model N*<br /><br />Now we want to show (1) that Val-In holds of |-*, (2) that Val-Out holds in N*, and (3) that if A |-* B, then if N* |= A, N* |= B.<br /><br />For (1), suppose that A |-* B. Then there is some Val_n which contains [A, B]. Given our definition of the Val_n's, [0, Val(A, B)] will be in Val_n+1, and thus |-* Val(A, B) as required.<br /><br />For (2), suppose that A and Val(A, B) are true in N* and B is not true in N*. Then there is a least n such that for some C, D, [C, D] is in Val_n, C is true in N*, and D is not. As [C, D] is in Val_n, there is a classical proof of D from C which might use Val(P, Q) for any [P, Q] in some Val_m where m < n. But, by hypothesis all such Val(P, Q) are true in N*, so as C is true in N*, so is D. Contradiction.<br /><br />For (3), any proof in |-* will be classical except for the possible use of Val(A, B) for [A, B] in some Val_n as extra premises. As all such [A, B] are in the extension of Val(x, y) in N*, the proofs will be effectively classical in N*. <br /><br />Best,<br />SamSam Robertshttp://bbk.academia.edu/SamRobertsnoreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-19989612899609236902011-04-05T16:50:28.687+01:002011-04-05T16:50:28.687+01:00Hi Jeff,
Julien suggested I post here with a few ...Hi Jeff,<br /><br />Julien suggested I post here with a few thoughts on this, to see what you think, if you get time.<br /><br />I take it the sticking point between your suggestion and Julien and JC's is that the notion of validity they use is broader that logical validity. In particular, their Valid-In rule will apply to derivations which might have used that very rule itself (or of course Valid-Out). <br /><br />One way around this is to say that Valid-In cannot properly be applied to derivations which include applications of Valid-In. But I think we can allow them this broader notion of validity and simply restrict Valid-Out to an axiom form.<br /><br />So, I propose the following theory T (which includes PA). We have an axiom:<br /><br />(Val-Out) A & Val(A, B) --> B<br /><br />for all A, B in the language of arithmetic plus the predicate Val(x, y). In addition we have a sequent rule:<br /> <br />(Val-In) A |- B<br /> ---------<br /> |- Val(A, B) <br /><br />where the derivation from A to B might have used applications of Val-In.<br /><br />Then I claim that there is a relation |-* which is closed under classical consequence and satisfies Val-In. Moreover I claim that there is an extension of the standard model of arithmetic N to include an extension for Val(x, y) which satisfies Val-Out and for which |-* is sound,<br /><br />Proof: First we define an extension for Val(x, y) recursively in the following way:<br /><br />Val_0 = { : A |-_c B} where |-_c is classical consequence.<br /><br />Val_n+1 = { : A |-_Val_n B} where A |-_Val_n B just in case we can derive B from A classically using any Val(C, D) for in Val_n as an extra premise. <br /><br />Then we take our deduction relation |-* to be the union of all the Val_n's. We also make the union of the Val_n's our extension of Val(x, y), which we add to N. Call the resulting model N*<br /><br />Now we want to show (1) that Val-In holds of |-*, (2) that Val-Out holds in N*, and (3) that if A |-* B, then if N* |= A, N* |= B.<br /><br />For (1), suppose that A |-* B. Then there is some Val_n which contains . Given our definition of the Val_n's, <0, Val(A, B)> will be in Val_n+1, and thus |-* Val(A, B) as required.<br /><br />For (2), suppose that A and Val(A, B) are true in N* and B is not true in N*. Then there is a least n such that for some C, D, is in Val_n, C is true in N*, and D is not. As is in Val_n, there is a classical proof of D from C which might use Val(P, Q) for any in some Val_m where m < n. But, by hypothesis all such Val(P, Q) are true in N*, so as C is true in N*, so is D. Contradiction.<br /><br />For (3), any proof in |-* will be classical except for the possible use of Val(A, B) for in some Val_n as extra premises. As all such are in the extension of Val(x, y) in N*, the proofs will be effectively classical in N*. <br /><br />It is open to Julien and JC to claim that Val-Out is inadequate in axiom form. In particular, they might claim that their notion of validity is such that Val-Out is itself valid, an thus can be used in proofs without stating it as an explicit assumption (much like we do with A --> (B --> A), say).<br /><br />But no matter how general their notion of validity is, it mustn't include all truths (otherwise it looks like we've just got another paradox of truth). That is, there must be truths A such that ~Val(0, A). Given that there are such, I don't see why we can't claim that Val-Out is one of them.<br /><br />Of course, just because Val-Out is about validity, doesn't means it should be valid itself. <br /><br />Best,<br />SamSam Robertsnoreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-61277422052977633352011-03-21T10:57:49.730+00:002011-03-21T10:57:49.730+00:00Hi Julien - I don't know Myhill's paper, s...Hi Julien - I don't know Myhill's paper, so yes, let's discuss that (I'm not in Munich this week though). Right, you and JC are treating validity as a broader notion than logical (e.g., first-order) implication. So, (V-Intro)* yields Val("A", "B") given a derivation of B from A in the theory of validity+arithmetic.Jeffrey Ketlandhttps://www.blogger.com/profile/01753975411670884721noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-5631387875910260762011-03-21T09:47:35.023+00:002011-03-21T09:47:35.023+00:00OK: 'what you suggest seems to point'OK: 'what you suggest seems to point'Julienhttps://www.blogger.com/profile/10145885350564771431noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-83301445612957033832011-03-21T09:46:42.841+00:002011-03-21T09:46:42.841+00:00Thanks much for these comments, Jeff. Indeed, the ...Thanks much for these comments, Jeff. Indeed, the validity paradox we discuss is closely related to the Montague-Kaplan-Myhill Paradox, or Paradox of the Knower, and absolute knowability (I talk about this and Myhill 1960 in a follow up to the paper with Jc I have recently drafted). <br /><br />Concerning the step from 5 to 6, I tend to take the validity predicate to express a broader notion of validity (although we don't really say as much in the paper). At any rate, what you suggests seem to point to a hierarchical approach to v-curry - one on which validity predicates are always added on the top of deductive systems, so to speak. I think I like this approach; this is very likely the way to go if we're classical logicians. Incidentally, Myhill's 'Levels of implication' (1975) may point in that direction, although I haven't had a chance to get a hold of this paper yet (I must read it, and it may be a good idea to discuss it at some point in our reading group!).Julienhttps://www.blogger.com/profile/10145885350564771431noreply@blogger.com