Приведите пример в Coq, где (AB: Prop), P: Prop -> Type, такой, что A <-> B, но нельзя заменить PA на PB

Question

Как следует из названия, я приведу sh пример, где:

Section Question:
Definition A: Prop := <whatever you like>.
Definition B:Prop := <whatever you like>.
Definition/Inductive/Fixpoint P: Prop -> Type := <whatever you like>.

Theorem AEquivB: A <-> B.
Proof. <supply proof here>. Qed.

(* Question 1. can we pick a P, A, B to prove this? *)
Theorem PA_not_equals_Pb: P A <> P B.
Proof. <supply proof here>. Qed.

(* Question 1.5. can we pick a P, A, B to prove this? *)
Theorem PA_not_equiv_PB: ~(P A <-> P B)
Proof. <supply proof here>. Qed.  

В общем, мне интересно понять, достаточно ли "доказательственная эквивалентность" "достаточна", чтобы использовать ее как " равенство "в некотором смысле, или есть ли ситуации, когда мы можем иметь P A и A <-> B, но не P B.

Answer 1

Это соответствует Coq, что forall A B : Prop, (A <-> B) -> A = B. (То есть вы можете добавить это как аксиому, и теория не рухнет.) Эта аксиома называется расширением высказываний . Поскольку A = B быстро дает forall P : Prop -> Prop, P A <-> P B, нет таких терминов P, A, B, которые могли бы (A <-> B) /\ ~(P A <-> P B), поскольку это противоречило бы аксиоме, но мы знаем, что она последовательна. Точно так же мы также быстро получаем P A = P B, что означает, что мы также не можем получить P A <> P B. Обратите внимание, что хотя таких P, A, B, которые нарушают экстенсиональность высказываний, не существует, мы все равно не можем доказать экстенсиональность высказываний. Coq просто не в силах так говорить о себе (что хорошо, так как это означает, что вы можете настроить его), поэтому экстенсивность высказываний должна быть добавлена ​​в качестве аксиомы, если вы этого хотите.