# Is this propositional formula an instance of an axiom?

Please help me automate my discrete mathematics homework. Given a valid propositional formula, check if it is an instance of one of Łukasiewicz's axioms. Here's how it works.

A term can be defined inductively as follows:

• Single lower-case letters of the Latin alphabet (a, b, c, etcetera) are terms.
• Given a term ϕ, ¬ϕ is also a term.
• Given terms ϕ and ψ, (ϕ→ψ) is also a term.

A formula is itself a term, usually made up of smaller terms. An example of a formula is (a→b)→¬(¬c→¬¬a).

Now, these are the three axioms. They are formula templates; some formulae are instances of an axiom. You make an instance by replacing all the variables (the Greek letters) with terms.

A: ϕ→(ψ→ϕ)
B: (ϕ→(ψ→χ))→((ϕ→ψ)→(ϕ→χ))
C: (¬ϕ→¬ψ)→(ψ→ϕ)


Same Greek letters have to be substituted with the same terms. Thus, one instance of the axiom A is (b→¬c)→(c→(b→¬c)). In this case ϕ has been substituted with (b→¬c), and ψ with c. Key to solving problems or making proofs in propositional logic is recognising when formulae are instances of axioms.

Note that all these axioms have their outer parens stripped away, which is common to do on the highest level. The strict way to write these is (ϕ→(ψ→ϕ)) ((ϕ→(ψ→χ))→((ϕ→ψ)→(ϕ→χ))) ((¬ϕ→¬ψ)→(ψ→ϕ)), with surrounding parens, but people usually leave those out when the meaning is clear so I'll leave it free how you choose to parse them.

The goal of the program is to take as input a valid formula in string or character array format, and output A, B or C (upper or lower case is fine) if it is an instance of the respective axiom, and do something else (output zero, output nothing, basically do anything except throwing an error) if it is not. The question is ; the shortest code wins!

### Test cases

input; output
(a→(a→a))→((a→a)→(a→a)); B
(a→(b→¬¬¬¬¬c))→((a→b)→(a→¬¬¬¬¬c)); B
(¬¬¬x→¬z)→(z→¬¬x); C
(¬(a→(b→¬c))→¬(c→c))→((c→c)→(a→(b→¬c))); C
(b→¬c)→(c→(b→¬c)); A
a→(b→c); 0


Alternatively, with surrounding parentheses:

input; output
((a→(a→a))→((a→a)→(a→a))); B
((a→(b→¬¬¬¬¬c))→((a→b)→(a→¬¬¬¬¬c))); B
((¬¬¬x→¬z)→(z→¬¬x)); C
((¬(a→(b→¬c))→¬(c→c))→((c→c)→(a→(b→¬c)))); C
((b→¬c)→(c→(b→¬c))); A
(a→(b→c)); 0


If you want to stick with printable ascii characters, you can use > for → and ! for ¬:

input; output
(a>(a>a))>((a>a)>(a>a)); B
(a>(b>!!!!!c))>((a>b)>(a>!!!!!c)); B
(!!!x>!z)>(z>!!x); C
(!(a>(b>!c))>!(c>c))>((c>c)>(a>(b>!c))); C
(b>!c)>(c>(b>!c)); A
a>(b>c); 0


Alternatively, with surrounding parentheses:

input; output
((a>(a>a))>((a>a)>(a>a))); B
((a>(b>!!!!!c))>((a>b)>(a>!!!!!c))); B
((!!!x>!z)>(z>!!x)); C
((!(a>(b>!c))>!(c>c))>((c>c)>(a>(b>!c)))); C
((b>!c)>(c>(b>!c))); A
(a>(b>c)); 0

• Given the rules as stated, how is e.g. a>(b>c) even a valid term? The rules, literally interpreted, say that every implication has to be enclosed in parentheses. Apr 14 at 17:14
• @DanielSchepler Good point xD Outer parentheses are typically left out but indeed, to be fully correct, they should be added. I will do so now. Apr 14 at 17:15
• @DanielSchepler on second thought; outer parentheses are not strictly necessary because a formula template doesn't have to be the same as a formula. I have also never seen that axiom with surrounding parentheses. So, so as to not invalidate the previous two answers; I am going to let it be open whether one uses parens there or not. Apr 14 at 20:12

# Curry (PAKCS), 175 bytes

n s='!':s
s%t='(':s++'>':t++")"
p[a]|a>''=1
p(n s)=p s
p(s%t)=p s*p t
f(a++'>':b%a)|p a==p b="A"
f(a%(b%c)++'>':(a%b)%(a%c))|p a*p b==p c="B"
f(n a%n b++'>':b%a)|p a==p b="C"


Try it online!

Takes input in ASCII characters. Returns nothing if it is not an axiom.

• That's cool; I don't often see declarative languages but it makes sense for this challenge of course Apr 14 at 10:23

# Pip, 99 83 bytes

