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 code-golf; 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
a>(b>c)
even a valid term? The rules, literally interpreted, say that every implication has to be enclosed in parentheses. \$\endgroup\$