Skip to main content
18 events
when toggle format what by license comment
Aug 6 at 3:12 comment added Frode Alfson Bjørdal @BrandenFitelson Did you find another single axiom which combines with the weaker rule?
S Mar 25, 2020 at 17:26 history suggested CommunityBot CC BY-SA 4.0
Reduced size of image
Mar 25, 2020 at 15:58 review Suggested edits
S Mar 25, 2020 at 17:26
Mar 22, 2020 at 19:48 comment added Frode Alfson Bjørdal @BrandenFitelson Thank you very much for this important information.
Mar 22, 2020 at 19:20 comment added Branden Fitelson or, in TPTP format: (1) fof(scharle1,axiom,![X]: t(s(X,s(X,X)))). (2) fof(scharle2,axiom,![X,Y,U,R]: t(s(s(X,s(Y,R)),s(s(s(U,Y),s(s(X,U),s(X,U))),s(s(U,Y),s(s(X,U),s(X,U))))))).
Mar 22, 2020 at 19:19 comment added Branden Fitelson Note: Scharle's two-basis contains a typo. Here is a sound and complete 2-axiom system, when combined with your weaker detachment rule (which Scharle calls D3): (1) DpDpp, (2) DDpDqrDDDsqDDpsDpsDDsqDDpsDps
Mar 22, 2020 at 17:11 comment added Branden Fitelson yes, i suspect there is a single axiom for the weaker rule. i'll be working on this now.
Mar 22, 2020 at 2:27 comment added Frode Alfson Bjørdal I accepted this answer because of the very useful literature reference in an edit. Scharle's article settles the question in the negative, but it does not exclude that there are other single axioms in the single connective $\uparrow$ for not both ,,, and ... which are adequate for classical propositional logic jointly with normal detachment as the only inference rule.
Mar 22, 2020 at 2:17 vote accept Frode Alfson Bjørdal
Mar 22, 2020 at 2:13 history edited Branden Fitelson CC BY-SA 4.0
added 318 characters in body
Mar 21, 2020 at 23:09 history edited Branden Fitelson CC BY-SA 4.0
added 290 characters in body
Mar 21, 2020 at 22:51 comment added Branden Fitelson note, also that Nicod's stronger rule also works with many other known axioms, including Lukaiewicz's. so, even if somehow this rule had worked with his axiom (in syntactically idiosyncratic way) it would still in this sense have been less generally useful than his stronger rule.
Mar 21, 2020 at 22:36 comment added Branden Fitelson Right, sorry, thanks Andreas. I have fixed this above. Now a 4-element model is required. Note that t(•) is the theorem-hood predicate, and c1 = 0 is the instance of s(s(X,X)X) that fails to be a theorem. i.e., t(s(s(0,0),0)) = 0.
Mar 21, 2020 at 22:34 history edited Branden Fitelson CC BY-SA 4.0
deleted 214 characters in body
Mar 21, 2020 at 22:08 comment added Andreas Blass As far as I can see, the Lukasiewicz axiom in the answer differs from the Nicod axiom in the question in that U replaces both $s$ and $t$. Does the Nicod axiom hold in your countermodel?
Mar 21, 2020 at 21:59 comment added Frode Alfson Bjørdal Welcome to Mathoverflow! I don't understand how the countermodel works, but maybe others can contribute?
Mar 21, 2020 at 21:50 review First posts
Mar 21, 2020 at 23:05
Mar 21, 2020 at 21:48 history answered Branden Fitelson CC BY-SA 4.0