Automated Reasoning in Higher Order Logic

Automated Reasoning in Higher Order Logic

Math Gate

Scunak

Javascript Interactive Higher-Order Theorem Prover

Simptcheck: Simple Proof Term Checker in OCaml

I claim there is a minor error in the 1958 paper Dualität by Ernst Specker and that I have a fix. I am working from Thomas Forster's translation from Specker's original German version. The issue is minor and does not affect the results of the paper.

The Claim

Specker claims (see page 6 of Forster's translation) that given formulas S1 and S2 he can find a formula T such that the conjunction of equivalences (S1 ↔ S1') ∧ (S2 ↔ S2') is equivalent to the single equivalence T ↔ T'. Here a prime indicates taking the dual of the formula (where 'dual' depends on the language under consideration). I believe the claim is true, but do not believe Specker's proof.

Before reading the rest, any guess how to define a T from S1 and S2 (and their duals) so that the equivalence holds? You can try to interactively solve this problem in JITPRO by clicking here:

The Error

Specker chooses T to be
(S1 ↔ S1' ∧ S2 ∧ ¬S2') ∨ (S2 ↔ S2' ∧ ¬S1 ∧ S1') ∨ (¬S1 ∧ S1' ∧ S2 ∧ ¬S2')

Minor Point: Specker then says that T' is obtained from T by swapping the indices 1 and 2. Clearly T' (as the dual of T) is not obtained in this way. Instead T' is obtained from T by priming unprimed occurrences of Si and unpriming primed occurrences of Si. (In fact one can check that if T' were the same as T up to swapping the indices, then no choice of T could work.)

The question now is whether or not (S1 ↔ S1') ∧ (S2 ↔ S2') and T ↔ T' are provably equivalent. Unfortunately, it is not clear whether ↔ should bind more tightly than ∧ or not. So T could be either
((S1 ↔ S1') ∧ S2 ∧ ¬S2') ∨ ((S2 ↔ S2') ∧ ¬S1 ∧ S1') ∨ (¬S1 ∧ S1' ∧ S2 ∧ ¬S2')
or
(S1 ↔ (S1' ∧ S2 ∧ ¬S2')) ∨ (S2 ↔ (S2' ∧ ¬S1 ∧ S1')) ∨ (¬S1 ∧ S1' ∧ S2 ∧ ¬S2').
We consider both possibilities and show neither works.

Assume T is
((S1 ↔ S1') ∧ S2 ∧ ¬S2') ∨ ((S2 ↔ S2') ∧ ¬S1 ∧ S1') ∨ (¬S1 ∧ S1' ∧ S2 ∧ ¬S2')
so that T' is
((S1' ↔ S1) ∧ S2' ∧ ¬S2) ∨ ((S2' ↔ S2) ∧ ¬S1' ∧ S1) ∨ (¬S1' ∧ S1 ∧ S2' ∧ ¬S2).
Suppose we have formulas S1 and S2 and a model in which S1 and S2 are false but the duals S1' and S2' are true. In this case, the conjunction
(S1 ↔ S1') ∧ (S2 ↔ S2') is false (both conjuncts are false).
On the other hand, both T and T' are false, hence T ↔ T' is true.

Click here to prove in JITPRO that this counterexample works:

Next assume T is
(S1 ↔ (S1' ∧ S2 ∧ ¬S2')) ∨ (S2 ↔ (S2' ∧ ¬S1 ∧ S1')) ∨ (¬S1 ∧ S1' ∧ S2 ∧ ¬S2')
so that T' is
(S1' ↔ (S1 ∧ S2' ∧ ¬S2)) ∨ (S2' ↔ (S2 ∧ ¬S1' ∧ S1)) ∨ (¬S1' ∧ S1 ∧ S2' ∧ ¬S2).
Suppose we have formulas S1 and S2 and a model in which S1, S1' and S2 are false but S2' is true. In this case, the conjunction
(S1 ↔ S1') ∧ (S2 ↔ S2') is false (the second conjunct is false).
On the other hand, both T and T' are true, hence T ↔ T' is true.

Click here to prove in JITPRO that this counterexample works:

The Fix

My candidate for T is (¬S1' ∧ S2) ∨ (S1' ∧ ¬S2').
In this case T' is (¬S1 ∧ S2') ∨ (S1 ∧ ¬S2).

Before reading the proof, you can try to prove this choice of T works in JITPRO by clicking here:

Proof:

If (S1 ↔ S1') ∧ (S2 ↔ S2'), then T ↔ T' since T and T' are the same up to the primes.

Assume T ↔ T'. That is,
((¬S1' ∧ S2) ∨ (S1' ∧ ¬S2')) &equiv ((¬S1 ∧ S2') ∨ (S1 ∧ ¬S2)).
We must prove (S1 ↔ S1') and (S2 ↔ S2'). We consider two cases.

Case 1: Suppose T and T' are both true. There are four possiblities.

Case 1a: Suppose ¬S1' ∧ S2 and ¬S1 ∧ S2'. The equivalences hold in this case.

Case 1b: Suppose ¬S1' ∧ S2 and S1 ∧ ¬S2. This is impossible.

Case 1c: Suppose S1' ∧ ¬S2' and ¬S1 ∧ S2'. This is impossible.

Case 1d: Suppose S1' ∧ ¬S2' and S1 ∧ ¬S2. The equivalences hold in this case.

Case 2: Suppose T and T' are both false. In this case we have
((S1' ∨ ¬S2) ∧ (¬S1' ∨ S2'))
and
((S1 ∨ ¬S2') ∧ (¬S1 ∨ S2)).
From this we can conclude four disjunctions by resolution:
(¬S2 ∨ S2'),
(¬S2' ∨ S2),
(S1' ∨ ¬S1) and
(S1 ∨ ¬S1').
The two equivalences clearly follow.