Automated Reasoning in Higher Order Logic | I claim there is a minor error in the
1958 paper ## The ClaimSpecker claims (see page 6 of Forster's translation)
that given formulas S
he can find a formula _{2}T such that the conjunction of equivalences
(S
is equivalent to the single equivalence
_{1} ↔ S_{1}') ∧ (S_{2} ↔ S_{2}')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 S (and their duals)
so that the equivalence holds?
You can try to interactively solve this problem in
JITPRO by clicking here:
_{2}## The ErrorSpecker chooses
S.
(In fact one can check that if _{i}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
T ↔ T'
are provably equivalent.
Unfortunately, it is not clear whether ↔ should bind more tightly than ∧ or not.
So T could be either
((S_{1} ↔ S_{1}') ∧ S_{2} ∧ ¬S_{2}')
∨ ((S_{2} ↔ S_{2}') ∧ ¬S_{1} ∧ S_{1}')
∨ (¬S_{1} ∧ S_{1}' ∧ S_{2} ∧ ¬S_{2}')
or
(S_{1} ↔ (S_{1}' ∧ S_{2} ∧ ¬S_{2}'))
∨ (S_{2} ↔ (S_{2}' ∧ ¬S_{1} ∧ S_{1}'))
∨ (¬S_{1} ∧ S_{1}' ∧ S_{2} ∧ ¬S_{2}').
We consider both possibilities and show neither works.
Assume so that T' is
((S_{1}' ↔ S_{1}) ∧ S_{2}' ∧ ¬S_{2})
∨ ((S_{2}' ↔ S_{2}) ∧ ¬S_{1}' ∧ S_{1})
∨ (¬S_{1}' ∧ S_{1} ∧ S_{2}' ∧ ¬S_{2}).
Suppose we have formulas S and _{1}S
and a model in which _{2}S and _{1}S are false
but the duals _{2}S and _{1}'S are true.
In this case, the conjunction_{2}'(S is false (both conjuncts are false)._{1} ↔ S_{1}') ∧ (S_{2} ↔ S_{2}')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 so that T' is
(S_{1}' ↔ (S_{1} ∧ S_{2}' ∧ ¬S_{2}))
∨ (S_{2}' ↔ (S_{2} ∧ ¬S_{1}' ∧ S_{1}))
∨ (¬S_{1}' ∧ S_{1} ∧ S_{2}' ∧ ¬S_{2}).
Suppose we have formulas S and _{1}S
and a model in which _{2}S, _{1}S and _{1}'S are false
but _{2}S is true.
In this case, the conjunction_{2}'(S is false (the second conjunct is false)._{1} ↔ S_{1}') ∧ (S_{2} ↔ S_{2}')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 In this case T' is
(¬S
_{1} ∧ S_{2}') ∨ (S_{1} ∧ ¬S_{2}).Before reading the proof, you can try to prove this choice of ## Proof:If
T ↔ T' since T and T' are the same up to the primes.
Assume We must prove (S and _{1} ↔ S_{1}')(S.
We consider two cases.
_{2} ↔ S_{2}')
¬S.
The equivalences hold in this case.
_{1} ∧ S_{2}'
S This is impossible.
_{1} ∧ ¬S_{2}.
¬S. This is impossible.
_{1} ∧ S_{2}'
S
The equivalences hold in this case.
_{1} ∧ ¬S_{2}.
and ((S_{1} ∨ ¬S_{2}') ∧ (¬S_{1} ∨ S_{2})).From this we can conclude four disjunctions by resolution: (¬S_{2} ∨ S_{2}'),(¬S_{2}' ∨ S_{2}),(S and_{1}' ∨ ¬S_{1})(S_{1} ∨ ¬S_{1}').The two equivalences clearly follow. |