Here is an informal explanation of the one-point laws. Let’s start with ∃v: D· v=x ∧ b
and we are given x: D . Let’s suppose D is disjunction.
(0=x ∧ b) ∨ (1=x ∧ b) ∨ (2=x ∧ b) ∨ … We can use context in each of these disjuncts.
nat .
The existential quantification is an infinite
(0=x ∧ ( b ∨ (1=x ∧ ( b ∨ (2=x ∧ ( b ∨ …
but replace but replace but replace
x with x with x with
0 )) 1 )) 2 ))
Since x isin nat,exactlyoneof 0=x,1=x,2=x,…is ⊤ andtheothersare ⊥. That’swhyit’s called “one-point”. Let’s suppose x is 1 .
(⊥ ∧ ( b ∨ (⊤ ∧ ( b ∨ (⊥ ∧ ( b ∨ …
but replace but replace but replace
x with 0 )) x with 0 )) x with 0 ))
= ⊥ ∨ ( b but replace x with 1 ) ∨ ⊥ ∨ …
= ( b but replace x with 1 )
Now the other one. ∀v: D· v=x ⇒ b
and we are given x: D . Let’s suppose D is conjunction.
(0=x ⇒ b) ∧ (1=x ⇒ b) ∧ (2=x ⇒ b) ∧ … We can use context in each of these conjuncts.
nat .
The universal quantification is an infinite
(0=x ⇒ ( b ∧ (1=x ⇒ ( b ∧ (2=x ⇒ ( b ∧ …
but replace but replace but replace
x with x with x with
0 )) 1 )) 2 ))
Since x isin nat,exactlyoneof 0=x,1=x,2=x,…is ⊤ andtheothersare ⊥. That’swhyit’s called “one-point”. Let’s suppose x is 1 .
(⊥ ⇒ ( b ∧ (⊤ ⇒ ( b ∧ (⊥ ⇒ ( b ∧ …
but replace but replace but replace
x with x with x with
0 )) 0 )) 0 ))
= ⊤ ∧ ( b but replace x with 1 ) ∧ ⊤ ∧ …
= ( b but replace x with 1 )