[thaumasiotes]

> { NAND } is considered functionally complete, even though it can only produce a function that maps any input x to TRUE, and can't produce the value TRUE itself.

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?

[codeflo]

Yeah, listing {AND, NOT} was a mistake — you’re right, you do need a constant.

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.

[thaumasiotes]

> It’s not 1, it’s a unary function that returns 1.

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.

[deadbeeves]

When I'm aiming for elegance, I like to define NAND as an N-ary function:

nand() = false

nand(x, ...) = !(x && !nand(...))

That eliminates the problem of needing arbitrary constants.