Is there a way to prove that the absurdity axiom is consistent?

Question

I'm currently looking for a way to prove that the Reductio ad absurdum axiom of classical logic is consistent. That's what i've done :

You want to prove $A\implies B$

Your suppose $\neg(A\implies B)$

You replace $(A\implies B)$ by it's equivalent $\neg (A) \vee B$, it gives you : $\neg(\neg(A) \vee B)$, i can apply De Morgan law, which gives : $A \wedge \neg(B)$ From that assertion i found a contradiction (something always false) $(A \wedge \neg(B))\implies \perp$

I replace the implies by it's equivalent form $\neg(A \wedge \neg(B)) \vee \perp$

$\perp$ is neutral for $\vee$, then, it's equivalent to $\neg(A \wedge \neg(B))$

Now i can apply de Mogan law $\neg (A) \vee B$ And i can replace $\neg(A) \vee B$ by it's equivalent form with implication : $A\implies B$

So, is it a valid view of the Reductio ad absurdum axiom ?

Answer 1

Can you state that axiom as a well-formed formula (there's not necessarily just one axiom)? Because, if you do, it probably ends up an easy matter to point out that the antecedent of the absurdity axiom can't unify with the axiom itself due to symbol clash. Consequently, the only consequences of the absurdity axiom under detachment are it's substitution instances. But, the rule of substitution is truth-preserving. So, since the absurdity axiom is a tautology, all of it's consequences are tautologies also. Therefore, the absurdity axiom is consistent.

But, you do have to show that symbol clash would occur or that no unification between the antecedent of the absurdity axiom and the absurdity axiom itself comes as possible.

Or did you mean that the axiom is consistent with some other axioms/rules of inference?

Edit: Suppose the absurdity axiom in Polish notation would get re-written, with - marks used informally to mark the antecedent, as C-CNpq-CCNpNqp.

Now, let's look at 1. CNab and 2. CCNpqCCNpNqp. The first symbol of both is C, so unification might be possible so far. The second symbol of CNab is N, and the second symbol of CCNpqCCNpNqp is C. Thus, we have symbol clash, and there is no way to unify 2. with itself. Consequently, nothing can get derived from 2. by detachment. Only substitution instances can get derived, and since the rule of substitution preserves truth, and 2. is tautology, only tautologies can get derived. Denote any member from the family of tautologies as $\tau$. N$\tau$ is not a tautology, and thus not derivable. Thus, for no formula derivable from 2. does $\vdash$$\tau$ and $\vdash$N$\tau$ hold.

Suppose the absurdity axiom, with 0 denoting falsity, has form CCCp0qCCCp0Cq0p and no definitions come as permissible. Consider 1. CCa0b and 2. CCCp0qCCCp0Cq0p. Let $\alpha$/$\beta$ denote substituting $\alpha$ with $\beta$. So, in 1. and 2. let a/Cp0, q/0, b/CCCp0C00p. Thus, they do have a most general unifier. So, we'll draw out the consequences of the absurdity axiom as follows.

The absurdity axiom    1 CCCp0qCCCp0Cq0p
1 q/0                  2 CCCp00CCCp0C00p
1 p/Cp0 q/CCCp0C00p    3 CCCCp00CCCp0C00pCCCCp00CCCCp0C00p0Cp0
3 * C2-4               4 CCCCp00CCCCp0C00p0Cp0

Now there exist only two possibilities for detachable well-formed formulas. Either 1 or a substitution instance of it gets used as the major premiss, or 4 or a substitution instance of it gets used as the major premiss. We've already found the most general unifier of the antecedent of 1 above. So, does the antecedent of 1 unify with 4, does the antecedent of 4 unify with 1, or does 4 unify with itself?

Considering the antecedent of 1 with 4, consider CCa0b and 4. We can substitute a with CCp00, and we're alright. But, now CCa0b becomes 1' CCCCp000b. 4 and 1' match up to their eighth symbol. The eighth symbol of 1' is 0. The eighth symbol of 4 is C. Thus, we have symbol clash, and nothing can get inferred from some variant of 1 as the major premiss and 4 as the minor premiss.

Considering the antecedent of 4 with 1, consider CCCa00CCCCa0C00a0 and CCCp0qCCCp0Cq0p. We substitute a/p and q/0 yielding 4' CCCp00CCCCp0C00p0 and 1' CCCp00CCCp0C00p. But, now the 10th symbol of 4' is C and the 10th symbol of 1' is p. The 10th through 12th symbols of 4' is Cp0. Thus, the smallest substitution for p in 1' would be Cp0. But, then we have p substituted with some well-formed formula which has p in it also. So, to unify p with Cp0 would require another substitution. But any such substitution also has p in it. So, we would require another substitution with p in it ad infinitum. This is the occurs check. Thus, the antecedent of 4 does not unify with 1. Consequently, nothing can get detached with some variant of 4 as the major premiss and 1 as the minor premiss.

Lastly, let's consider 4-1 CCCCp00CCCCp0C00p0Cp0 and 4-2 CCCa00CCCCa0C00a0. We'll substitute a/Cp0 yielding 4-3 CCCCp00CCCCCp00C00Cp00. Now the first spot where 4-1 and 4-3 differ consists of their 12th symbol. The smallest substitution would consist of substituting p with Cp0. But, now the occurs check happens (which leads to a non-terminating recursive blow-up as suggested in the previous case). Consequently, the antecedent of 4 does not unify with itself.

Since above cases qualify as exhaustive, the only theorems starting from 1 obtainable under detachment is 4 or one of it's substitution instances. Now, both 1 and 4 are tautologies and so are any of their substitution instances. Thus, from the absurdity axiom 1 we can only obtain tautologies and consequently no negation of tautology can get derived. Therefore, this absurdity axiom is (self) consistent under detachment.