When you're reducing formulas, those are the same thing.
p 🡑 p ≡ ¬p
p 🡑 ¬p ≡ 1
¬1 ≡ 0
So then you're happy to say (p 🡑 (p 🡑 p)) 🡑 (p 🡑 (p 🡑 p)) ≡ (p 🡑 ¬p) 🡑 (p 🡑 ¬p)
≡ 1 🡑 1
≡ 0
The expression "(p 🡑 (p 🡑 p)) 🡑 (p 🡑 (p 🡑 p))" is just a particularly longwinded name for the constant "0".I don't see why you're comparing {NAND, FALSE} to {AND, NOT} - how do you produce TRUE from {AND, NOT} by a standard that {NAND} by itself doesn't also meet? The normal way to produce TRUE from {AND, NOT} is
NOT (p AND (NOT p))
but you seem to have already rejected that?My problem with p 🡑 ¬p ≡ 1 is simply that you need some (arbitrary) value p from somewhere. It’s not 1, it’s a unary function that returns 1. That just bothers me.
nand() = false
nand(x, ...) = !(x && !nand(...))
That eliminates the problem of needing arbitrary constants.
How do you know it's a unary function? For all you know, the function in question is f(p,q,r,s,t) = p 🡑 ¬p.
In fact it's a nullary function, because you don't need any input. There is no difference between the functions f(p,q,r,s,t) = p 🡑 ¬p and f(p,q,r,s,t) = r 🡑 ¬r. They have exactly the same behavior in every respect. And for the same reason, there is also no difference between those functions and the functions f(p) = p 🡑 ¬p, f(q) = p 🡑 ¬p [sic], and f() = p 🡑 ¬p.