KeizerHarm
• 971
• 6
• 18

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 axiom A isthese 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 read that oneparse them.

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


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

KeizerHarm
• 971
• 6
• 18

ThusNote that the strict way to write axiom A 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 read that one.

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!

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


Alternatively:

((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
(b>!c)>(c>(b>!c)); A
(a>(a>a))>((a>a)>(a>a)); B
(a>(b>!!!!!c))>((a>b)>(a>!!!!!c)); B
(!!!x>!z)>(z>!!x); C
(a>(b>c)); 0
(!(a>(b>!c))>!(c>c))>((c>c)>(a>(b>!c))); C
(b>!c)>(c>(b>!c)); A
a>(b>c); 0


Alternatively:

((b>!c)>(c>(b>!c))); A
(a>(b>c)); 0

KeizerHarm
• 971
• 6
• 18

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.

Thus, 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
(b→¬c)→(c→(b→¬c)); A
(a→(a→a))→((a→a)→(a→a)); B
(a→(b→¬¬¬¬¬c))→((a→b)→(a→¬¬¬¬¬c)); B
(¬¬¬x→¬z)→(z→¬¬x); C
(a→(b→c)); 0
(¬(a→(b→¬c))→¬(c→c))→((c→c)→(a→(b→¬c))); C


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

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

Became Hot Network Question
edited tags