Is a statement of propositional logic always true?

Question

The challenge is to golf a program that checks if a statement of propositional calculus/logic is a logical tautology (i.e. it is true for all possible values of the variables).

Input

Input formulas will use P, P', P'' ect. as variables. They can either be true or false.

(P and P') means both P and P' are true.

(P or P') means at least one of P and P' is true.

(P implies P') means that if P is true, than P' must be true.

(not P) means that P is false.

These forms can be nested.

Example input: (P implies ((P' or P'') and P'''))

Output

Output will be a truthy value if the input is a tautology, and a falsy value if it is not. (i.e True/False 1/0)

Test Cases

P: False

(P implies P): True

((P implies P') implies ((P' implies P'') implies (P implies P''))): True

(P implies (P or P')): True

(P implies (P and P')): False

(P or (not P)): True

and, or, not, and implies are the ONLY operators.

This is code-golf. Shortest program in bytes wins.

Clarification

The type of logic used here is Classical logic.

Answer 1

Retina 0.8.2, 136 124 121 bytes

{T`()`<>
.*P.*
<$& ¶ $&>
(?=(P'*))(?=.*\1[^P']*(¶|$))\1
$.2
¶
a
<not 1>|<0 or 0>|<1 [ai]\w* 0>|<0 a\w* .>|(<[^P<>]*>)
$#1

Try it online! Link includes test cases. Explanation: Works by considering each variable in turn, replacing the string f(p) with the string <f(1) and f(0)> for each variable p. The resulting string is then evaluated according to Boolean arithmetic.

{`

Repeat the entire program until the buffer stops changing.

T`()`<>

Change the ()s to something that doesn't need to be quoted.

.*P.*
<$& ¶ $&>

If the line still contains a variable, then duplicate it, and wrap the whole buffer in <>, however the two copies are still separated by a newline for now.

(?=(P'*))(?=.*\1[^P']*(¶|$))\1
$.2

Replace all copies of the last variable in the line with 1 or 0 depending on whether this is the original or duplicate line.

¶
a

Replace the newline with an a so that the two lines are joined together by an < and > operation.

<not 1>|<0 or 0>|<1 [ai]\w* 0>|<0 a\w* .>|(<[^P<>]*>)
$#1

Simplify any expressions that only contain constants. The expressions <not 1>, <0 or 0>, <1 implies 0>, <1 and 0>, <0 and 0>, <0 and 1> and <0 and P> (edge case) all evaluate to 0, while any other expression that contains no sub-expressions or variables evaluates to 1. (The original version of the code was buggy in this respect and needed a byte to fix it which I have included in the revised byte count in the header.)

Answer 2

Python 3, 128 bytes

lambda s:eval("all("+s.replace("implies","<=").replace(*"'_")+"".join(f" for P{'_'*i} in[0,1]"for i in range(s.count("P")))+")")

Try it online!

The operator names in the task definition are the same as in Python (except implies, which is replaceable by <=), but there is an extra annoyance due to the necessity to replace apostrophes with something else.

To enumerate all possible values of variables, we construct a multi-level list comprehension of the form <given expression> for P in[0,1] for P_ in[0,1]... and evaluate whether all values are True.

I haven't found a short way to determine the number of distinct variables (= the number of levels), so I'm just counting all instances of P (which is more than necessary, and thus does the job). In principle, we could even shorten this check to len(s), but this would lead to timeouts for longer expressions...

Answer 3

JavaScript (ES6),  129 ... 122  115 bytes

Saved 1 byte thanks to @Neil

Returns 0 or 1.

f=(s,n)=>eval(s.replace(m=/\w+'*/g,s=>(m|=l=s.length,{a:"&",i:"<=",n:"!",o:"|"})[s[0]]||n>>l-1&1))?n>>m||f(s,-~n):0

Try it online!

How?

We use /\w+'*/g to match all variables and operator names.

The operators and, not and or can be easily translated to &, ! and | respectively.

Translating implies is a little trickier. We know that \$A \Rightarrow B\$ is equivalent to \$\neg A \lor B\$. But inserting a leading ! would be quite difficult. Fortunately, this can also be expressed as \$(A \operatorname{xor} 1)\lor B\$. Given the precedence of JS operators, no parentheses are needed. So, implies  is  could be translated to ^1|.

Edit: Better yet, as noticed by @Neil, implies can also be translated to <=, which is 1 byte shorter.

Variables are replaced by either \$0\$ or \$1\$ depending on their size and the current value of the counter \$n\$.

Once everything has been replaced in the original expression, we test whether it eval()uates to \$1\$.

We keep track in \$m\$ of all lengths of the matched strings OR'ed together. This value is greater than or equal to the length of the longest string and a fortiori of the longest variable name. We use it to make sure that all possible combinations are tried at least once.

Commented

f = (s, n) =>             // s = input string, n = counter
  eval(                   // evaluate as JS code:
    s.replace(            //   replace in s:
      m = /\w+'*/g,       //     all operator and variable names
      s =>                //     s = matched string
        (                 //
          m |=            //     do a bitwise OR between m and ...
            l = s.length, //       ... the length l of the matched string
          {               //     lookup object:
            a: "&",       //       "and"     -> "&"
            i: "<=",      //       "implies" -> "<="
            n: "!",       //       "not"     -> "!"
            o: "|"        //       "or"      -> "|"
          }               //
        )[s[0]] ||        //     translate the operator name according to
                          //     its first letter
        n >> l - 1 & 1    //     or replace the variable name with 0 or 1
    )                     //   end of replace()
  ) ?                     // end of eval(); if truthy:
    n >> m ||             //   stop if n is equal to 2 ** m (success)
    f(s, -~n)             //   otherwise, do a recursive call with n + 1
  :                       // else:
    0                     //   failure: return 0

Answer 4

05AB1E (legacy), 45 bytes

„€Ÿ(ì'''_:'Ø¢„<=:D'P¢ƒ1Ý'_Nד €‡ Pÿ€†ÿ“}')J.Eb

Port of @KirillL.'s Python answer, so make sure to upvote him!

Outputs 1/0 respectively. If outputting True/False is allowed (even though these are both falsey in 05AB1E), the trailing b could be omitted.

Uses the legacy version of 05AB1E, where list [0,1] will be input as string with ÿ, whereas this would result in an error in the new version of 05AB1E.

Try it online or verify all test cases.

Explanation:

„€Ÿ(              # Push dictionary string "all("
    ì             # Prepend it in front of the (implicit) input-string
'' '_:           '# Replace all "'" with "_"
'Ø¢ „<=:         '# Replace dictionary string "implies" with "<="
D                 # Duplicate the string
 'P¢             '# Pop and count the amount of "P" in this string
    ƒ             # Loop `N` in the range [0, count]:
     1Ý           #  Push list [0,1]
     '_N×        '#  Push a string consisting of `N` amount of "_"
     “ €‡ Pÿ€†ÿ“  #  Push dictionary string " for Pÿ inÿ",
                  #  where the first `ÿ` is automatically replaced with the "_"-string
                  #  and the second the stringified "[0,1]" list
    }')          '# After the loop: push a ")"
J                 # Join all strings on the stack together
 .E               # Execute it as Python code
   b              # Then convert the "True"/"False" to 1/0 with the binary builtin
                  # (after which the result is output implicitly)

See this 05AB1E tip of mine (section How to use the dictionary?) to understand why „€Ÿ( is "all("; 'Ø¢ is "implies"; and “ €‡ Pÿ€†ÿ“ is " for Pÿ inÿ".

Answer 5

SageMath, ^{140 134} 132 bytes

lambda p:propcalc.formula(r(*"'0",r("implies","->",r("or","|",r("and","&",r("not","~",p)))))).is_tautology()
from re import sub as r

Try it online!

Answer 6

J, ¹¹⁴102 bytes

[:*/([:;e.&' ()'({.;(<./@i.~&'rapt'{ ::''+`*`<:,'1-';'&{',~&":1-~#)@}.);.1]),/&.":"#.2#:@i.@^1#.e.&'P'

Try it online!

How it works

2|:@#:@i.@^1#.e.&'P'

Count the P's in the string, 2^y, range, and base 2 it. This is a matrix with all boolean combinations for P variables. Now transforming the string to a J expression:

e.&' ()'

Bit mask if () is at that position.

(…);.1]

Split the string based on the bit masks first item (which will be 1 expect in the single P case.) The groups start whenever the bit mask is 1, i.e. we either have the single groups ,(,) or a group that starts with that and also has a word like (P'''

{.;(…)@}.

Take the first character of the group unmodified, and for the rest apply:

'&{',~&":1-~#

Length - 1 as string prepended with &{, e.g. 3&{ for P'''.

+`*`<:,'1-';

The operators: or, and, implies, not. Now we have a list of things we have to pick from.

<./@i.~&'rapt'{ ::''

Search for any of rapt (or, and, implicit, not) with the implicit P at the 5th place), reduce the word to that index, and take from the list (with an empty string if the group was only one character long.) We now have a list of valid J expressions like (0&{ <: (2&{ + 1&{)).

,/&.":"1

With the function on the left side and the booleans on the right side: Convert from numbers to strings with ": (this will only change the booleans), append them to the function, and with &. the inverse of ": will be called afterwards, so (0&{ <: (2&{ + 1&{)) 0 1 will then be called and converted to the integer 1.

[:*/

Multiply-reduce the results.

Answer 7

R, 230 197 191 bytes

f=function(s,`[`=gsub)`if`(grepl("P",s<-sapply(0:1,`[`,pa="Q","and"["&","or"["|","not"["!","implies"["<=","P([^'])|P$"["Q\\1",s]]]]])),all(sapply("P'"["P",s],f)),all(sapply(parse(t=s),eval)))

Try it online!

Edits: -39 bytes in exchange for quite a lot of warnings

This was a lot of fun, but I must confess that I needed to look at the other answers for inspiration about how to handle 'implies'...

Works by recursively substituting each P (without any apostrophes) for 1 and 0, then reducing the number of apostrophes after all the remaining Ps and calling itself, until there are no more Ps left, at which point it evaluates each expression.

My pattern matching & substitution is rather clunky, so I suspect that this could still be reduced quite a lot.

Commented version:

is_tautology=f=function(string) {
    string=                         # exchange in string:
    gsub("and","&",                 # and -> &
    gsub("or","|",                  # or -> |
    gsub("not","!",                 # not -> !
    gsub("implies","<=",            # implies -> <=
    gsub("P([^'])","Q\\1",
    gsub("P$","Q",                  # P (but not P') -> Q
    string))))))                            
                                    # now exchange Q for 1 or for 0:
    string=sapply(0:1,gsub,pattern="Q",string)      
    if(!any(grepl("P",string))){    # if there are no more P's left:
                                    # return true if expression evaluates true
                                    # in both cases (Q->1 and Q->2)
        return(eval(parse(text=string[1]))&&eval(parse(text=string[2])))
    } else {                        # otherwise (there are still some P's):
        string=g("P'","P",string)   # remove one apostrophe from each P'
                                    # and recursively call self 
                                    # with both cases (Q->1 and Q->2)
        return(f(string[1])&&f(string[2]))
    }
}

Answer 8

Wolfram Language (Mathematica), 10 bytes

TautologyQ

Yep, there's a builtin.... Now, the OP will have to decide if the input format is acceptable (I feel that it is well within the spirit of this site's guidelines).

In terms of the variables themselves, we need to use strings of letters in place of P, P', P'', and so on: we can use P, Pp, Ppp, and so on (as has been done in the TIO link), or a, b, c, foo, bar, or whatever. (Strangely, TautologyQ seems to be ok with a single variable containing primes, but two different such variables seems to break it.)

Logical input can be taken in two different formats. We can preserve the infix notation in the examples, such as:

TautologyQ[(P \[Implies] (P \[And] Pp))]

Or we can use prefix notation, such as:

TautologyQ[Implies[P, And[P, Pp]]]

(If the input format is completely inflexible, then one can add some processing commands like StringReplace followed by ToExpression.)

Try it online!