Implement logical axioms

[ed963]

For each of the logical axioms, implement a function that takes a Formula as input and returns whether it is an instance of the axiom.

• (E1) - Reflexivity: $x = x$ for each variable $x$
• (E2) - Substitution for functions: $[(x_1=y_1)\wedge(x_2=y_2)\wedge\dots\wedge(x_n=y_n)]\rightarrow(f(x_1,x_2,\dots,x_n)=f(y_1,y_2,\dots,y_n))$
• (E3) - Substitution for relations: $[(x_1=y_1)\wedge(x_2=y_2)\wedge\dots\wedge(x_n=y_n)]\rightarrow(R(x_1,x_2,\dots,x_n)\rightarrow R(y_1,y_2,\dots,y_n))$
• (Q1) - Universal instantiation: $(\forall x\phi)\rightarrow\phi^x_t$, if $t$ is substitutable for $x$ in $\phi$
• (Q2) - Existential generalization: $\phi^x_t\rightarrow(\exists x\phi)$, if $t$ is substitutable for $x$ in $\phi$

[ed963]

f28b0dc implements functions that create Formula instances of logical axioms.

TBD: Whether it's worth to implement functions to decide whether a Formula is a logical axiom.

[ed963]

dcd45a3