(AZ'^.("9>,9>\1
,9>,9>9  >,,\1>\2 >,\1>\3
,!9>!9 >,\2>\1"R9C+XX^n). $NaTRpk@?:1)  Attempt This Online! ### Explanation A lightly compressed regex solution. First, we're going to modify the input a bit: aTRpk a Command-line argument TR Transliterate p from "()" k to ", "  Using ,  in place of () saves bytes on backslashes in the regexes. Next, we're going to construct a list containing the following three regexes for axioms A, B, and C respectively: ^(.+)>,.+>\1$
^            $The full string must match (.+) Match any run of characters (capture group 1) >, →( .+ Match any run of characters > → \1 Match group 1 again ␠ ) ^,(.+)>,(.+)>(.+) >,,\1>\2 >,\1>\3$
^                                    $The full string must match , ( (.+) Match any run of characters (capture group 1) >, →( (.+) Match any run of characters (capture group 2) > → (.+) Match any run of characters (capture group 3) ␠␠>,, ))→(( \1 Match group 1 again > → \2 Match group 2 again ␠>, )→( \1 Match group 1 again > → \3 Match group 3 again ␠␠ )) ^,!(.+)>!(.+) >,\2>\1$
^                     $The full string must match ,! (¬ (.+) Match any run of characters (capture group 1) >! →¬ (.+) Match any run of characters (capture group 2) ␠>, )→( \2 Match group 2 again > → \1 Match group 1 again ␠ )  We start with this string: "9>,9>\1 ,9>,9>9 >,,\1>\2 >,\1>\3 ,!9>!9 >,\2>\1"  Then: '^.("..."R9C+XX^n).$
"..."                The above string
R9              Replace each 9 with:
XX            Regex .
+              Apply + quantifier: .+
C               Wrap in capture group: (.+)
^n        Split the resulting string on newlines
'^.                      Concatenate "^" to the front
. $ Concatenate $ to the end, coercing the result to a regex


Now we use the N operator to count the number of matches of each of these regexes in the transliterated input. The result will be a list of 0's and 1's: [1 0 0] if the first regex matched, [0 1 0] if the second matched, [0 0 1] if the third matched, or [0 0 0] if none matched.

Finally:

(AZ...@?:1)
...       That three-element list
@?:    Find the index of the first occurrence of
1   1
(AZ       )  Use that number to index into the uppercase alphabet
If 1 is not found, returns nil, which results in no output

• It is surprising (but provable!) that the groups captured by those regexes must be valid terms. This relies on the fact that foo and (foo) cannot both be terms; otherwise, something like (a>(b>b))>(a) would be a false positive. Apr 14 at 21:02

# Python3, 450 bytes:

lambda t,y:next((b for a,b in t if all(c(a,p(y),{}))),0)
T=type
def p(s,c=0):
q,n=[],0
while s and(c==0 or s!=')'):
n+=(S:=s)=='!'
if S.isalpha():q+=[[n,S]];n=0
if S=='(':t,s=p(s[1:],1);q+=[(n,t)];n=0
s=s[1:]
return q,s
def c(a,b,d):
if T(a)!=T(b):return
for x,y in zip(a,b):
p,q=x;n,m=y
if(t:=T(x))==list:yield all([d.get(q,m)==m,not p or p%2==n%2]);d[q]=m
if t==tuple:yield all([T(y)==tuple,not p or p%2==n%2,*c(q,m,d)])


Try it online!

# Retina 0.8.2, 102 bytes

T(){}
{((.+)>{.+>\2}|(.+)>{(.+)>(.+)}}>{{\3>\4}>{\3>\5}|!(.+)>!(.+)}>{\7>\6)}$|.+$#2$*A$#4$*B$#6$*C  Try it online! Link includes test cases. Outputs nothing unless the input is one of the axioms. Explanation: Another regex-based answer. T(){}  Translate the ()s to {}s to avoid 14 \s. {((.+)>{.+>\2}|(.+)>{(.+)>(.+)}}>{{\3>\4}>{\3>\5}|!(.+)>!(.+)}>{\7>\6)}$|.+


Try to match one of the three axioms, but if there isn't an immediate match then just match everything.

$#2$*A$#4$*B$#6$*C


Output the corresponding letter if one of the capture groups in the relevant axiom exists. (Axiom A only has one capture group but for the others any representative capture group works.)

## PERL, 116114 bytes

#!/usr/bin/perl -p
y/()/XY/;s/^(.+)>X(.+)>\1Y$/A/;s/(X.+>)X(.+)>(.+YY)>X\1\2Y>\1\3$/B/;s/X!(.+)>!(.+)Y>X\2>\1Y/C/


This comes with a shebang line, so is suitable for a standalone executable script. If you are willing to execute it as perl -p scriptfilename, the shebang line can be dropped, or to execute as perl scriptfilename, the shebang line can be replaced with a final ;print`

The behaviour for the "not an axiom instance" case is to print the input with parentheses replaced by X and Y, respectively. This certainly counts as "do something else" because this output is guaranteed to be different from A, B, C (e.g., it is guaranteed to contain a lowercase letter)