I am hoping to look at all the possible bots to submit to a noniterated prisoner's dilemma where both bots can reason about each other's behavior. Can I hide unsafeNecessitation within the definition of prove and/or open a fresh context for prove? Can I construct Coops such that fixedpoint2 is true? How can my proofs be shortened? What should I write differently? In particular the asserts to duplicate hypotheses seem clumsy. How should I automate the application of unfix? How should I automate the search of what theorems to prove?

Require Setoid.

Parameter Provable : Prop -> Prop.
Axiom Pmodus : forall {a b:Prop}, Provable (a -> b) -> Provable a -> Provable b.
Axiom loeb : forall {a:Prop}, Provable (Provable a -> a) -> Provable a.
Axiom unsafeNecessitation: forall {a:Prop}, a -> Provable a. (* WRONG *)
Ltac prove := repeat match goal with 
  | [ H : Provable _ |- _ ] => refine (Pmodus _ H); clear H
end; clear; apply unsafeNecessitation; intuition. (* sometimes doesnt clear *)

Parameter Fixedpoint2 : (Prop -> Prop -> Prop) -> (Prop -> Prop -> Prop) -> Prop. (* SHOULD BE REDUNDANT *)
Notation "A <3 B" := (Fixedpoint2 A B) (at level 70).
Axiom fixedpoint2 : forall {a b}, a <3 b = a (a <3 b) (b <3 a).
Ltac unfix := rewrite fixedpoint2.

Definition Prudent (self other:Prop) := Provable (self <-> other).
Definition Fair    (self other:Prop) := Provable other.
Definition Coop    (self other:Prop) := True.
Definition Defect  (self other:Prop) := False.

Theorem prudentbotcoops : Prudent <3 Prudent. unfix. prove. Qed.

Theorem fairbotcoops : Fair <3 Fair. unfix. apply loeb. prove. unfix. prove. Qed.

Theorem p2pp : forall {a : Prop}, Provable a -> Provable (Provable a).
  intros a pa.
  refine (Pmodus _ (@loeb (a /\ Provable a) _)).
  prove. prove. prove.

Theorem prudentfaircoops : Prudent <3 Fair.
  apply loeb.
  unfix. apply p2pp in H. prove. unfix. assumption.
  unfix. exact H.

Definition PA_1 (a:Prop) := (forall {a:Prop}, Provable a -> a) -> a.

Theorem npnp : forall x, PA_1 (~Provable (~Provable x)).
  intros x trust pnp.
  apply trust.
  apply loeb.
  contradict H.

Theorem fairdbotdefect : PA_1 (~Fair <3 Defect).
  intros trust cooperates.
  rewrite fixedpoint2 in cooperates.
  apply trust in cooperates.
  rewrite fixedpoint2 in cooperates.
  exact cooperates.

(* Take the action for which you can prove the best lower bound. *)
Definition UDT (self other:Prop) := Provable (self -> other) /\ ~Provable (~self -> other).

Theorem theyneverknowUDTcoops : forall b, PA_1(~Provable (UDT <3 b)).
Proof. intros b trust pub. assert (pub' := pub). apply trust in pub. rewrite fixedpoint2 in pub. firstorder.
  clear H. contradict H0. prove.

Notation "'UC'" := (UDT <3 UDT).
Lemma UDTdoesntgetexploitedbyUDT : UC <-> ~Provable (~UC -> UC).
Proof. split.
  intro. rewrite fixedpoint2 in H. firstorder.
  intro. unfix. firstorder. prove.

Lemma modus_tollens: forall {p q: Prop}, (p->q) -> ~q -> ~p. auto. Qed.

Theorem udtcoops : PA_1 UC.
  intros trust.
  rewrite UDTdoesntgetexploitedbyUDT.
  refine (modus_tollens (Pmodus _) (theyneverknowUDTcoops UDT trust)).
  rewrite UDTdoesntgetexploitedbyUDT.
  rewrite UDTdoesntgetexploitedbyUDT in H.

Theorem prudentunexploitable : forall b, PA_1 (Prudent <3 b -> b <3 Prudent).
Proof. intros b trust pb. assert (eq := pb). rewrite fixedpoint2 in eq. apply trust in eq.

Theorem UDTunexploitable : forall b, PA_1 (UDT <3 b -> b <3 UDT).
Proof. intros b trust ub. assert (ub' := ub). rewrite fixedpoint2 in ub. destruct ub as [notexp _].
  apply trust in notexp. firstorder.

Theorem whenPBcoopstheyknow : forall b, Prudent <3 b -> Provable (Prudent <3 b).
  intro b. unfix. intro pb. apply p2pp. firstorder.

Theorem prudentudtdefect : PA_1 (~Prudent <3 UDT).
  intros trust pu.
  absurd (Provable (UDT <3 Prudent)).
  exact (theyneverknowUDTcoops _ trust).
  assert (pu' := pu).
  rewrite fixedpoint2 in pu'.
  refine (Pmodus _ pu').
  refine (Pmodus _ (whenPBcoopstheyknow _ pu)).
  • \$\begingroup\$ I don't think you can use Provable : Prop -> Prop like this. As you've noticed, you cannot reason about when Coq's context is empty. In short, you must either define a separate type PROP of object propositions, or use some Kripke semantics for provability logic to define Provable and the various connectives of your logic. I'm afraid the long version is too long for a comment — hope somebody can help... \$\endgroup\$ Commented Jul 29, 2019 at 15:55
  • 1
    \$\begingroup\$ You might be interested in github.com/JasonGross/lob-paper/blob/master/… which proves in Agda that that FairBot cooperates with itself, and github.com/JasonGross/lob, which demonstrates how to encode Löb's theorem in both Coq and Agda both axiomatically and via an internal AST. \$\endgroup\$ Commented Aug 6, 2019 at 3:10


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.