3
$\begingroup$

In a base for propositional logic using the Polish connective $\uparrow$ for not both, J. Nicod isolated one axiom as sufficient:

$\uparrow\uparrow p\uparrow q r\uparrow\uparrow t\uparrow tt\uparrow\uparrow s q\uparrow\uparrow p s\uparrow ps$

J. Nicod used the somewhat odd inference rule $r$ if $\uparrow p\uparrow q r$ and $p$. May we use $\uparrow p\uparrow r r$ and $p$ instead of Nicod's rule, or is there some deeper reason for including $q$?

Improve this question
$\endgroup$
3
  • $\begingroup$ About the title: It seems to me that the rule "infer $r$ from $\uparrow p\uparrow rr$ and $p$" (i.e., in Nicod's rule replace $q$ with $r$ rather than with $p$) is intuitively closer to modus ponens than the rule you asked about. $\endgroup$
    – Andreas Blass
    Commented Mar 21, 2020 at 22:11
  • $\begingroup$ @AndreasBlass Thank you for identifying that typo. I will edit. $\endgroup$
    – Frode Alfson Bjørdal
    Commented Mar 21, 2020 at 22:22
  • $\begingroup$ You could really make the format of the second part readable form. $\endgroup$
    – Wlod AA
    Commented Mar 22, 2020 at 3:46

1 Answer 1

Reset to default
4
$\begingroup$

 enter image description here

This weakening of Nicod's inference rule is too weak. The 4-element counter-model above is one on which (a) your rule holds, (b) Nicod's single axioms holds, but (c) the formula s(s(X,X),X) fails to be a theorem (even though it is a classical theorem), where s(•,•) is the sheffer stroke.

Here is the code (3-lines of TPTP format) I used to find this model with mace4. 

fof(mpweak,axiom, ![X,Z]: ((t(s(X,s(Z,Z))) & t(X)) => t(Z))).

fof(nicod,axiom, ![X,Y,Z,U,V]: t(s(s(X,s(Y,Z)),s(s(V,s(V,V)),s(s(U,Y),s(s(X,U),s(X,U))))))).

fof(luka1,conjecture,![X]: t(s(s(X,X),X))).

For a discussion of alternative axiomatizations, I suggest the following article and the references therein.

https://projecteuclid.org/euclid.ndjfl/1093958259

Axiomatization of propositional calculus with Sheffer functors. Thomas W. Scharle Notre Dame J. Formal Logic Volume 6, Number 3 (1965), 209-217.

Improve this answer
$\endgroup$
10
  • $\begingroup$ Welcome to Mathoverflow! I don't understand how the countermodel works, but maybe others can contribute? $\endgroup$
    – Frode Alfson Bjørdal
    Commented Mar 21, 2020 at 21:59
  • 3
    $\begingroup$ 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? $\endgroup$
    – Andreas Blass
    Commented Mar 21, 2020 at 22:08
  • $\begingroup$ 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. $\endgroup$
    – Branden Fitelson
    Commented Mar 21, 2020 at 22:36
  • 1
    $\begingroup$ 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 $\endgroup$
    – Branden Fitelson
    Commented Mar 22, 2020 at 19:19
  • 1
    $\begingroup$ 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))))))). $\endgroup$
    – Branden Fitelson
    Commented Mar 22, 2020 at 19:20

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .