# Is IMPLY enough for this function? [closed]

Given a boolean function with inputs, check if it's possible to only use IMPLY gate to express it.

There's no extra limitation on how you use this gate, and you can use each input for any amount of times. See examples below:

$$\\begin{matrix} \text{Expression}&&&&&\text{Solution}&\text{Your output}\\ a&0&0&1&1&a&\text{true}\\ b&0&1&0&1&b&\text{true}\\ a\vee b&0&1&1&1&\left(a\rightarrow b\right)\rightarrow b&\text{true}\\ \neg a&1&1&0&0&-&\text{false}\\ a\wedge b&0&0&0&1&-&\text{false}\\ 1&1&1&1&1&a\rightarrow a&\text{true} \end{matrix}\$$

This actually checks if there is one input that make the output of function true as long as it's true. Proof is left as an exercise.

Input can be taken as a function, a boolean array of length $$\2^n\$$, or any convenient format. Shortest code wins.

• What format should people take the input in? Jul 2, 2021 at 1:27
• Can you spell out what the 4 numbers correspond to? Also in the first example how is the single value a supposed to be implemented by imply? I’m probably missing something obvious but I’m still not getting it Jul 2, 2021 at 3:20
• @Jonah The four numbers are the evaluation of the expression for the four possible inputs ab: 00, 01, 10, 11, in that order. The single value solutions seem to mean that we are taking the vacuous truth that if the logical expression can be implemented with no gates then it can be implemented with only imply gates. These do seem like they should be in the question body, though. Jul 2, 2021 at 4:42
• What is IMPLY gate? You need to include that in the challenge rather than relying on an external link. Jul 2, 2021 at 15:09
• @l4m2 Fwiw, I thought this was a very interesting challenge (once I understood it), and I think it's worth making it more clear to re-open it. Jul 2, 2021 at 22:56

# Jelly, 9 8 bytes

oJ’|/‘nL


Try it online!

-1 because it came to me in a dream... to use >, which would not have worked at all, but it still got me thinking

Same input format as hyper-neutrino's solution and also uses OP's spoiler.

oJ          Replace each 0 in the input with its index in the input,
‘         then decrement each.
oJ‘         We now have every bitmask which yields false, and some extra zeroes.
|/       Reduce by bitwise OR.
‘      Incremented,
nL    is it not equal to the length?


The bitwise OR of the false bitmasks is 1 less than the length (the length being a power of 2) iff each input variable can produce false while being true.

A rough proof of the spoiler:

It is necessary for the function to be implied by a variable:
An expression composed of just implications is either a variable or the implication of two such expressions. In butchered BNF: $$\text{} \text{ ::= } \text{} \text{ | } \text{} \rightarrow \text{}$$ Clearly, any expression consisting of a lone variable is true precisely when that variable is true.
An implication $$\a \rightarrow b\$$, furthermore, is true at least when $$\b\$$ is true, for any expression $$\b\$$. If $$\b\$$ satisfies the property that some variable implies it, so does $$\a \rightarrow b\$$. Therefore this is true of any implication of variables, any implication of implications of variables, and so on.

It is sufficient for the function to be implied by a variable:
There is no function satisfying the condition which cannot be expressed only in implicatures. Let's call the variable which implies the function $$\a\$$. If we look only at the cases in which $$\¬a\$$, $$\¬b\$$ can be written $$\b \rightarrow a\$$. From there, considering that $$x \vee y \iff (x \rightarrow y) \rightarrow y$$ we have $$x \wedge y \iff ¬(¬x \vee ¬y) \iff (((x \rightarrow a) \rightarrow (y \rightarrow a)) \rightarrow (y \rightarrow a)) \rightarrow a$$ hence any function can be expressed in nothing but implicatures presupposing a known false variable, and such an expression without the presupposition is the disjunction of any function and an additional variable.

• For me it's the other way around - I worked out that the second spoiler implies that any variable implying the function implied that the function can be written as a combination of implications, but I don't see how the reverse is true yet.
– Neil
Jul 2, 2021 at 15:30
• @Neil Edited to explain more fully (I hope) Jul 2, 2021 at 16:30
• Ah yes, it was the fact that (a->b)->(a->(c->b)) that I was missing.
– Neil
Jul 2, 2021 at 16:55
• Writing $x∧y$ as $x→\left(y→⊥\right)$ may be more direct, though
– l4m2
Jul 3, 2021 at 1:52

# Jelly, 11 bytes

;2/ƬḊm2ȦƊ€Ẹ


Try it online!

-2 bytes thanks to Unrelated String

Still looking to shorten this with a more intelligent way of applying OP's spoiler. Accepts input as a length $$\2^n\$$ list in the order of [0, 0, 0], [0, 0, 1], [0, 1, 0], [0, 1, 1], [1, 0, 0], [1, 0, 1], [1, 1, 0], [1, 1, 1] (standard bit mask enumeration). Working on a proof first though.

• s2F€\$ -> ;2/? Jul 2, 2021 at 2:05
• @UnrelatedString Oh yeah good catch, I've never really used n-wise reduce much. Thanks. Jul 2, 2021 at 2:08

# Charcoal, 14 bytes

⊙↨⊖Ｌθ²⌊Φθ＆μＸ²κ


Try it online! Link is to verbose version of code. Takes input as a binary array of length 2ⁿ and outputs a Charcoal boolean, i.e. - for implied, nothing if not. Explanation:

    θ           Input array
Ｌ            Length
⊖             Decremented
↨   ²          Convert to base 2
⊙               Does any bit satisfy
θ       Input array
Φ        Filtered where
μ     Inner index
＆      Bitwise And
Ｘ²   2 raised to power
κ  Outer index
⌊         Does not contain zero


# Japt, 11 bytes

Port of Unrelated String's solution 'cause I genuinely don't have the first clue what the challenge is asking us to do.

ÊÉ¦UËÉ©EÃr|

ÊÉ¦UËÉ©EÃr|     :Implicit input of array U
Ê               :Length
É              :Subtract 1
¦             :Not equal to
UË           :Map each element in U at 0-based index E
É          :  Subtract 1
©E        :  Logical AND with E
Ã       :End map
r|     :Reduce by bitwise OR