Javascript Interactive Higher-Order Theorem Prover
Automated Reasoning in Higher Order Logic
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.